canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the canonical threshold used in the RS CMB acoustic-peak analysis. Cosmologists working the φ-power spacing of multipoles (ℓ₁≈220, ℓ₂≈540, ℓ₃≈800) cite it when comparing domain cost to a fixed cutoff. The body is a one-line abbreviation of that arithmetic combination of 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
The module treats CMB acoustic peaks under Recognition Science: observed multipoles satisfy rough ratios $\ell_2/\ell_1 \approx 2.45 \sim \varphi^2$ and $\ell_3/\ell_1 \approx 3.64 \sim \varphi^{2.8}$, so peak locations are read as φ-power spacing on the ladder. Status is structural (zero sorry, zero axiom).
φ itself is the unique self-similar fixed point forced at T6 of the unified forcing chain; it appears throughout RS-native constants and the mass ladder. The Cost import supplies the J-cost and related nonnegativity facts used by sibling lemmas such as domainCost and domainCost_nonneg. The threshold φ − 3/2 sits just below 0.12 and is the fixed comparison value against which domain cost is tested when certifying peak positions.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression φ − 3/2. No proof obligations; positivity and downstream comparisons are handled by sibling lemmas (e.g. canonicalThreshold_pos).
why it matters
Gives a single named cutoff for the CMB peak-position certificate (CMBPeakPos_v3Cert and the inhabited cert). Without a fixed threshold, domain-cost comparisons that underwrite the φ-power reading of ℓ-ratios would be ad hoc. It sits inside the cosmology layer that links the eight-tick / φ-ladder structure (T6–T7) to observable multipole spacing, keeping the structural theorem free of free parameters beyond φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.