w8_from_eight_tick
plain-language theorem explainer
Supplies the parameter-free closed-form expression for the canonical gap weight w₈ as the normalized projection onto the fundamental 8-tick basis. Researchers deriving the single gap term in the alpha pipeline or verifying numerics in the Recognition Science constants would cite this definition. The value is introduced directly as an explicit algebraic combination of the golden ratio phi and sqrt(2) without auxiliary hypotheses.
Claim. The gap weight is given by the closed-form expression $w_8 = (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7$, where phi is the golden ratio. This supplies the normalized projection weight of the gap onto the 8-tick basis for use in the alpha pipeline.
background
The GapWeight module defines the single gap term in the alpha pipeline as f_gap = w₈ ln(phi). The eight-tick basis is the fundamental period of length 2^3 in the forcing chain. This definition replaces prior numeric certificates to enforce the no-free-parameters requirement, presenting w₈ as the normalized DFT-8 neutral spectral deficit weight of the canonical phi-pattern (distinct from the raw DFT sum).
proof idea
This is a direct definition that states the closed-form expression without invoking lemmas or tactics. The body simply evaluates the algebraic combination of rational coefficients, sqrt(2), and phi, then divides by 7.
why it matters
This definition feeds f_gap, gap_weight_approx, w8_pos, and eight_tick_neutral_implies_exact. It fills the parameter-free requirement for the gap term in the alpha pipeline and aligns with the eight-tick octave (T7) in the unified forcing chain. It touches the open reconciliation between the DFT candidate and the required projection step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.