simplicial_linearization_discharge
If a deficit angle functional D is calibrated against a weighted ledger graph G, meaning its Regge sums on conformal edge-length fields match the scaled Laplacian actions of G, then the Regge deficit linearization hypothesis holds. Researchers proving the field-curvature identity in simplicial Regge calculus or Recognition Science would cite this result. The proof is a one-line wrapper applying the definitional equivalence between calibration and the hypothesis.
claimLet $D$ be a deficit angle functional on $n$-simplices, $a>0$, hinges a list of hinge data, and $G$ a weighted ledger graph. If for every log-potential $ε$ the Regge sum of $D$ on the conformal edge-length field equals $jcost_to_regge_factor$ times the Laplacian action of $G$ on $ε$, then the Regge deficit linearization hypothesis holds.
background
This declaration sits in Phase C5 of the program to prove the paper's Theorem 5.1 (field-curvature identity) as a Lean theorem. The module composes Phases C1–C4 into a general simplicial discharge of the ReggeDeficitLinearizationHypothesis. WeightedLedgerGraph is the structure carrying non-negative symmetric edge weights that represent the discrete Laplacian action (quadratic J-cost Dirichlet energy). CalibratedAgainstGraph is the property that regge_sum D (conformal_edge_length_field a ha ε) hinges equals jcost_to_regge_factor times laplacian_action G ε for all ε; the referenced sibling shows this property is definitionally identical to ReggeDeficitLinearizationHypothesis. The cubic case supplies explicit calibration; the general simplicial case uses Phase C4's linear_regge_vanishes together with the Schläfli identity.
proof idea
The proof is a one-line wrapper that applies the left-to-right direction of the equivalence lemma calibrated_iff_hypothesis. This lemma states that CalibratedAgainstGraph and ReggeDeficitLinearizationHypothesis are definitionally the same statement, so the calibration hypothesis directly yields the target.
why it matters in Recognition Science
The result supplies the general simplicial discharge used by field_curvature_identity_simplicial to equate J-cost Dirichlet energy with (1/κ) times the Regge action on the conformal field, and by simplicialFieldCurvatureCert to assemble the full certificate. It completes Phase C5 for the paper's Theorem 5.1 on the field-curvature identity in piecewise-flat Regge calculus, generalizing the cubic lattice discharge from CubicDeficitDischarge. The argument relies on the Recognition Composition Law and the eight-tick octave structure to guarantee the linear term vanishes while the quadratic term matches.
scope and limits
- Does not establish the calibration condition itself (supplied by Phase C4).
- Does not apply outside calibrated simplicial complexes.
- Does not compute explicit numerical values for constants or fields.
- Does not address curvature terms beyond the linearization hypothesis.
Lean usage
simplicial_linearization_discharge D a ha hinges G hCalformal statement (Lean)
110theorem simplicial_linearization_discharge {n : ℕ}
111 (D : DeficitAngleFunctional n) (a : ℝ) (ha : 0 < a)
112 (hinges : List (HingeDatum n)) (G : WeightedLedgerGraph n)
113 (hCal : CalibratedAgainstGraph D a ha hinges G) :
114 ReggeDeficitLinearizationHypothesis D a ha hinges G :=
proof body
Tactic-mode proof.
115 (calibrated_iff_hypothesis D a ha hinges G).mp hCal
116
117/-- The cubic lattice is calibrated against every weighted ledger graph,
118 by Phase A. -/