periodicConformalGeneratorMap5_apply_endpoint
plain-language theorem explainer
On the encoded 5×5×5 periodic Freudenthal torus, the conformal generator map evaluated on any edge equals the arithmetic mean of the two endpoint vertex coefficients. Gravity and discrete-geometry workers cite it when reducing vertex-potential ansatzes to two-point edge support. The proof unfolds the map definitions and simplifies with the endpoint formula plus elementary sum and field algebra.
Claim. Let $T$ be the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus, and let $c$ assign a real coefficient to each encoded vertex of $T$. For every edge $e$ of $T$, the conformal generator map sends $c$ at $e$ to $\bigl(c(v_1)+c(v_2)\bigr)/2$, where $v_1,v_2$ are the two endpoints of $e$ (decoded via the standard vertex equivalence).
background
Track 1.D isolates the tensor/shear sector of weak-field gravity on a discrete lattice. Track 1.B already uses a conformal ansatz: one scalar potential per vertex, with edge-length variations induced by averaging the endpoint potentials. That scalar slice cannot represent pure shear, so it misses transverse-traceless gravitational-wave modes. This module separates independent edge perturbations from vertex-conformal ones and records elementary obstructions (e.g. rectangle non-conformality).
The ambient geometry is the canonical encoded $5\times 5\times 5$ periodic Freudenthal torus (PeriodicTorus5), with edges PeriodicEdge5. The conformal generator map packages the vertex-potential ansatz as a linear map from coefficient vectors on vertices to real values on edges. The companion endpoint lemma for the underlying conformal generator states that only the two endpoints of a concrete edge contribute; the present statement lifts that fact to the full generator map used in the Track 1.D payload.
proof idea
Term-mode proof under classical logic. Unfold the definitions of the conformal generator map and the underlying gauge generator map, then simp with the already-proved endpoint evaluation of the conformal generator on a single edge, together with Finset.sum_add_distrib, the rewrite div_eq_mul_inv, and the ring identities mul_add and mul_comm. No case split on edges or vertices is required: after unfolding, the two-point average is exactly what remains.
why it matters
This is a bookkeeping identity inside the Track 1.D tensor/shear scaffold: it makes the two-point support of the conformal ansatz fully explicit on the encoded $5\times 5\times 5$ torus. Downstream shear-versus-conformal comparisons (rectangle obstruction, nontrivial edge perturbations outside the vertex-conformal subspace) rely on knowing that conformal edge values are nothing but endpoint averages. In the broader Recognition gravity program this pins the scalar conformal slice that must be quotiented or complemented before pure shear and TT modes can be isolated. No parent theorem currently lists it as a direct dependency (used_by is empty), so it is infrastructure for the shear-sector development rather than a closed forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.