canonicalThreshold
plain-language theorem explainer
Defines the real scalar threshold φ − 3/2 used as the cut separating recognition-detectable branches from undetectable ones in the J-cost many-worlds module. Anyone citing the structural many-worlds claim (branches macroscopically distinct only when J is at least J(φ)) needs this constant. It is a bare definitional abbreviation, not a proved inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of the Recognition self-similarity relation.
background
The module treats many-worlds branching as a J-cost phenomenon: branches multiply when the cost of the amplitude exceeds the cost of φ, while small-amplitude branches with J below J(φ) remain recognition-undetectable. Only branches with J at least J(φ) count as macroscopically distinct.
J is the unique nonnegative cost forced by the Recognition Composition Law, J(x) = (x + x^{-1})/2 − 1 (equivalently cosh(log x) − 1). φ is the self-similar fixed point forced at T6 of the unified forcing chain. The present definition simply names the real offset φ − 3/2 that the surrounding certificates use as a numerical cut relative to that scale.
The module imports the global Constants and Cost layers, so φ and J are the standard RS objects; no local redefinition occurs here.
proof idea
Pure definition: the identifier is bound to the real expression φ − 3/2. There is no proof body, no tactic, and no lemma application.
why it matters
Gives a single named real that the many-worlds certificates (positivity of the threshold, the three-world certificate, and the inhabited cert) can cite without repeating the arithmetic. It sits inside the structural many-worlds story of the module: J-cost above J(φ) marks macroscopically distinct branches. The offset relative to φ is local bookkeeping for that cut; it does not itself re-derive T5–T6 or the eight-tick octave. Downstream siblings such as the positivity lemma and the ManyWorlds3Cert package are the places that turn the bare constant into a usable hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.