Public Review and Formalization Gateway ​

This gateway explains how authorial claims in the public corpus are routed into theorem targets, proof obligations, implementation tests, and external review pathways. It is for readers who want to inspect readiness and boundary conditions rather than consume a finished proof narrative. The page should be read as a local scaffold for formalization and review preparation; it does not imply proposed theorems, completed proof-assistant exports, or accepted publication status.

Page Thesis ​

This gateway transforms the contributor and discovery canons into a routeable, inspectable proof and readiness interface. It bridges the gap between authorial frameworks and formal verification paths.

Claim-to-Proof Routing ​

This map routes public claims into proof obligations, implementation tests, or external review paths.

Theorem Target Registry ​

Defines the current public state of evidence for each authorial discovery, explicitly noting where independent mathematical or peer validation is still required.

Scientific Review Dossier ​

REV

Scientific Review Dossier

This theory is indexed in the Scientific Review Dossier, where claims are mapped to evidence classes, source anchors, theorem targets, and review-readiness status.

Open the Scientific Review Dossier →

Verification Status Dashboard ​

Tracks internal readiness of formalization targets across distinct status tiers (S0 through S7).

Proof Obligation Index ​

Decomposes theorem targets into explicit obligations required before formal verification can proceed.

Formalization Queue ​

Outlines the priority sequence for formalization efforts:

  1. Priority 1 - Definitions (Fabricon tuple semantics, Digital Fabric object, etc.)
  2. Priority 2 - Architecture Theorems (DFT invariant preservation, CodexStation ordinal execution)
  3. Priority 3 - Theorematic Targets (ISP Trace Reciprocity, Observer-Knot Algebra)
  4. Priority 4 - Physics-Facing Review (Equations, predictions, falsifiability criteria)

Implementation Test Matrix ​

Maps implementation readiness to specific test types and evidence.

Lean 4 Formalization Inventory & Proof Exports ​

The repository maintains 35 machine-verified Lean 4 theorem declarations across 11 formal modules in docs/04-mathematics/lean/Fabrica/ (with 0 quarantined axioms under pinned Lean 4.16.0):

  • Fabrica.KPField (6 proofs) — Non-local kernel symmetry, generator symmetry, resolvent norm contraction bound, deficiency indices nullity, Cayley transform unitarity, and maximal self-adjoint domain closure.
  • Fabrica.InvariantEngineering (3 proofs) — Identity invariant preservation, composite transformation preservation, and invertible admissible transition equivalence.
  • Fabrica.ObserverKnot (3 proofs) — Commuting observer projector composite idempotence, identity projector, left-absorption.
  • Fabrica.TraceReciprocity (3 proofs) — Bilinear trace involution ⟨x,y⟩τ⟺⟨y,x⟩τ, dual symmetry, reflexive self-duality.
  • Fabrica.FFE (4 proofs) — Variational stationarity, KKT zero-nullity boundary, homogeneous triviality, multiplier superposition.
  • Fabrica.FQFT (4 proofs) — Two-sided resolvent inverse, algebraic and exact First Resolvent Identity, shifted difference.
  • Fabrica.PGP (3 proofs) — Gauge identity, composition, and orbit invariance.
  • Fabrica.ObserverMonad (3 proofs) — Categorical monad left identity, right identity, and associativity.
  • Fabrica.Fabricon (3 proofs) — Reflexive coupling, conjugate involution, and coupling symmetry.
  • Fabrica.Realica (3 proofs) — Fixed-point idempotence, sequence convergence, and partition conservation.
  • Fabrica (0 theorems, master certificate) — Umbrella compilation and deductive soundness certificate.

Reader Path ​

Source Anchor Requirements ​

Equation Hygiene Register ​