seedFlat_eq_cast
plain-language theorem explainer
For each of the ten local edge slots, the flat Freudenthal squared length equals the corresponding natural mask weight cast to a real. Anyone matching the seed-hinge edge vector to the incidence layer's XOR bit counts cites this. The proof is exhaustive case split on Fin 10 with numeric unfolding of both tables.
Claim. For every local edge index $e \in \{0,\ldots,9\}$, the flat squared edge length $\ell^2_{\mathrm{flat}}(e)$ equals the natural mask value $m(e)$ viewed as a real number: $\ell^2_{\mathrm{flat}}(e) = (m(e):\mathbb{R})$.
background
This module builds the Regge 4D seed-hinge dihedral cosine kernel at the flat Freudenthal point, the next kernel-checked step after the flat kernel. Scope is the seed triangle hinge inside its two seed-cell 4-simplices only; the full lattice orbit sum remains open.
The ten local squared edge lengths live in slot order fixed by the incidence layer. At flat, both seed simplices share one squared-edge vector seedFlatSqEdges, with values $(1,2,3,4,1,2,3,1,2,1)$. The companion seedFlatMaskNat is the same table as naturals, intended for decidable comparison with bit weights of XOR masks: unit Freudenthal steps flip one axis each, so flat squared length is the number of set bits of the incidence mask.
Casting $\mathbb{N}\to\mathbb{R}$ is the only bridge needed before proving those mask weights agree with the geometric edge vector on each seed simplex.
proof idea
Tactic proof by exhaustive cases on $e:\mathrm{Fin},10$. After fin_cases e, each goal is a concrete equality of a real literal from seedFlatSqEdges with the cast of the matching natural from seedFlatMaskNat. norm_num unfolds both definitions and closes the arithmetic. No external lemmas beyond the two table definitions.
why it matters
This cast lemma is the rewrite hinge for the two agreement theorems seedFlatSqEdges_simplex0 and seedFlatSqEdges_simplex1. Those state that flat local squared lengths equal bit weights of the incidence layer's edge masks on seed simplices 0 and 1; each proof rewrites via this equality then discharges the $\mathbb{N}$ identity by decide.
In the QG campaign this pins the flat edge vector to the Freudenthal incidence layer without redefining that API, which is required before the Gram-projection cosine, the flat value $\cos=1/\sqrt{2}$, and the ten coordinate derivatives of the dihedral kernel. It does not itself touch the eight-tick octave or $D=3$ forcing; it is local discrete-geometry bookkeeping inside the 4D Regge hinge analysis. Downstream still leaves open the full lattice orbit sum, the flat Hessian of the 4D Regge action, and S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.