FreudenthalAxisDisp0ExplicitFiberClosedFormTarget_false
plain-language theorem explainer
On the N=5 periodic Freudenthal torus witness with axis-displacement-0 endpoint unit data, the closed-form explicit-fiber mixed hinge-deficit target fails. Gravity and discrete-Regge workers cite this as a concrete negative instance blocking that closed-form route. The proof is a short term reduction: closed form implies the flat-unfolded target, already known false at the same witness.
Claim. For lattice sizes $N_x = N_y = N_z = 5$ (with the standard bounds $2 < N_i$), the closed-form explicit-fiber mixed hinge-deficit identity does not hold: it is not true that for every vertex potential $\xi$ and every periodic edge $e$, the hinge directional derivative times the negative sum of closed-form expanded fiber pair summands equals $\sqrt{\mathrm{periodicDispSq}(e)}$ times the corresponding right-hand side.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not grant the physical Dirichlet equality for free; each target Prop is a concrete identity that must be proved or refuted on chosen witnesses.
The closed-form explicit-fiber mixed target asserts a pointwise edge identity: the hinge-measure directional derivative of a vertex potential, multiplied by a fiber sum built entrywise from the closed-form expanded pair summand, matches a geometric factor $\sqrt{\mathrm{periodicDispSq}}$ times the model right-hand side. The witness used here is the axis-displacement-0 endpoint-unit configuration at $N=5$ in each direction (with the trivial bounds $2<5$).
Upstream, a one-way implication already shows that any closed-form success yields the weaker flat-unfolded explicit-fiber target. Separately, that flat-unfolded target is known to fail on the same $N=5$ axis-disp-0 witness by direct evaluation against a global fiber-sum identity.
proof idea
Term-mode reductio. Assume the closed-form target at the $N=5$ axis-disp-0 witness. Apply the implication lemma that closed form yields the flat-unfolded explicit-fiber mixed target on the same parameters. Feed that conclusion into the already-proved negation of the flat-unfolded target at this witness, obtaining a contradiction. Hence the closed-form target is false.
why it matters
Negative control inside the physical six-tet cubic Dirichlet instantiation path. Downstream, the local edge-stencil correspondence theorem at $N=5$ uses this negation: if one assumed the closed-form explicit-fiber target, one would derive a false local correspondence statement, so that route is blocked.
In the broader gravity stack (periodic Freudenthal torus, Regge cubic lattice limit, length-chain endpoint certificates), this pins that the closed-form fiber expansion does not automatically discharge the mixed hinge-deficit identity on the standard small periodic witness. It forces either a different fiber presentation, a restricted class of potentials/edges, or a non-closed-form proof strategy before the physical Dirichlet model can be certified on this scaffold.
No T0–T8 forcing step is settled here; the result is local discrete-geometry bookkeeping that keeps the Dirichlet instantiation honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.