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

visibleSector

show as:
view Lean formalization →

The visibleSector definition selects the even phases 0, 2, 4, 6 from the 8-tick cycle as the visible matter sector. Cosmologists working within Recognition Science cite this partition when separating luminous ledger configurations from non-luminous shadows. It is a direct list definition with no further computation.

claimThe visible sector comprises the even phases $0,2,4,6$ of the eight-tick parity cycle.

background

Recognition Science obtains the eight-tick octave (T7) as period $2^3$ from the phi-forcing chain. The Cosmology.DarkMatter module models dark matter as ledger shadows at temporal resolution, with the dark sector occupying odd-phase orbits of the 8-tick parity cycle. The module documentation states: 'This module describes the σ=0, Z≠0 phantom sector at the temporal resolution scale: odd-phase orbits of the 8-tick parity cycle.' The complementary even phases therefore define the visible sector that couples to photons.

proof idea

The declaration is a direct definition that enumerates the even indices in Fin 8.

why it matters in Recognition Science

This definition supplies the visible-sector partition required by the ledger-shadow account of dark matter in COS-010. It implements the eight-tick octave (T7) landmark and supports downstream ratio calculations such as Ω_dm/Ω_b ≈ 5.4. The module links the partition to the rs_explains_null_detection suppression mechanism via phase mismatch and J(φ) suppression.

scope and limits

formal statement (Lean)

 146def visibleSector : List (Fin 8) := [0, 2, 4, 6]

proof body

Definition body.

 147
 148/-- The dark sector: phases 1, 3, 5, 7 (odd phases). -/