Mathematical Agential Semioverse Repository

This specification defines what an Agential Semioverse Repository looks like when its content domain is mathematics. It extends the general ASR’s type vocabulary and typed relations with content types and relations specific to mathematical knowledge.

The general ASR defines types like term, concept, and text that describe what a page is for, but not what makes it valid within a particular domain. Mathematical content has structural validity requirements that general types cannot express: a theorem without a proof is not a theorem — it is a conjecture. A proof that does not specify what it proves is meaningless. These requirements are constitutive: the presence or absence of certain relations determines what the content IS.

Validity principle: provability

Mathematical knowledge is governed by provability. Content is valid when it is grounded — traceable through a chain of proofs, definitions, and axioms to accepted starting points. The dependency graph is directed and acyclic: axioms are taken as given, definitions establish vocabulary, and theorems are demonstrated from these through proofs.

Machine verification (via Lean or similar proof assistants) is possible in this domain because validity is formal. The proven-by relation accepts both natural-language proofs (.md) and machine-checked proofs (.lean).

Content types

These extend the general ASR type: field. Each type carries validity requirements expressed as MUST (constitutive — violation means the content is ill-formed or mistyped) and SHOULD (recommended but not constitutive).

definition

Establishes the meaning of a mathematical term or structure within a formal context.

• MUST include defines: listing terms or structures being defined (at least one).
• MUST specify enough formal context (inline or via requires:) that the definition is unambiguous.
• MUST NOT depend on itself.
• SHOULD declare notation: listing symbolic representations.
• SHOULD link to example pages via has-example:.
• SHOULD link to related definitions via extends: or requires:.

type: definition
defines:
  - "group"
requires:
  - /mathematics/objects/prealgebra/terms/monoid.md

axiom

A proposition taken as given within a theory. Not proven.

• MUST state the proposition clearly in the body.
• MUST specify part-of: identifying the axiomatic system.
• MUST NOT have a proven-by: relation.
• SHOULD specify enables: listing results that depend on it.

type: axiom
part-of: zermelo-fraenkel-set-theory
defines:
  - "axiom of choice"

theorem

A proposition proven true within a formal system. Distinguished from lemma and proposition by significance, not logical status.

• MUST have proven-by: linking to at least one proof (.md or .lean). Without proof, use conjecture.
• MUST specify requires: listing dependencies.
• SHOULD link to corollaries.
• MAY have multiple proofs.

type: theorem
defines:
  - "fundamental theorem of algebra"
requires:
  - /mathematics/objects/fields/terms/algebraically-closed-field.md
proven-by:
  - /mathematics/objects/fields/proofs/fta-topological.md

proof

A demonstration that a proposition is true. Always of something.

• MUST specify proves: linking to exactly one theorem, lemma, or proposition.
• MUST contain a complete argument in the body.
• MUST specify uses: listing definitions, axioms, and results invoked.
• SHOULD name the proof technique in a technique: field (direct, contradiction, induction, construction, etc.).

type: proof
proves: /mathematics/objects/fields/theorems/fta.md
technique: topological
uses:
  - /mathematics/objects/topology/theorems/brouwer-fixed-point.md

lemma

Auxiliary result supporting a theorem’s proof. Same logical status as theorem.

• MUST be proven (proven-by:).
• MUST specify requires:.
• SHOULD specify supports: linking to the theorem(s) it serves.

proposition

Proven result of intermediate significance. Same requirements as theorem.

corollary

Result following readily from a theorem.

• MUST specify follows-from: linking to the source theorem.
• MUST have proven-by: (even if brief).

conjecture

Proposition believed true but not yet proven.

• MUST NOT have proven-by:. If proven, reclassify as theorem.
• SHOULD specify evidence: listing heuristic support.

example

Concrete instance illustrating a definition, theorem, or concept.

• MUST specify illustrates: (at least one target).
• MUST be concrete — specific values, structures, or constructions.

counterexample

Concrete instance demonstrating a statement is false.

• MUST specify refutes: linking to the target statement.
• MUST be concrete.
• MUST demonstrate explicitly why the instance violates the target.

Relation vocabulary

These typed relations extend the general ASR’s semantic frontmatter relation set.

These relations carry mathematical validation requirements intrinsically. When a page uses proven-by, the SHACL shapes for that relation validate it — regardless of where the page lives or what other relations it uses. See Domain-Specific Content for how domain-specific relations coexist in a single repository.

Notation

Mathematical objects SHOULD declare their symbolic notation via a notation: frontmatter field.

notation:
  - symbol: "S"
    for: "successor function"
  - symbol: "S(n)"
    for: "successor of n"

Scoping rules

Notation is scoped to fragments. Each page constitutes a local fragment; its requires: chain defines its scope (the page plus everything it depends on).

• Within a page’s scope: each symbol MUST denote at most one thing. If page A requires page B, and both introduce notation, the combined notation set must be unambiguous. A conflict means the page needs to qualify or rename.
• Across unrelated pages: the same symbol MAY denote different things. This is standard mathematical overloading — + in the natural numbers, + in a vector space, and + in a lattice (as join) are different operations sharing a symbol because they share algebraic structure.
• Across fragments: the same object MAY have different notation. Composition can be written ∘, ·, or by juxtaposition depending on context. A group operation may be written additively or multiplicatively depending on convention.

This mirrors the Interactive Semioverse fragment model: fragments are local contexts with their own notation, and sheaf semantics handles coherence at overlaps.

Why SHOULD, not MUST

Not every mathematical object has conventional notation (some are referred to only by name), and forcing notation where none is standard creates artificial symbols that obscure rather than clarify. The requirement is constitutive only in the negative direction: when notation IS declared, the scoping rules MUST hold.

Dependency graph

The mathematical dependency graph is a DAG (directed acyclic graph):

axiom ──enables──► theorem ◄──proven-by── proof ──uses──► definition
                      │                                      axiom
                      │                                      theorem
             corollary ──follows-from──► theorem

Cycles indicate an error. The SHACL shapes catch direct self-reference; transitive cycle detection requires a build-time validator.

Formal artifacts

• Ontology — OWL classes and properties for mathematical content types
• SHACL Shapes — validation shapes for mathematical relations

Lean correspondence

Mathematics is the domain closest to formal verification. The existing Lean formalization at formalization/Relationality/ proves that the recognition field axioms constitute a Heyting algebra (Genesis.lean).

What this domain’s axioms look like formally. Each content type T defines a theory Phi_T: the set of MUST/SHOULD axioms. For mathematics, these theories are unusually precise — a theorem’s theory requires proven-by: to point to a page of type proof, which is a formal dependency that Lean can express and verify.

What satisfaction means beyond field presence. The current Python approximation checks whether proven-by: exists and whether its target is type proof. Full satisfaction would verify that the proof actually proves the theorem — that the logical content of the proof page entails the claims of the theorem page. This is exactly what Lean proofs do. The .lean files colocated with mathematical content ARE the Layer 2 verification for this domain.

Current satisfaction data. 22 typed pages checked, 22 satisfied (100.0%), 0 errors, 13 warnings (all SHOULD gaps: missing notation, missing cites).

Lean target. Formalize the mathematical content type theories as Lean type classes. A MathTheorem structure would carry a proof field typed to MathProof, enforcing the proven-by axiom at the type level. The existing Lean code proves the algebra; extending it to prove that the mathematical ASR’s axioms correctly instantiate the semiotic universe’s type theories is the next step.