EdgeLengthFromPsiCert
plain-language theorem explainer
EdgeLengthFromPsiCert packages the bridge equality between discrete J-cost Laplacian action and linearized Regge sum, conditioned on the deficit linearization hypothesis, together with three flat-space identities. Discrete-gravity researchers in the Recognition framework cite it to certify that the Einstein coupling is derived from J-cost calibration rather than fitted. The structure is assembled directly from the field-curvature identity lemma and the flat-action lemmas.
Claim. Let $D$ be a deficit-angle functional, $a>0$ a scale, hinges a list of hinge data, $G$ a weighted graph, and $h$ the Regge deficit linearization hypothesis for these data. The certificate requires that the Laplacian action on any log-potential field $ε$ equals $(1/κ)$ times the Regge sum on the conformal edge-length field $L(ε)$ with $L_e = a·exp((ε_i+ε_j)/2)$, where $κ=8φ^5$. It further requires that the Regge sum vanishes at $ε≡0$, the Laplacian action vanishes at $ε≡0$, and the log-potential of the constant field $ψ≡1$ is identically zero.
background
In the Recognition Science setting a recognition potential $ψ$ on graph vertices is converted to a log-potential $ε_i=ln ψ_i$. The Laplacian action is the quadratic Dirichlet form $(1/2)∑{i,j} w{ij}(ε_i-ε_j)^2$ on a weighted graph. A HingeDatum records the edges meeting at a hinge together with nonnegative weights; a DeficitAngleFunctional supplies, for any edge-length field, both an area and a deficit angle at each hinge. The Regge sum is then the weighted sum of these deficits. The conformal edge-length field is defined by the ansatz $L_e=a·exp((ε_i+ε_j)/2)$, recovering the flat length $a$ when $ε≡0$. The ReggeDeficitLinearizationHypothesis asserts that the Regge sum on these lengths equals $κ$ times the Laplacian action at leading order. Upstream, jcost_to_regge_factor is defined as $8φ^5$ because “J''(1)=1 (the calibration axiom A3), and the Regge action has normalization 1/κ”.
proof idea
The declaration is a structure definition. Its bridge field is populated by the field-curvature identity under linearization lemma. The flat_regge field is populated by the regge sum flat under linearization lemma. The flat_jcost field is populated by the laplacian action flat lemma. The psi_flat field follows directly from the definition of logPotentialOf on the constant field. No additional tactics are used.
why it matters
This certificate isolates the linearization hypothesis so that the bridge from J-cost to Regge action becomes a genuine theorem rather than a definitional tautology. It feeds the parent theorem edgeLengthFromPsiCert that constructs an instance of the certificate. In the Gravity from Recognition draft it discharges the field-curvature identity (Theorem 5.1) modulo the linearization step, confirming that κ is derived from the J-cost second derivative at unity. The construction uses the explicit value κ=8φ^5 but does not invoke the full forcing chain or the eight-tick octave beyond that constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.