phi
plain-language theorem explainer
The golden ratio $\varphi=(1+\sqrt{5})/2$ as a real constant. Cosmology and baryogenesis staging code cites it whenever RS-native scales, ladders, or dimensionless ratios appear. The body is the classical closed form; nothing is proved.
Claim. Define $\varphi := (1 + \sqrt{5})/2 \in \mathbb{R}$.
background
Recognition Science forces a unique dimensionless self-similarity ratio. In the forcing chain, T6 identifies that fixed point with the golden ratio $\varphi=(1+\sqrt{5})/2$, which then sets the $\varphi$-ladder for masses, the eight-tick octave, and RS-native constants ($\hbar=\varphi^{-5}$, $G=\varphi^{5}/\pi$, etc.).
This module stages honest theorem targets for the Steve baryogenesis derivation. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus equilibration yields vanishing final baryon number. Local quantities (reprocessing factors, washout exponents, freeze-out windows) are dimensionless and often expressed relative to $\varphi$-scaled thresholds.
The definition supplies a single Mathlib-backed real for those expressions, avoiding ad-hoc numeric literals.
proof idea
Pure definition: the noncomputable real is introduced as the classical algebraic value $(1+\sqrt{5})/2$. No lemmas, tactics, or proof obligations.
why it matters
Gives the baryogenesis staging lane a canonical $\varphi$ matching the RS forcing chain (T6) and the mass/ladder conventions used elsewhere in the monolith. Downstream staging targets (sphaleron reprocessing, relic charge, freeze-out windows) can write $\varphi$-native bounds without redefining the constant. No parent theorem is wired yet (used_by is empty); the def is infrastructure so loop-generated targets stay axiom-free and do not fake physics conditions as True.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.