ReggeDeficitLinearizationHypothesis
plain-language theorem explainer
ReggeDeficitLinearizationHypothesis asserts that the Regge sum of areas times deficit angles, evaluated on the conformal edge-length field from scale a and log-potential ε, equals jcost_to_regge_factor times the Laplacian action of weighted graph G. Derivations of the field-curvature identity in Recognition Science gravity cite it to obtain a non-tautological match between J-cost Dirichlet energy and linearized Regge action. The declaration is a direct definition of the Prop as the universal quantification over ε of that algebraic equality.
Claim. For deficit-angle functional $D$, scale $a>0$, hinge list, and weighted ledger graph $G$, the hypothesis states that for every log-potential field $ε$, the Regge sum $∑_h A_h δ_h(L(a,ε))$ equals $8φ^5$ times the Laplacian action of $G$ on $ε$, where $L(a,ε)$ is the conformal edge-length field and the Laplacian action is the associated Dirichlet energy.
background
This module supplies the missing map from scalar recognition potential on simplices to edge lengths together with the linearization rule that converts deficit angles into differences of log-potentials. DeficitAngleFunctional is the structure that, given an edge-length field, returns both the deficit angle and the area at each hinge; HingeDatum records the edges meeting at a hinge and their nonnegative geometric weights. The local theoretical setting is the Gravity from Recognition draft Theorem 5.1, which requires the J-cost Dirichlet energy to match the linearized Regge action with coupling $κ=8φ^5$ without defining one side to be a multiple of the other.
proof idea
The declaration is a one-line wrapper that directly defines the Prop as the statement ∀ε, regge_sum D (conformal_edge_length_field a ha ε) hinges = jcost_to_regge_factor * laplacian_action G ε. No tactics or lemmas are applied inside the definition itself; the algebraic content is supplied by downstream discharge theorems such as cubic_linearization_discharge.
why it matters
This hypothesis supplies the genuine physical content for the field-curvature identity that ContinuumBridge only obtains tautologically. It is discharged unconditionally for cubic lattices in cubic_linearization_discharge, which feeds directly into ContinuumFieldCurvatureCert and bridge_chain_complete; the latter completes the chain from RCL through J-uniqueness and φ-forcing to the Einstein coupling. The module doc notes that general discharge remains open and is expected via Piran–Williams or Cheeger–Müller–Schrader convergence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.