CanonicalPeriodicMixedHingeDeficitExplicitFiberClosedFormTarget
plain-language theorem explainer
Defines the closed-form explicit-fiber mixed hinge-deficit target on the canonical periodic Freudenthal torus: for every vertex potential and every positive-displacement edge, the hinge-measure directional derivative times a negated fiber sum of closed-form pair summands equals edge length times the squared potential jump. Gravity and Regge-lattice workers cite it as the Prop that intermediate closed-form lemmas discharge. The body is a pure Prop packaging, not a proof.
Claim. For lattice sizes $N_x,N_y,N_z>2$, let $P$ be the canonical encoded periodic Freudenthal torus. The target asserts: for every vertex potential $\xi$ on $P$ and every positive-displacement periodic edge $e$, $$(\partial_{\mathrm{hinge}}\xi)(e)\cdot\Bigl(-\sum_{\mathrm{pairs\ in\ fiber}} S^{\mathrm{cl}}(\xi,e,\mathrm{pair})\Bigr)=\sqrt{\ell(e)^2}\,\bigl(\xi(v_1)-\xi(v_2)\bigr)^2,$$ where $S^{\mathrm{cl}}$ is the closed-form expanded fiber-pair summand and $\ell(e)^2$ depends only on the displacement class.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not free the physical Dirichlet equality; it names the intermediate targets that must be proved.
The ambient geometry is the canonical encoded periodic Freudenthal torus $P$ on an $N_x\times N_y\times N_z$ lattice with each side larger than 2. Edges are positive-displacement periodic edges (base vertex plus one of seven cube displacements). Squared edge length is read from the displacement class alone (values 1, 1, 1, 2, 2, ...). Vertices are indexed by the canonical finite equivalence vertexFinEquiv.
A vertex potential is a real function on the finite vertex set of $P$. The left-hand side multiplies the hinge-measure directional derivative of that potential along the edge by a negated sum over the local pair-displacement fiber; each summand is the closed-form expanded fiber-pair expression. The right-hand side is the geometric edge length times the squared jump of the potential between the two endpoints.
proof idea
Definition only: the body is a let-bound universal Prop. It fixes $P$ as the canonical encoded periodic Freudenthal torus, then quantifies over vertex potentials and periodic edges, equating the product of the hinge-measure directional derivative with the negated closed-form fiber sum to length times squared endpoint jump. No tactics or lemmas are applied; discharge happens in downstream theorems that take this Prop as a hypothesis or conclusion.
why it matters
This Prop is the closed-form explicit-fiber mixed target that several discharge and correspondence lemmas in the same module hang on. Downstream results include: the all-bilinear and flat-unfolded routes into this target; the per-displacement specialization; the lift from this target to the per-disp closed-form target; the edge-stencil local correspondence assembled from the family of closed-form deficit targets; and a negative witness at the $N=5$ axis-displacement unit that this target alone does not force local correspondence.
In the broader gravity stack it sits between the encoded periodic Freudenthal scaffold and the physical six-tet cubic Dirichlet model, so it is one of the named obligations that must close before the discrete Regge/Dirichlet action on the torus is identified with the continuum target. It does not itself touch T0–T8 or the RCL; it is lattice-geometry scaffolding for the gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.