canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, with φ the RS self-similar fixed point. Domain-coverage and milestone certificates in FinalModule_1400 cite this constant when comparing domain costs. The body is a one-line definitional assignment, not a derived equality.
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
FinalModule_1400 is a structural milestone module: zero sorry, zero axioms, certifying domain coverage in the Recognition Science physics layer. It imports Constants (for φ) and Cost (for the J-cost and related domain cost functionals).
In the forcing chain, T6 fixes φ as the unique self-similar scale; here it appears only as that named constant. The threshold φ − 3/2 is a fixed real cut used when domain costs are compared against a single canonical bar inside the milestone certificate.
Sibling material in the same file includes a positivity lemma for this threshold, a domain-cost evaluation identity, and the MilestoneCert structure that packages the coverage claim.
proof idea
Pure definition: the real constant is introduced by the assignment φ − 3/2. No lemmas, tactics, or algebraic reduction. Downstream positivity or comparison proofs unfold this def and work with the resulting real expression.
why it matters
Gives the milestone module a single named cut for domain-cost comparisons, so the structural certificate can state coverage against one RS-native number rather than an ad-hoc literal. φ enters from T6 (self-similar fixed point); the offset 3/2 is a module-local choice for the coverage bar, not a forcing-chain identity. Feeds the local MilestoneCert / cert package; no external used_by edges are recorded. Does not itself close any open physics derivation beyond naming the cut the certificate uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.