hingeMeasure_conformal_eq
plain-language theorem explainer
On the canonical periodic Freudenthal torus, the conformal hinge measure at any edge equals the square root of the typed conformal edge-length field built from a vertex potential u. Anyone identifying the frozen-wave Regge action with the true nonlinear action cites this equality. The proof unfolds both sides and rewrites via the canonical edge-vertex and squared-edge lemmas plus elementary sqrt/exp algebra.
Claim. Let $u$ be a real function on the periodic cubic vertices of the $N\times N\times N$ Freudenthal torus, and let $e$ index a global edge of the canonical periodic triangulation. Then the conformal hinge measure of $e$ (square root of the global squared edge length times $\exp((\xi_i+\xi_j)/2)$ for the vertex potential $\xi$ associated to $u$) equals $\sqrt{\ell_e(u)}$, where $\ell(u)$ is the typed conformal edge-squared-length field induced by $u$.
background
This module is Stage 1 of the Regge TT continuum-symbol program: it defines the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, its flat point, and the frozen-model identification that ties the conformal ansatz to that action.
The hinge measure under a vertex-conformal ansatz is the 3D Regge edge length: for incidence-consistent triangulation $K$ and vertex potential $\xi$, edge $e$ with endpoints $i,j$ contributes $\sqrt{\ell_e^{\mathrm{glob}}},\exp((\xi_i+\xi_j)/2)$. The typed conformal edge field is the squared-length field obtained by the same conformal scaling of the lattice's global squared edges. Vertices are the periodic cube $\mathrm{Fin},N^3$; edges are indexed by the canonical finite equivalence edgeFinEquiv.
Upstream stencil preflight supplies the equalities that the canonical edge-vertex pair and global squared edge match the periodic displacement data used by the typed field. The BIT kernel family is imported only as ambient infrastructure and is not used in this identity.
proof idea
Term-mode proof by unfolding. Unfold the conformal hinge measure and the typed conformal edge field. Rewrite the edge endpoints and global squared length via the canonical stencil lemmas canonical_edgeVerts_eq and canonical_globalSqEdge_eq. Then apply $\sqrt{ab}=\sqrt{a}\sqrt{b}$ (using nonnegativity of the periodic displacement squared edge), rewrite $\exp(x/2)$ via half-exponent, and cancel the two toPotential symmetry applications that identify $u$ with the vertex potential on each endpoint. Both sides match.
why it matters
This is the per-edge hinge step of the frozen-model identification. Downstream, reggeAction_conformal_eq sums over edges (via edgeFinEquiv) to prove that the conformal-ansatz Regge action analyzed by the frozen wave equals the true nonlinear Regge action on conformal edge fields: the kernel equation stating which restriction of the true action the frozen model lives on.
In the QG full-theory campaign this closes part of Stage 1 preflight before the open continuum target ReggeTTContinuumIsotropyTarget (TT Bloch symbol isotropic with $K(0)=-(1/4)I_{TT}$). It does not itself touch T0–T8 or the Recognition Composition Law; it is lattice gravity infrastructure that makes the true Regge action and the frozen conformal sector interchangeable on this torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.