pith. machine review for the scientific record. sign in
def definition def or abbrev high

experimentalStatus

show as:
view Lean formalization →

This definition assembles a list of three experimental anchors for the baryon asymmetry derivation in Recognition Science. A cosmologist studying baryogenesis from the eight-tick phase structure would cite it to check consistency with Planck data and observed CP violation. The definition constructs the list directly from three EtaFalsifier records without further computation.

claimThe experimental status is the list of pairs recording potential falsifier type and status: ⟨η measurement, (6.10 ± 0.04) × 10^{-10}⟩, ⟨CP violation, observed in K, B, D mesons⟩, ⟨φ connection, φ^{-47} gives right order of magnitude⟩.

background

The module COS-007 targets derivation of the baryon-to-photon ratio η ≈ 6.1 × 10^{-10} from Recognition Science's φ-structure via intrinsic asymmetry in the 8-tick phase and CP violation from the ledger. EtaFalsifier is the structure that records a falsification type (String) and its current status (String). Upstream results include the dimensionless bridge K = φ^{1/2} from Constants, the structure of nuclear densities and photon fluxes from NucleosynthesisTiers, and the J-cost structure from PhiForcingDerived.

proof idea

This is a direct definition that enumerates three EtaFalsifier structures with their respective falsifier types and status strings.

why it matters in Recognition Science

This definition anchors the COS-007 target of deriving η from the φ-structure and eight-tick asymmetry (T7) to current data. It supports the Sakharov conditions listed in the module and connects to the phi forcing chain in the foundation. No downstream theorems reference it yet.

scope and limits

formal statement (Lean)

 310def experimentalStatus : List EtaFalsifier := [

proof body

Definition body.

 311  ⟨"η measurement", "Precisely known: (6.10 ± 0.04) × 10⁻¹⁰"⟩,
 312  ⟨"CP violation", "Observed in K, B, D mesons"⟩,
 313  ⟨"φ connection", "φ^(-47) gives right order of magnitude"⟩
 314]
 315
 316end MatterAntimatter
 317end Cosmology
 318end IndisputableMonolith

depends on (8)

Lean names referenced from this declaration's body.