Pith. sign in
def

canonicalThreshold

definition
show as:
module
IndisputableMonolith.Cosmology.Spectral_Index3_FromJCost
domain
Cosmology
line
20 · github
papers citing
none yet

plain-language theorem explainer

Canonical threshold is the real constant φ − 3/2 used as the comparison scale in the J-cost derivation of the scalar spectral index on the φ-ladder. Cosmologists citing the RS n_s structural theorem (Plan v7) need this cutoff when checking domain-cost positivity and certificate bounds. It is a bare definitional binding, not an inequality.

Claim. Let $\varphi$ be the golden ratio (self-similar fixed point of the Recognition forcing chain). The canonical threshold is the real number $\varphi - 3/2$.

background

The module derives the scalar spectral index from the φ-ladder and the Recognition cost $J$. In RS units $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), and $\varphi$ is forced as the unique self-similar fixed point (T6 of the UnifiedForcingChain). The local claim is structural: RS predicts $n_s=1-2/(N_e+1)=1-2/45\approx0.9556$, consistent with Planck 2018 $n_s=0.9649$ inside roughly $3\sigma$, with zero sorry and zero axioms.

Sibling material in the same file introduces a domain cost on the ladder and a positivity lemma for this threshold. The numerical value $\varphi-3/2\approx0.118$ sits at the small positive scale where rung comparisons and cost defects become nontrivial relative to golden-ratio geometry.

proof idea

Definitional binding only: the constant is identified with the real expression $\varphi-3/2$. No tactics, no lemmas, no proof obligations.

why it matters

Gives the explicit numerical cutoff consumed by the spectral-index certificate chain in this module (siblings such as the positivity statement for the threshold and the nS3Cert / cert inhabitants). Anchors the cosmology layer to the forced $\varphi$ of the T0–T8 chain and to the J-cost that underlies mass and coupling ladders elsewhere in RS. Supports the module-level structural claim that the RS $n_s$ prediction is observationally consistent without introducing new axioms.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.