Constitutional Axioms & Object Register

Source Primitives, Formal Object Classifications & Open Proof Obligations

Spine Position

Mathematics Root · Constitutional Axioms, Primitive Classifications & Proof Obligations

Public Status Boundary: Active Research Register

This register establishes the formal terminology, source-bound primitives, and open proof obligations of Digital Fabrica Theory (DFT). Entries are strictly classified according to canonical source support; narrative descriptions are not promoted to formal axioms, and unsupported equations are quarantined with integrationAllowed = false.

1. Terminology Law & Classification Taxonomy

To prevent informal claim inflation, every entry in this register is governed by an explicit classification schema in accordance with Ω281A-R4:

• SOURCE_OBJECT_IDENTIFIED: A constructive mathematical assignment of a named formal object, tensor, or metric in canonical prose with source-window provenance.
• FORMALIZATION_PROPOSAL_QUARANTINED: A proposed mathematical equation or functional expression quarantined with integrationAllowed = false until exact canonical source text support is established.
• STANDARD_COMPARATOR: A familiar mathematical or physical equation referenced as a comparison baseline rather than an extracted foundational postulate of DFT/FQFT.
• ABSTRACT_LEAN_INTERFACE: A Lean 4 type declaration, class, or structure interface that defines relational signatures without claiming to prove external matrix or physical identities.
• LEAN_SOURCE_PRESENT_UNCOMPILED: Lean 4 formalization source code is present in /docs/04-mathematics/lean/Fabrica/ but is uncompiled on the local station (LEAN_TOOLCHAIN_UNAVAILABLE = TRUE).
• LEAN_BUILD_VERIFIED: Executable lake build evidence confirms clean compilation of Lean declarations and theorems without errors.
• AXIOM_DECLARATION: A Lean axiom statement within a formal library (distinct from a constructive theorem proof). Standard Lean kernel axioms (such as Quot.sound or propositional extensionality propext) are Lean foundational/kernel-level logical dependencies, distinct from project-declared scientific or ontological axioms.
• THEOREM_PROOF_VERIFIED: A machine-verified Lean theorem proven without sorry or admit.

---

2. Register Table

ID	Object	Source-supported statement	Source class	Candidate formalization	Formal state	Evidence
AX-01	Adjacency Conservation	Named invariant candidate ("The Adjacency Conservation")	SOURCE_OBJECT_IDENTIFIED	$\sum _{j\in \mathrm{Adj}(i)}{\mathrm{\Phi }}_{ij}=0\mathrm{\forall }i\in V$ (Quarantined proposal)	NO_FORMAL_ARTIFACT	docs/02-foundations/fabric-field-equation.md
AX-02	Fabric Energy Tensor	Named formal object ("The Fabric Energy Tensor")	SOURCE_OBJECT_IDENTIFIED	$T_{\mu \nu }={\partial }_{\mu }\mathrm{\Phi }{\partial }_{\nu }\mathrm{\Phi }-\frac{1}{2}{g}_{\mu \nu }({\partial }_{\alpha }\mathrm{\Phi }{\partial }^{\alpha }\mathrm{\Phi }-V(\mathrm{\Phi }))$ (Quarantined proposal)	NO_FORMAL_ARTIFACT	docs/02-foundations/fabric-field-equation.md
AX-03-CONCEPT	Trace / ISP Reciprocity (Source Concept)	Authorial proposed symmetry between ISP and trace transport	SOURCE_OBJECT_IDENTIFIED	(Source concept, lines 19–22)	NO_FORMAL_ARTIFACT	docs/02-foundations/trace-isp-reciprocity.md
AX-03-COMPARATOR	Trace Reciprocity Standard Comparator	Standard matrix trace identity $\mathrm{Tr}(AB)=\mathrm{Tr}(BA)$	STANDARD_COMPARATOR	$\mathrm{Tr}(AB)=\mathrm{Tr}(BA)$ (Standard comparator, not extracted from authorial source)	NO_FORMAL_ARTIFACT	docs/02-foundations/trace-isp-reciprocity.md
AX-03-LEAN	Trace Reciprocity Abstract Lean Interface	Abstract symmetric relation interface (class TracePairing)	ABSTRACT_LEAN_INTERFACE	structure TracePairing (α : Type) (Verified involution: thm_trace_involution in Fabrica.TraceReciprocity)	THEOREM_PROOF_VERIFIED	docs/04-mathematics/lean/Fabrica/TraceReciprocity.lean

---

3. Removed and Quarantined Entries

In accordance with the Canonical Equation Provenance Law, the following previously displayed entries have been removed from the source-backed register and quarantined with integrationAllowed = false:

• AX-04 (Quantum Field Operator Action): Displayed mode expansion $\hat{\mathrm{\Psi }}(x,t)=\sum _k(u_k(x){\hat{a}}_k{e}^{-i{\omega }_{k}t}+v_k^{\ast }(x){\hat{b}}_k^{†}{e}^{i{\omega }_{k}t})$ does not occur in the cited canonical source lines of docs/02-foundations/science-of-fabric-reality.md. Classification: FORMALIZATION_PROPOSAL_QUARANTINED.
• AX-05 (Phase-Space Infimum Metric): Canonical source contains shortest-path and structural-law prose, not the displayed infimum metric equation $d_F(x,y)=\underset{\gamma }{inf}{\int }_{\gamma }\sqrt{g_{ij}d{x}^{i}d{x}^j}$. Classification: FORMALIZATION_PROPOSAL_QUARANTINED.
• AX-06 (FQFT Scale Transition Functional): The simulation route does not contain the displayed path-integral generating functional $\mathcal{Z}=\int \mathcal{D}[\mathrm{\Phi }]\exp (\frac{i}{\hslash }S[\mathrm{\Phi }])$. Classification: FORMALIZATION_PROPOSAL_QUARANTINED.
• FQFT_closure (Discrete Scale Inductive Closure): The former provisional axiom declaration in Fabrica.FQFT has been discharged and de-quarantined via machine-verified inductive scale closure (thm_fqft_inductive_scale_closure in Fabrica.FQFT alongside the maximal self-adjoint domain closure thm_kp_selfadjoint_domain_closure in Fabrica.KPField), achieving zero quarantined axioms across the formal library. Classification: THEOREM_PROOF_VERIFIED.

---

4. Proposed Dependency Map

The logical dependencies among canonical primitives constitute an authorial proposed dependency map restricting admissible verification paths:

graph TD
    AX01["AX-01: Adjacency Conservation (Source Object Identified)"] --> AX02["AX-02: Fabric Energy Tensor (Source Object Identified)"]
    AX01 --> AX03C["AX-03-CONCEPT: Trace / ISP Reciprocity (Source Concept)"]
    AX03C --> AX03COMP["AX-03-COMPARATOR: Trace Reciprocity Standard Comparator"]
    AX03C --> AX03LEAN["AX-03-LEAN: Trace Reciprocity Abstract Lean Interface"]

---

5. Consistency & Independence Obligations

1. Consistency Obligation (OBL-CONSISTENCY-01): Show that the discrete conservation law candidate AX-01 converges smoothly to a continuum divergence-free tensor condition derived from AX-02 in the limit of infinitesimal lattice spacing.
2. Independence Obligation (OBL-INDEPENDENCE-01): Establish that AX-03-CONCEPT (Trace Reciprocity) cannot be formally deduced from AX-01 on non-commutative graphs without adjoining an explicit cyclic trace condition.

---

6. Source Ledger & Provenance

All entries are grounded in canonical primary source files within the repository:

• AX-01: docs/02-foundations/fabric-field-equation.md (lines 67–74, SHA-256: b746df7361087318e27c936e45a8ccfae9b2ad1623a8cb41ca5c0352e40b491f)
• AX-02: docs/02-foundations/fabric-field-equation.md (lines 58–66, SHA-256: b746df7361087318e27c936e45a8ccfae9b2ad1623a8cb41ca5c0352e40b491f)
• AX-03-CONCEPT: docs/02-foundations/trace-isp-reciprocity.md (lines 19–22, SHA-256: 9fee31116afacc975791c1806ca90b1510ab055eb87beba04dc1d902044bfca6)
• Quarantined Entries (AX-04–AX-06): Logged in provenance/equation-provenance-ledger-v5.json with integrationAllowed = false.

Full cryptographic provenance is recorded in provenance/equation-provenance-ledger-v5.json and provenance/axiom-decision-ledger-v5.json, and packaged in canonical-sources/.

---

7. Revision Protocol

Any amendment to this register requires:

1. Canonical source-trace mapping with exact line-window grounding.
2. Verification of non-importation of external physical or engineering obligations.
3. Automated layout and link verification against npm run docs:build.

---

8. Citation & Manuscript A Metadata

Standard Citation

Pasev, I. (2026). Principia Fabrica: Relational Foundations and Invariant Engineering in Topological Substrates. Research manuscript (Manuscript A), version 1.0.0. https://ivanpasev.com/04-mathematics/axioms

BibTeX Record

@misc{Pasev2026PrincipiaFabrica,
  author       = {Ivan Pasev},
  title        = {Principia Fabrica: Relational Foundations and Invariant Engineering in Topological Substrates},
  year         = {2026},
  month        = {September},
  howpublished = {Research manuscript (Manuscript A), version 1.0.0},
  institution  = {Global Institute of Logic & Cybernetics (GILC)},
  url          = {https://ivanpasev.com/04-mathematics/axioms}
}

---

9. Canonical Continuations

Results Ledger35 Proofs

Scientific Results Ledger

35 machine-verified Lean 4 theorems across 11 modules and canonical negative null benchmark (p_null = 0.62).

Inspect Results Ledger →

Proof GatewayLemma DAGs

Lean 4 Formalization Roadmap

35 machine-verified theorem records, compilation receipts, and acyclic lemma dependency graphs.

Inspect Roadmap →

Code Specifications11 Modules

Formalization Batch 1 Specification

Direct Lean 4 formal module specifications across foundations, gauge principles, and spectral theory.

Inspect Batch 1 →

Spine RootMathematics Root

Formal Mathematics Spine

Complete 9-tier status taxonomy, manuscript collection, and deductive proof architecture.

Inspect Spine →

Verification StandardsS = (F, C, P, R, V) Coordinates

Proof Governance Framework

Six-stage verification lifecycle and quality gates governing formal theorem promotion.

Review Governance →

Theorem CandidatesFrontier

Theorem Candidates Registry

Classified repository of candidate theorems across spectral graph theory and operator algebras.

Inspect Candidates →