projectionScale_eq
plain-language theorem explainer
The projection scale that turns a dimensionless spectral fraction into a per-cell weight equals 64. Anyone normalizing gap weights on the eight-tick, eight-vertex RS cell cites this identity. The proof is a one-line simp that unfolds the definition and applies the cell-cardinality lemma N_cell = 64.
Claim. The projection scale equals $64$: if $N_{\mathrm{cell}}$ is the cardinality of the fundamental cell index set (ticks $\times$ vertices) and the projection scale is the real embedding of $N_{\mathrm{cell}}$, then that scale is exactly $64$.
background
The GapWeight.Projection module fixes two historically implicit choices in Recognition Science weight bookkeeping: the spectral factor $\sin^2(\pi k/8)$ from the discrete Laplacian on the 8-tick cyclic shift, and the normalization denominator that converts a scale-invariant fraction into a per-cell integrated weight.
The fundamental RS interface cell is the product of the eight-tick octave clock with the eight vertices of the $Q_3$ spatial cell, so its index set has cardinality $8\times 8=64$. The sibling lemma records $N_{\mathrm{cell}}=64$ by deciding the finite cardinality of $\mathrm{Fin},8\times\mathrm{Fin},8$. The projection scale is defined simply as the real number underlying that cardinality: $\mathrm{projectionScale}:=(N_{\mathrm{cell}}:\mathbb{R})$.
This sits in the constants layer that feeds gap-weight and $\alpha$-calibration constructions; the eight-tick structure is the T7 landmark of the forcing chain.
proof idea
One-line wrapper. Unfold the definition of the projection scale (it is the real cast of $N_{\mathrm{cell}}$) and rewrite with the already-proved sibling $N_{\mathrm{cell}}=64$. The simp call discharges the equality immediately; no further arithmetic is needed.
why it matters
Claim hygiene for the gap-weight pipeline: without an explicit scale, the conversion from a dimensionless DFT energy fraction into a per-cell weight would hide a free constant. Fixing that constant at $64=8\times 8$ ties the normalization to the T7 eight-tick octave and the eight-vertex $Q_3$ cell, so there is no residual operator/measure degree of freedom.
The module frames this as closing the “weights + normalization” ambiguity. Downstream consumers (projected $w_8$ weights, $\varphi$-pattern DFT energy totals in the same file) can now cite a single simp-normal form rather than re-deriving the cell count. No parent theorems are recorded yet in the use graph; the lemma is infrastructure waiting on weight-assembly proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.