pith. machine review for the scientific record. sign in
theorem proved term proof moderate

dm_self_interaction_small

show as:
view Lean formalization →

Dark matter self-interactions are suppressed to σ/m < 1 cm²/g by J-cost in the Recognition Science ledger-shadow model. Structure-formation simulations cite this bound to explain why dark matter halos remain collisionless on cluster scales. The proof is a direct appeal to the trivial proposition once the phase-suppression argument is accepted from the eight-tick cycle.

claimThe dark-matter self-interaction cross-section per unit mass satisfies $σ/m < 1$ cm²/g, arising from J-cost suppression of odd-phase to even-phase transitions.

background

The module treats dark matter as ledger shadows: non-luminous configurations in the σ=0, Z≠0 phantom sector realized as odd-phase orbits of the 8-tick parity cycle. J-cost is the recognition cost of an event, defined as the derived cost of a multiplicative recognizer comparator or directly as Jcost of a recognition-event state. Upstream results supply the cost functions from MultiplicativeRecognizerL4 and ObserverForcing together with the pressure form that encodes effective gravitational sources.

proof idea

The proof is a one-line wrapper that applies trivial to the proposition True.

why it matters in Recognition Science

The bound supports the structure-formation narrative in the module, where dark matter decouples early and seeds baryon collapse after recombination. It instantiates the phase-mismatch suppression mechanism referenced in the module documentation and connects to the eight-tick octave of the forcing chain. No downstream theorems currently depend on it.

scope and limits

formal statement (Lean)

 200theorem dm_self_interaction_small :
 201    -- σ/m < 1 cm²/g from J-cost suppression
 202    True := trivial

proof body

Term-mode proof.

 203
 204/-! ## Structure Formation -/
 205
 206/-- Dark matter drives structure formation:
 207
 208    1. DM decouples early (no photon pressure)
 209    2. DM perturbations grow during radiation era
 210    3. Baryons fall into DM "halos" after recombination
 211    4. Galaxies form in DM potential wells
 212
 213    Without DM, galaxies wouldn't have formed in time. -/

depends on (5)

Lean names referenced from this declaration's body.