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

structureFormation

show as:
view Lean formalization →

Dark matter ledger shadows in Recognition Science drive structure formation by decoupling early at z around 10^6, permitting linear growth of perturbations during the radiation era. Baryons subsequently collapse into the resulting halos after recombination near z 1100, enabling galaxies to assemble on observed timescales. Cosmologists working in the eight-tick parity framework cite this sequence to account for the required matter density without extra particles. The declaration is a direct list literal with no reduction steps.

claimThe sequence of dark matter driven structure formation is DM decouples early ($z sim 10^6$), DM perturbations grow as $delta propto a$, baryons fall in after $z sim 1100$, galaxies form in DM halos.

background

The COS-010 module treats dark matter as the temporal projection of the sigma=0, Z nonzero phantom sector, realized as odd-phase orbits within the 8-tick parity cycle. Upstream, the EightTick.phase definition supplies the discrete angles k pi over 4 for k in Fin 8, periodic with period 2 pi, while the Wedge.phase supplies the unimodular complex number exp(i w). These phases underwrite the ledger-shadow picture in which gravitationally active entries remain electromagnetically decoupled, consistent with the observed Omega_dm approximately 0.27 and the requirement that galaxies form in time.

proof idea

The declaration is a direct definition that assigns a four-element list of strings. It references the phase constructions from EightTick and Wedge only for contextual parity, with no tactic steps or lemma applications inside the body.

why it matters in Recognition Science

This definition fills the structure-formation step of the COS-010 paper proposition on non-luminous ledger configurations. It anchors the T7 eight-tick octave within cosmology and supplies the qualitative mechanism that resolves the galaxy-formation timeline. No downstream theorems are recorded, leaving open its quantitative link to the phi-ladder mass formula and the alpha band.

scope and limits

formal statement (Lean)

 214def structureFormation : List String := [

proof body

Definition body.

 215  "DM decouples early (z ~ 10⁶)",
 216  "DM perturbations grow: δ ∝ a",
 217  "Baryons fall in after z ~ 1100",
 218  "Galaxies form in DM halos"
 219]
 220
 221/-! ## Detection? -/
 222
 223/-- Can ledger shadows be detected?
 224
 225    1. **Gravitational**: Already detected (rotation curves, etc.)
 226    2. **Direct detection**: Scattering off nuclei - difficult
 227       (Odd-phase doesn't couple well to even-phase)
 228    3. **Indirect**: Annihilation products - possible
 229       (Odd + odd → even, produces visible particles)
 230    4. **Collider**: Produce at LHC - no luck so far -/

depends on (2)

Lean names referenced from this declaration's body.