cubic_linearization_discharge
This theorem shows that the Regge deficit linearization hypothesis holds exactly for the cubic deficit functional on any weighted ledger graph G. Researchers formalizing the continuum limit of the Recognition Science ledger cite it to justify the leading-order identity in the field-curvature theorem. The proof is a term-mode reduction that rewrites the Regge sum via hinge summation, applies the Laplacian action identity, and closes by ring.
claimFor any natural number $n$, real $a>0$, and weighted ledger graph $G$, the Regge deficit linearization hypothesis holds for the cubic deficit functional on $n$, the scale $a$, the list of hinges extracted from $G$, and the graph $G$.
background
The module CubicDeficitDischarge supplies the cubic-lattice case of the linearization step. A weighted ledger graph $G$ is a structure carrying a symmetric nonnegative weight function on pairs of vertices in Fin $n$. The cubic deficit functional assembles the quadratic deficit at each hinge from the squared log-potential difference together with an area term proportional to the edge weight.
proof idea
The proof is a term-mode script. It introduces the log-potential field, rewrites the Regge sum by the lemma regge_sum_cubicHinges, rewrites the Laplacian action by laplacian_action_as_prod_sum, and closes the resulting equality by the ring tactic.
why it matters in Recognition Science
This declaration discharges the ReggeDeficitLinearizationHypothesis for the cubic presentation and is invoked directly by bridge_chain_complete and continuumFieldCurvatureCert. It realizes the linearization step of the paper's Theorem 5.1 on the cubic lattice. In the Recognition framework it equates the J-cost Dirichlet energy to the leading-order Regge sum, supporting the passage from the discrete ledger to the continuum Einstein equations while higher-order corrections are deferred to later phases.
scope and limits
- Does not establish the hypothesis for non-cubic deficit functionals.
- Does not incorporate O(ε³) corrections to the full Regge deficit.
- Does not derive the Einstein coupling from the Recognition constants.
- Does not prove convergence of the discrete sums to continuum integrals.
Lean usage
cubic_linearization_discharge a ha Gformal statement (Lean)
277theorem cubic_linearization_discharge {n : ℕ} (a : ℝ) (ha : 0 < a)
278 (G : WeightedLedgerGraph n) :
279 ReggeDeficitLinearizationHypothesis
280 (cubicDeficitFunctional n) a ha (cubicHinges G) G := by
proof body
Term-mode proof.
281 intro ε
282 rw [regge_sum_cubicHinges a ha ε G, laplacian_action_as_prod_sum G ε]
283 ring
284
285/-! ## §9. The paper's Theorem 5.1 on the cubic lattice -/
286
287/-- **THE FIELD-CURVATURE IDENTITY (cubic lattice).** -/