classDisp_axis0
plain-language theorem explainer
The zeroth Freudenthal edge class on the 4-cube is exactly the unit axis displacement along coordinate 0. Anyone wiring the 15-class stencil back to the TT attachment layer cites this identity. The proof is a four-case bit-mask check: mask 1 has only bit 0 set, matching the axis vector.
Claim. The displacement vector of edge class $0$ (mask $1$) equals the unit axis displacement $e_0$ on $\mathbb{R}^4$: $\mathrm{classDisp}(0) = e_0$, i.e. the map $i \mapsto 1$ if $i=0$ and $0$ otherwise.
background
This module packages the 4D Regge edge stencil after the TT attachment layer: fifteen nonzero Freudenthal-style classes of $0/1$ displacements in ${0,1}^4$, indexed by Fin 15 via bit masks $d.val+1 \in {1,\ldots,15}$.
maskOf d is that integer mask. classBit d i is whether bit $i$ of the mask is set. classDisp d is the corresponding displacement in $\mathbb{R}^4$ with entries in ${0,1}$. From the attachment module, axisDisp a is the standard unit vector along axis $a$.
Class $0$ has mask $1 = 2^0$, so only coordinate $0$ is live. The claim is the dictionary entry that recovers the attachment-layer axis vector from the class packaging.
proof idea
Pointwise equality of functions Fin 4 → ℝ. Apply function extensionality, then case-split on the four coordinates. Each case reduces by unfolding classDisp, classBit, maskOf, and axisDisp, together with Nat.testBit on mask $1$: only bit $0$ is set, so the values match $e_0$ on every coordinate.
why it matters
Opens §8 of the module: axis classes recover the attachment layer. Downstream, classCoeff_axis0 rewrites the class quadratic load on class $0$ as the attachment edgeLoad on axisDisp 0, and planeWaveClassPert_axis0 identifies the plane-wave midpoint perturbation on class $0$ with the axis-edge perturbation.
In the QG campaign this is a small but necessary bridge between the 15-class Freudenthal packaging and the earlier 4D TT attachment (ReggeEdgeTTAttachment4D). It does not touch true Regge Hessian weights (still OPEN), nor S_RS_converges_EH_4d, nor full edge_tt_decomposition. It only pins the axis-0 dictionary entry used by the provisional finite quadratic and its nonvacuity checks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.