Proof Governance & Verification Scale

Orthogonal Status Coordinates S = (F, C, P, R, V), Formal Proof Standards & Epistemic Boundaries

Spine Position

Mathematics Root · Formal Proof Governance, Orthogonal Coordinates & Quality Gates

Public Status Boundary. To protect the integrity of the mathematical and physics canon, all theoretical propositions, candidate theorems, and formal models in the Science of Fabric Reality are governed by an explicit orthogonal coordinate system. Status coordinates are claim-local: they classify a specific evidentiary object (theorem, manuscript, simulation, implementation, prediction, experiment, review event, publication artifact), not an entire conceptual horizon or heterogeneous research program.

$$\boxed{{\displaystyle F\ne C\ne P\ne R\ne V}}$$$$\boxed{{\displaystyle \mathbf{\text{Formal Proof}}\ne \mathbf{\text{Numerical Simulation}}\ne \mathbf{\text{Empirical Confirmation}}\ne \mathbf{\text{Peer Review}}\ne \mathbf{\text{Publication}}}}$$

---

1. The Orthogonal Status Coordinate Architecture

Rather than compressing distinct scientific dimensions into a single overloaded ordinal ladder, every claim and evidentiary object in the corpus is evaluated along five independent, orthogonal axes:

$$S=(F,C,P,R,V)$$

• $F$ — Formal / Mathematical Status: Degree of deductive mathematical rigor ($F0$ through $F5$).
• $C$ — Computational Status: Depth and reproducibility of algorithmic/numerical implementation ($C0$ through $C5$).
• $P$ — Prediction / Empirical Status: Degree of empirical contact, calibration, and prospective observation ($P0$ through $P6$).
• $R$ — Review Status: Level of documented peer critique and refereeing ($R0$ through $R3$).
• $V$ — Publication / Provenance Status: Publication venue, archiving, and public accessibility ($V0$ through $V4$).

Claim-Local Evaluation Rule

Status coordinates apply strictly to specific evidentiary objects. A broad research program cannot be assigned a single universal tuple: it may simultaneously contain $F4\text{-CHECKED}$ theorem artifacts, $C3$ numerical benchmarks, $P2$ calibrated fits, $R1$ internal critiques, and $V1$ publication records. Where documentary evidence for a specific dimension is absent, that coordinate is designated NOT_CLASSIFIED.

---

2. Axis Definitions & Verification Gates

A. Formal / Mathematical Axis ($F$)

• $F0$ — Heuristic Motivation: Informal descriptive physical or mathematical intuition.
• $F1$ — Typed Statement: Mathematically typed proposition declaring carrier sets, operators, and invariance groups.
• $F2$ — Proof Architecture: Explicit lemma tree and structural proof strategy with isolated boundary conditions.
• $F3$ — Paper Proof: Complete human-readable analytical derivation in manuscript format.
• $F4\text{-DRAFT}$ — Formalization Open: Syntactic Lean 4 source stubs under active construction.
• $F4\text{-CHECKED}$ — Machine Verified: Interactive Lean 4 proof closed by the compiler kernel without sorry or admit stubs (35 verified declarations across 11 modules in Fabrica.*, with 0 quarantined axioms).
• $F5$ — Canonical Formal Artifact: Machine-checked proof fully integrated into the sovereign mathematical library.

Machine Verification Rule

$F4\text{-CHECKED}$ certifies that the Lean 4 compiler verified the encoded theorem under its stated hypotheses and formal axioms. It does not imply empirical truth, physical realization, journal review, or whole-theory verification.

B. Computational Axis ($C$)

• $C0$ — None: No algorithmic or numerical implementation.
• $C1$ — Toy Model: Exploratory script or discrete toy model.
• $C2$ — Numerical Sanity Check: Solver stability and discretization sanity checks.
• $C3$ — Computational Benchmark: Formal benchmark testing bounded error and convergence.
• $C4$ — Implementation Test: Automated continuous integration test suite with regression protection.
• $C5$ — Reproducible Implementation: Deterministic, environment-independent computational pipeline.

Simulation Is Not Proof

Numerical simulation belongs exclusively to the computational axis ($C$). Simulation models stress-test mathematical assertions and boundary limits; they never constitute formal mathematical proofs. The legacy label M4-SIMULATION is deprecated.

C. Prediction / Empirical Axis ($P$)

• $P0$ — Formal Identity: Deductive mathematical relation with no direct physical observable mapping.
• $P1$ — Numerical Benchmark: Computational baseline in model space.
• $P2$ — Calibrated Retrodiction: Post-hoc parameter calibration to known empirical data ($D_H^{\ast }=27.6\pm 0.3$).
• $P3$ — Held-Out Target: Statistical evaluation against held-out datasets or experimental benchmarks.
• $P4$ — Prospective Prediction: Pre-registered predictive invariant sealed prior to experimental test (ACTIVE_P4_SEALS = 0).
• $P5$ — Empirical Test Result: Empirical test measurement testing a prospective prediction.
• $P6$ — Replicated Empirical Result: Independent empirical replication confirmed across multiple experimental teams.

Empirical Demarcation

$P5$ requires an empirical measurement result. Independent external replication is classified under $P6$. The permutation result $p_{\text{null}}=0.62$ represents a NULL_ANALYSIS_RESULT and calibrated negative benchmark, not a fundamental physical constant.

D. Review Axis ($R$)

• $R0$ — No Documented Review: Unreviewed internal authorial draft.
• $R1$ — Internal Critique Recorded: Formal critique recorded via the SFR Review Portal or internal authorial critique intake.
• $R2$ — External Critique Documented: Documented commentary or critical reports from independent external scholars.
• $R3$ — External Peer Review Outcome Recorded: Formal peer-review outcome (accept, reject, revise) recorded by an independent academic journal editorial board or conference referee body.

Review Boundary

The existence of the SFR Review Portal does not automatically grant $R1$ to every corpus artifact; $R1$ requires a recorded critique event for the specific object. Internal critique intake must not be represented as independent external peer review ($R3$).

E. Publication / Provenance Axis ($V$)

• $V0$ — Internal Artifact: Private working document or draft.
• $V1$ — Public Corpus Artifact: Published within the public IvanPasev.com / Fabrica corpus.
• $V2$ — Archived / DOI Registered: Deposited in an open repository (Zenodo, arXiv, OSF) with persistent identifier.
• $V3$ — Submitted to External Venue: Formally submitted for consideration to an independent academic publisher.
• $V4$ — Externally Published: Formally accepted and published by an independent external venue or publisher.

Publication Demarcation

$V4$ denotes external publication venue acceptance; it does not evaluate the review process, which is tracked independently on the $R$-axis ($R3$). Persistent DOI registration ($V2$) timestamping does not constitute peer review ($R3$).

---

3. Legacy M0–M5 Lifecycle Crosswalk (PARTIAL HISTORICAL CROSSWALK)

Important Epistemic Invariant: Non-Lossless Mapping. THE LEGACY M SCALE IS NOT LOSSLESSLY MAPPABLE TO $(F,C,P,R,V)$. The legacy M0–M5 scale was an overloaded composite metric that compressed formal rigor, computational solvers, and empirical status into an informal linear ladder. This section provides a PARTIAL HISTORICAL CROSSWALK — NOT A STATUS PROMOTION TABLE. Non-formal axes ($C,P,R,V$) are strictly designated NOT_CLASSIFIED unless independent object-level documentary evidence exists.

Legacy Tier	Former Description	Possible Formal Implication	Non-Formal Coordinates ($C,P,R,V$)	Epistemic Boundary Note
M0	Historically heuristic / conceptual	$F0$	NOT_CLASSIFIED	Informal descriptive motivation; no non-formal coordinates implied.
M1	Historically formal definition	$F1$	NOT_CLASSIFIED	Mathematically typed statement; no non-formal coordinates implied.
M2	Historically proof architecture	$F2$	NOT_CLASSIFIED	Structured lemma strategy; no non-formal coordinates implied.
M3	Historically paper proof	$F3$	NOT_CLASSIFIED	Human-readable manuscript derivation; review ($R$) and publication ($V$) require independent evidence.
M4-CHECKED	Historically machine-verified theorem	$F4ext-CHECKED$	NOT_CLASSIFIED	Lean 4 compiler verified (0 sorry, 0 admit); empirical/venue axes require independent evidence.
M4-SIMULATION (Deprecated)	Historically numerical solver / simulation	NO FORMAL-AXIS MAPPING	Independently evidenced only ($C1$–$C5$, $P$, $R$, $V$)	Numerical computation is strictly classified on $C1$–$C5$. Simulation is not mathematical proof.
M5	Historically external / empirical	NO DIRECT MAPPING	Independently evidenced across $F,P,R,V$	Historically bundled incompatible notions. Decomposed independently across $F$, $P$, $R$, $V$ by evidence.

4. Hard Epistemic Invariants

1. Machine Verification Scope: $F4\text{-CHECKED}$ applies strictly to the encoded theorem declaration and its explicit hypotheses in Lean 4. It does not certify the global physical theory or empirical truth.
2. Review Integrity: Internal review within the SFR Review Portal is classified as $R1$. External peer review ($R3$) requires documented independent external refereeing.
3. Zero Prospective Seals: Prospective physical predictions remain strictly sealed (ACTIVE_P4_SEALS = 0).
4. Calibrated Constants: $D_H^{\ast }=27.6\pm 0.3$ remains a calibrated fit parameter ($P2$).
5. Null Analysis Result: $p_{\text{null}}=0.62$ is a NULL_ANALYSIS_RESULT establishing negative Fisher information rank bounds.

---

5. Canonical Continuations

Direction	Target Resource	Purpose
Mathematics Root	Formal Mathematics Spine →	Axiomatic governance and formal proof architecture
Proof Tracker	Lean 4 Formalization Roadmap →	35 machine-verified theorem records and lemma dependency DAGs
Publication Register	Publication Status & Maturity Register →	Provenance tracking across V-axis and R-axis
Results Ledger	Scientific Results Ledger →	Coordinated ledger of formal proofs, computational bounds, and empirical fits
Falsifiability Index	Falsifiability Index & Negative Theorems →	Explicit model failure, computational bounds, and null benchmarks