canonicalPeriodicMixedHingeDeficitExpandedLengthChainTypedEdgeTarget_of_typedEndpoint
plain-language theorem explainer
If the expanded mixed hinge-deficit identity holds in typed endpoint form on the canonical periodic Freudenthal torus, then it holds in typed periodic-edge form. Gravity workers packaging the six-tet cubic Dirichlet instance cite this to drop anonymous Fin edge indices. The proof is a short transport: unfold both targets, cancel the edgeFinEquiv round-trip on squared lengths, and apply the endpoint hypothesis.
Claim. Let $N_x,N_y,N_z\ge 3$. Write $P$ for the canonical encoded periodic Freudenthal torus of size $(N_x,N_y,N_z)$. If for every vertex potential $\xi$ and every periodic edge $e$ the expanded mixed hinge-deficit length-chain identity holds when edges are presented by typed endpoints and displacements, then the same identity holds when edges are presented as typed periodic edges (via $P$'s edge equivalence).
background
This module packages the exact obligations needed to instantiate PhysicalSixTetCubicDirichletModel on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
The canonical object $P$ is canonicalEncodedPeriodicFreudenthalTorus, built from the endpoint-incidence data of the periodic triangulation (sizes strictly larger than 2). Edges may be indexed anonymously as Fin nE, as typed PeriodicEdge values, or via endpoint pairs; canonicalPeriodicEdgeEquiv and canonicalEdgeVerts mediate those presentations. Squared edge lengths come from the Freudenthal globalSqEdge tables (axis edges length squared 1, face diagonals 2, etc.), specialized on the torus to periodicDispSqEdge of the edge displacement.
The two Props compared here are the expanded per-edge mixed targets: both assert that the hinge-measure directional derivative of a vertex potential, times a signed sum of tetrahedron contributions along edges incident to a hinge, matches an expanded length-chain expression. The endpoint variant writes the RHS from typed displacements and endpoints; the edge variant removes the anonymous Fin nE index and quantifies over PeriodicEdge directly.
proof idea
Fix $P$ as the canonical encoded periodic Freudenthal torus. For arbitrary potential $\xi$ and periodic edge, prove a one-line squared-length identity: the global squared length of the edge obtained by transporting through edgeFinEquiv.symm equals periodicDispSqEdge of the edge's displacement. That identity is just apply_symm_apply of the edge equivalence, rewritten under periodicDispSqEdge.
Then simpa unfolds both target Props and the canonical torus constructors (_of_endpoint, _of_incidence, edge equiv, triangulation, canonicalGlobalSqEdge, canonicalEdgeVerts), inserts the squared-length fact, and discharges the goal from the typed-endpoint hypothesis applied to the same $\xi$ and edge.
why it matters
This is a presentation bridge inside the gravity Dirichlet pipeline. Downstream, canonicalPeriodicEdgeStencilLocalCorrespondence_of_canonicalDeficitTypedEndpointTargets and canonicalPeriodicEdgeStencilLocalCorrespondence_of_stationary_and_cellTetTargets need the mixed deficit target in typed-edge form to state local stencil correspondence on the canonical torus (eventual-zero or weaker weighted-stationary Schläfli input).
In the broader RS gravity story, the six-tet cubic Freudenthal complex is the discrete geometry underlying the physical finite-difference Dirichlet action. Cleaning edge indexing so the expanded hinge-deficit identity is stated on PeriodicEdge rather than raw Fin indices is bookkeeping, but it is required bookkeeping before the stencil-local correspondence theorems can feed the physical model instance. No forcing-chain landmark (T5–T8) is touched directly; the result is pure discrete-geometry hygiene on the periodic lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.