gap_weight_unique
plain-language theorem explainer
The theorem asserts uniqueness of the gap weight w₈ as the sole real satisfying the eight-tick minimality condition. Researchers deriving the inverse fine-structure constant from Recognition Science parameters would cite it to fix the value of w₈ without free parameters. The proof is a term-mode construction that instantiates the witness directly from the closed-form definition and discharges uniqueness by reflexivity together with hypothesis substitution.
Claim. There exists a unique real number $w$ such that $w = w_8$, where $w_8 = (348 + 210 sqrt(2) - (204 + 130 sqrt(2)) phi)/7$ and $phi$ is the golden ratio.
background
The module axiomatizes eight-tick window neutrality and its link to ledger exactness via scheduler invariants such as sumFirst8 and observeAvg8. The gap weight w₈ is the normalized projection of the gap onto the fundamental 8-tick basis; its closed form is supplied by the upstream definition w8_from_eight_tick. Upstream results include the derivation of the gap as the product of closure and Fibonacci factors together with the structural conditions from PrimitiveDistinction and SimplicialLedger that underwrite the eight-tick minimality.
proof idea
The proof is a one-line term wrapper. It applies the definition w8_from_eight_tick as the witness for the existential quantifier, then uses constructor to split into existence (discharged by rfl) and uniqueness (discharged by introducing an arbitrary y and applying exact on the supplied equality hypothesis).
why it matters
The result anchors the parameter-free value of w₈ required for the α⁻¹ derivation inside the eight-tick neutrality setting. It directly implements the T6 eight-tick minimality step of the forcing chain by showing that the closed-form expression is the only real satisfying the condition. No downstream theorems are recorded, so the declaration closes the uniqueness interface for any later use of w₈ in mass or coupling calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.