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).
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 Adj (i)} Φ_{i j} = 0 \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_{μ ν} = \partial_{μ} Φ \partial_{ν} Φ - \frac{1}{2} g_{μ ν} (\partial_{α} Φ \partial^{α} Φ - V (Φ))$ (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 $Tr (A B) = Tr (B A)$	`STANDARD_COMPARATOR`	$Tr (A B) = Tr (B A)$ (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{Ψ} (x, t) = \sum_{k} (u_{k} (x) {\hat{a}}_{k} e^{- i ω_{k} t} + v_{k}^{*} (x) {\hat{b}}_{k}^{†} e^{i ω_{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) = inf_{γ} \int_{γ} \sqrt{g_{i j} 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 $Z = \int D [Φ] \exp (\frac{i}{ℏ} S [Φ])$ . Classification: FORMALIZATION_PROPOSAL_QUARANTINED.

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

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.
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:

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

8. Canonical Continuations

Direction	Target Resource	Purpose
Proof Gateway	Lean 4 Formalization Roadmap →	28 machine-verified theorem records and lemma dependency DAGs
Proof Governance	Proof Governance & Verification Scale →	Six-stage M0–M5 verification scale and quality gates
Theorem Candidates	Theorem Candidates Registry →	Candidate theorems across spectral graph and operator theory
Mathematics Spine	Formal Mathematics Spine →	Complete 9-tier status taxonomy and manuscript collection

Constitutional Axioms & Object Register ​

1. Terminology Law & Classification Taxonomy ​

2. Register Table ​

3. Removed and Quarantined Entries ​

4. Proposed Dependency Map ​

5. Consistency & Independence Obligations ​

6. Source Ledger & Provenance ​

7. Revision Protocol ​

8. Canonical Continuations ​