CanonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEndpointTarget
plain-language theorem explainer
Defines the typed-endpoint obligation for the expanded mixed hinge-deficit identity on a canonical periodic Freudenthal torus of size (Nx,Ny,Nz) with each side >2. For every vertex potential and every periodic edge, the hinge directional derivative times the Schläfli-weighted length-chain sum must equal the Euclidean edge length times the squared potential jump at the typed endpoints. Gravity workers cite it when packaging Dirichlet-model hypotheses. The body is a pure Prop abbreviation, not a proof.
Claim. Fix lattice sizes $N_x,N_y,N_z\ge 1$ with each $N_i>2$, and let $P$ be the canonical encoded periodic Freudenthal torus of that size. The typed-endpoint expanded mixed target asserts: for every vertex potential $\xi$ on $P$ and every periodic edge $e$ with displacement $\mathrm{disp}(e)$ and endpoints $(v_1,v_2)$, $$\partial_{\mathrm{hinge}}(\xi,e)\cdot\Bigl(-\sum_{\tau}\sum_{k}\mathbf{1}_{e\in\tau}\,\partial_{\mathrm{dih}}(\tau,f,k)\,\partial_{\ell}(\xi,\tau,k)\Bigr)=\sqrt{|\mathrm{disp}(e)|^2}\,(\xi(v_1)-\xi(v_2))^2.$$
background
This module packages the exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not free-assert the physical Dirichlet equality; it only names the residual identities.
The geometric scaffold is the canonical encoded periodic Freudenthal torus: a 3-torus triangulation built from the six-tetrahedron Freudenthal cube, with incidence maps edgeInTet / localEdgeOf sending global edges to local tet slots (Fin 6). Vertex potentials are real assignments on the torus vertices. The left-hand side is the mixed hinge-deficit expansion: hinge measure directional derivative times a Schläfli chain of dihedral derivatives against local edge-length derivatives. The right-hand side is written from the typed periodic edge (displacement vector and two endpoints), not from an abstract edge index.
Upstream geometry supplies the incidence tables and the periodic edge type; the dimensionless bridge constant $K=\varphi^{1/2}$ appears only as part of the ambient complex data, not in this Prop itself.
proof idea
Definitional abbreviation, not a proved theorem. The body binds $P$ to the canonical encoded periodic Freudenthal torus, then states a universal quantification over vertex potentials and periodic edges. For each edge it pulls back via the torus edge equivalence, multiplies the hinge directional derivative by the negated double sum over tets and local slots (zero when the edge is absent from the tet, otherwise Schläfli dihedral derivative times local length derivative), and equates that product to $\sqrt{\mathrm{periodicDispSqEdge}(\mathrm{disp})}$ times the squared potential difference at the two typed endpoints. No tactics or lemmas are applied.
why it matters
This Prop is the typed-endpoint packaging of the expanded mixed hinge-deficit length-chain identity that the physical six-tet cubic Dirichlet instance needs on the periodic Freudenthal scaffold. Downstream, conversion lemmas move between typed-slot, explicit-fiber, typed-edge, and typed-endpoint forms of the same target, and the local-correspondence theorems consume the typed-endpoint hypothesis (including a finite-$N=5$ obstruction witness and the positive correspondence under a weighted-deficit vanishing hypothesis).
In the Recognition gravity stack this sits between the Regge/Freudenthal geometry layer and the physical Dirichlet action target: it is one of the exact residual obligations that must hold before the discrete hinge action can be identified with a finite-difference Dirichlet energy on the cubic lattice. It does not itself close the continuum or curvature limits; it only names the finite-complex identity in endpoint language convenient for later stencil correspondence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.