allConditionsNeeded
plain-language theorem explainer
The declaration enumerates the three Sakharov conditions required for any net baryon asymmetry in the Recognition Science treatment of cosmology. Researchers deriving the observed baryon-to-photon ratio η ≈ 6.1 × 10^{-10} from the eight-tick phase structure would cite this list when stating the minimal prerequisites. The definition is a direct enumeration of the three constructors of the SakharovCondition inductive type with no further computation.
Claim. The complete list of Sakharov conditions is defined as the set containing baryon-number violation, C and CP violation, and departure from thermal equilibrium.
background
The module COS-007 derives the baryon-to-photon ratio η from Recognition Science's φ-structure, noting that the observed value η ≈ 6.1 × 10^{-10} requires an intrinsic asymmetry in the eight-tick phase structure together with CP violation in the ledger. The referenced inductive type SakharovCondition encodes the three classic requirements for baryogenesis: baryon number violation, C and CP violation, and departure from thermal equilibrium. Upstream definitions in sibling modules follow the same pattern of collecting complete finite lists (seven plot families, eight kinship systems, seven musical modes), indicating a uniform style for enumerating exhaustive collections.
proof idea
The definition is a direct one-line enumeration that constructs the list by naming the three constructors of the SakharovCondition inductive type. No lemmas or tactics are invoked; the body simply lists B_violation, C_CP_violation, and out_of_equilibrium in order.
why it matters
This definition supplies the explicit list needed to state that all three Sakharov conditions must hold for nonzero net baryon number at late times, directly supporting the module's target of obtaining η from the eight-tick octave and ledger CP violation. It fills the prerequisite step in the COS-007 derivation before any quantitative estimate of ε_CP or dilution factor can be attempted. The placement aligns with framework landmark T7 (eight-tick octave) where the intrinsic asymmetry originates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.