Pith. sign in
theorem

canonicalThreshold_pos

proved
show as:
module
IndisputableMonolith.Cosmology.RS_COS_Structural_008
domain
Cosmology
line
21 · github
papers citing
none yet

plain-language theorem explainer

The canonical threshold used for RS cosmology rung spacing is strictly positive. Structural cosmology certificates rely on this to keep the threshold above zero when adjacent rungs scale by φ. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.

Claim. The canonical threshold constant built from the golden ratio $\varphi$ in this module is strictly positive: $0 < \tau_{\mathrm{can}}$.

background

This module records structural facts for Recognition Science cosmology rung spacing: adjacent mass/energy rungs differ by the fixed factor $\varphi = (1+\sqrt{5})/2 \approx 1.618$. The status line is a pure structural theorem (no sorry, no axioms).

The golden ratio enters from Constants. The only upstream lemma used here is the tighter lower bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$ via $(1+\sqrt{5})/2 > 3/2$. The canonical threshold is a real constant defined from $\varphi$ in this file; positivity is the minimal arithmetic fact needed before comparing domain costs or certificate bounds against it.

proof idea

One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau_{\mathrm{can}}$ by linarith using the imported lemma $\varphi > 1.5$. No case splits or further Recognition identities are required.

why it matters

Keeps the structural certificate stack for RS cosmology module 8 on a positive threshold when rungs scale by $\varphi$. That matches the forcing-chain landmark T6: $\varphi$ is the self-similar fixed point that sets rung spacing. Sibling definitions (domainCost, nonnegativity, the certificate bundle) sit next to this fact; nothing downstream is wired yet in the graph, so this is a local positivity gate rather than a deep mass-ladder theorem. It does not touch $\alpha$, $D=3$, or the eight-tick octave.

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