FreudenthalAxisDisp0GlobalEndpointUnitFiberSumTarget
plain-language theorem explainer
Packages the proposition that the closed-form Freudenthal fiber sum, evaluated on the axis witness edge at the endpoint-unit potential with displacement class 0, equals -4. Gravity and Regge-lattice workers cite it as the global numerical target for the axis-disp-0 audit. It is a pure Prop abbreviation, not a proved equality.
Claim. The closed-form fiber sum of the canonical encoded periodic Freudenthal torus, taken at the axis witness edge (base $(1,0,0)$, displacement $0$) with the endpoint-unit vertex potential and positive displacement class $0$, equals $-4$.
background
This module wires the encoded periodic Freudenthal torus into the physical six-tet cubic Dirichlet model. It does not free-assert the Dirichlet equality; it packages the exact obligations needed to instantiate that model on a periodic Freudenthal scaffold.
The closed-form fiber sum is the explicit real-valued sum over one positive displacement class of the torus edge data. The axis witness edge is the concrete periodic edge with base $(1,0,0)$ and displacement $0$. The endpoint-unit potential is the vertex potential that is unit on the designated axis endpoints of that witness and (by construction) zero elsewhere in the relevant support.
Witness size hypotheses $2 < N_x, N_y, N_z$ fix a concrete finite torus large enough for the local stencil. The target Prop simply records the global numerical claim that this fiber sum equals $-4$ at that configuration.
proof idea
No proof: this is a def equating a Prop to the literal equality
freudenthalExplicitFiberClosedFormFiberSum ... axisWitnessEndpointUnitPotential axisWitnessEdge 0 = (-4 : ℝ).
Discharge is deferred to sibling theorems such as ..._of_local_and_audit (rewrite global sum to local audit, then apply the certified local value) and the one-line wrapper ..._holds.
why it matters
This target is the global numerical anchor for the axis-disp-0 fiber audit on the physical six-tet cubic Dirichlet instance. Downstream, FreudenthalAxisDisp0GlobalEndpointUnitFiberSumTarget_holds asserts it, via reduction through local-equality and local-audit lemmas.
It is the hypothesis that kills inconsistent templates: FreudenthalExplicitFiberBilinearEndpointTemplateTarget_false_at_disp0 shows the bilinear endpoint template cannot hold once the fiber sum is $-4$, and FreudenthalAxisDisp0ExplicitFiberFlatUnfoldedTarget_false uses the certified sum to refute the flat unfolded mixed-hinge deficit target on the same witness.
In the broader gravity chain this sits under the Regge cubic lattice limit and Freudenthal length-chain endpoint certificates: a concrete, checkable fiber value that any candidate Dirichlet or hinge-aware action on the periodic torus must match before the physical model instance is accepted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.