in

In the α pipeline the single gap term is $f_{\mathrm{gap}}=w_8\ln\varphi$. Historically $w_8$ sat as a numeric certificate; the module replaces that by a parameter-free closed form forced by the 8-tick octave (T7) and the φ-ladder (T6).

The geometric mode weight on $\mathbb{Z}/8$ is $g_k=\sin^2(k\pi/8),\varphi^{-k}$ for $k\neq 0$ (zero at DC): the $\sin^2$ factor is the spectrum of the discrete derivative $(S-I)$ on the cycle, and $\varphi^{-k}$ is the conjugate ladder envelope of the pattern $\varphi^t$. The unnormalized DFT candidate sums $A_k g_k$ over nonzero modes. The projected weight multiplies the ratio of that sum to the Parseval total energy by the 64-cell scale $|\mathrm{Fin},8\times\mathrm{Fin},8|$, coming from eight ticks times the $2^3$ cube vertices.

The closed form $(348+210\sqrt{2}-(204+130\sqrt{2})\varphi)/7$ is the target canonical value (numerically $\approx 2.49056927545$). The integers are not fitted: they are forced by the DFT closed form, Parseval, and the cell scale.

Scaffolded closure, five algebraic stages (not yet discharged in-tree as a zero-sorry proof).

1. For each mode $k=1..7$, unfold the geometric weight, drop the $k=0$ branch by decide, normalize Fin.val casts, and simplify with the explicit $\sin^2(k\pi/8)$ values.
2. For four rational pairs $T_i\cdot\mathrm{coeff}$, clear denominators by div_mul_eq_mul_div, div_eq_iff, and ring.
3. A helper shows the projection sum times $4 D_1 D_2 D_3 D_4$ equals a numerator polynomial, by distributing and combining the four pair identities.
4. Reduce the main identity with $\varphi^8-1$ and $\varphi^8+1$ factorizations and div_eq_div_iff; cancel the nonzero coefficient after converting divisions to multiplications via the helper.
5. The remaining polynomial identity in $(\varphi,\sqrt{2})$ is closed by linear_combination against the certificate $q_\varphi\cdot(\varphi^2-\varphi-1)+q_s\cdot((\sqrt{2})^2-2)$, with $q_\varphi,q_s$ from the SymPy Groebner script compute_w8_certificate.py.

This identity is what makes $w_8$ admissible under the no-free-parameters claim. Downstream the α pipeline consumes $f_{\mathrm{gap}}=w_8\ln\varphi$; without equality of the projected weight to the closed form, the gap term would still be a numeric insert.

Framework landmarks: T7 forces the eight-tick window and the DFT-8; T6 forces the φ-pattern and conjugate envelope; $D=3$ forces $2^3=8$ cube vertices, hence the 64-cell scale. The attacker breadcrumb in the module doc is the point of the theorem: the integers 348, 210, 204, 130, 7 look fitted to CODATA if one skips the chain, but they are the output of geometric-series DFT sums, Parseval, and cell scaling.

A separate mismatch certificate shows the unnormalized DFT sum is not equal to the closed form. That is a sanity check blocking a common identification error; the canonical object is the Parseval-and-64-cell projected weight, which is what this equality targets. No downstream Lean uses are wired yet (used_by empty), so the declaration is still a scaffold hinge rather than a live lemma in a larger proof.