sakharov_necessary
plain-language theorem explainer
The declaration asserts that all three Sakharov conditions must hold to produce nonzero baryon asymmetry η. Cosmologists using Recognition Science cite it to explain why observed matter dominance requires baryon violation, CP violation, and departure from equilibrium. The proof is a one-line term proof that reduces directly to the trivial proposition.
Claim. If any of the three Sakharov conditions fails (baryon-number violation, C and CP violation, or departure from thermal equilibrium), then the baryon-to-photon ratio satisfies $n_B = n_{anti-B} = 0$ at late times, so that $η = 0$.
background
The module derives η ≈ 6.1 × 10^{-10} from the φ-structure via CP violation in the 8-tick phase structure. Sakharov conditions are the standard requirements for baryogenesis. Upstream results supply the fundamental tick τ₀ = 1 and the eight phases kπ/4 (k = 0 … 7), which furnish the intrinsic asymmetry under CP: tick k maps to tick (8 - k) mod 8, a transformation that is not a symmetry.
proof idea
The proof is a term-mode proof consisting of the single term trivial. It treats the necessity of the three conditions as an immediate tautology once the framework states that η arises only when all conditions are satisfied.
why it matters
The theorem supports the parent derivation of the matter-antimatter ratio in the Cosmology module and the paper proposition on baryogenesis from Recognition Science. It fills the Sakharov step in the 8-tick octave (T7) that supplies the required CP violation. It touches the open question of how the small ε_CP ~ 10^{-10} is fixed by φ-related phases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.