FreudenthalExplicitFiberEndpointDependenceTarget
plain-language theorem explainer
For a fixed positive cube displacement on a periodic Freudenthal torus of size greater than two in each direction, the closed-form explicit-fiber sum is asserted to depend only on the two endpoint vertex potentials. Discrete gravity workers cite this target when wiring the bilinear endpoint template into the physical six-tet cubic Dirichlet model. The body is an existence Prop: some bivariate real map F recovers the fiber sum from the two endpoint values alone.
Claim. For integers $N_x, N_y, N_z > 2$ and a fixed positive cube displacement class $d$, there exists $F:\mathbb{R}\times\mathbb{R}\to\mathbb{R}$ such that, for every real vertex potential $\xi$ on the canonical encoded periodic Freudenthal torus and every periodic edge $e$ of displacement $d$, the closed-form explicit-fiber sum of $\xi$ along $e$ equals $F(\xi(v_0),\xi(v_1))$, where $v_0$ and $v_1$ are the two endpoints of $e$.
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 assert the physical Dirichlet equality for free; it only records the intermediate targets.
A periodic edge is a positive-displacement edge on the torus, given by a base vertex and one of seven positive cube displacements. Vertices are indexed by a canonical finite equivalence. A vertex potential assigns a real value to each torus vertex (the underlying scale uses the dimensionless bridge ratio $K=\varphi^{1/2}$). The closed-form explicit-fiber sum is the length-chain contribution associated to one such edge and displacement class.
Because that sum is $\mathbb{R}$-linear in the vertex potential, endpoint-only dependence is equivalent to vanishing of all coefficients on non-endpoint vertices in the linear expansion. The doc-comment flags a finite coefficient audit (Python script) that finds nonzero non-endpoint coefficients for axis and face-diagonal classes, so the target is load-bearing but not yet discharged for every $d$.
proof idea
This declaration is a Prop definition, not a proved theorem. Its body asserts existence of a single bivariate real function $F$ that, for the fixed displacement class $d$, reproduces the closed-form explicit-fiber sum from the two endpoint potentials of any edge of that class. No tactics or lemmas are applied; the definition simply packages the combinatorial claim that the fiber sum factors through the two endpoints.
why it matters
This target is the load-bearing combinatorial step for the bilinear endpoint template on the physical six-tet cubic Dirichlet instance. Downstream, uniform affine endpoint coefficients imply the target with $F(\xi_0,\xi_1)=c_0\xi_0+c_1\xi_1$ (and the global $F$ is sharp: per-edge auxiliary zeros are not enough unless the pair $(c_0,c_1)$ is constant on the class). A bilinear endpoint template likewise yields it by projecting to the fiber-sum clause. A companion vertex-coefficient expansion target records the honest linear form before any endpoint-only ansatz.
In the Recognition gravity stack this sits between the encoded periodic Freudenthal torus scaffold and the physical Dirichlet model: without endpoint dependence, the length-chain sum cannot collapse to a two-point stencil. The doc-comment notes that a finite audit finds nonzero non-endpoint coefficients for axis and face-diagonal classes; the remaining work is a Lean certificate of those cancellations, or a revised target. It does not itself touch the T0--T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.