canonicalThreshold
plain-language theorem explainer
Defines the canonical collapse threshold as φ − 3/2 in RS-native units. Anyone citing the wave-function collapse certificate or domain-cost comparison against the nearest rung uses this constant. The body is a one-line real definition from the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of the Recognition self-similarity relation.
background
In the RS wave-function collapse module, measurement is identified with a ledger posting (a recognition event). Collapse is J-cost minimization onto the nearest rung of the φ-ladder; the eight-tick octave fixes the minimal recognition time. No hidden-variable layer is introduced.
The cost functional J is the unique nonnegative generator forced by the Recognition Composition Law (T5): $J(x)=(x+x^{-1})/2-1$. The constant φ is the self-similar fixed point forced at T6. Domain cost (sibling domainCost) measures how far a candidate amplitude sits from a rung; the threshold below is the numerical cutoff against which that cost is compared.
The module imports only Mathlib, Constants (for φ), and Cost (for J). Status is structural: zero sorry, zero axiom.
proof idea
Pure definition: the real constant is written as phi - 3/2. No proof obligations, no lemmas applied. Positivity and certificate packaging live in sibling declarations (canonicalThreshold_pos, RSWFCollapseCert).
why it matters
Supplies the numerical gate for the collapse story: a recognition event posts when domain cost falls at or below this threshold. That gate sits inside the structural collapse certificate and the inhabited-cert construction in the same module. Framework landmarks touched are T5 (J uniqueness), T6 (φ forced), and T7 (eight-tick minimal recognition time). The module framing is that collapse equals ledger posting with no hidden variables; this constant is the concrete cutoff that makes the comparison well-defined in RS units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.