Cosmology Large Scale Structure From Rs Lssregime

The five cosmic scales

Cosmology recognizes five canonical large-scale structures in the universe: the acoustic scale imprinted on the cosmic microwave background, baryon acoustic oscillations, galaxy clusters, filamentary structure, and cosmic voids. Each is a standard object in observational astronomy, identified by its characteristic comoving length, the distance that expands with the universe. The Recognition Science framework's ledger, a discrete record of recognition events, names these five regimes as a single formal catalog in its machine-checked library of formal theorems.

The catalog's content is exact and deliberately spare. It defines five named regimes, proves there are exactly five, and assigns each a scale on a ladder where successive rungs differ by the golden ratio φ, approximately 1.618. The definition is a structure with three proved properties: the count is five, the ratio of consecutive scales is φ, and every scale is positive. The mathematics is closed and checked; the declaration proves these facts and nothing beyond them.

In Recognition Science, the golden ratio is not an aesthetic choice but a forced constant. The framework's core theorem, proved in its library, shows that any cost function meeting five plain conditions must equal a specific form, and from that form the golden ratio follows as the unique self-similar scaling. The cosmic catalog applies that scaling to comoving lengths: each regime sits one rung up the φ-ladder. This is a structural claim about ratios between scales, not a derivation of what those scales physically are.

What the declaration does not claim is equally important. It does not prove that these five structures exist, that they are the only large-scale structures, or that any particular galaxy survey will find them. It does not derive the physical processes, such as gravitational collapse or acoustic oscillations, that produce these structures. The catalog is a classification scheme with a proved spacing rule, not a theory of structure formation. The bridge from the framework's recognition mathematics to physical cosmology remains open, a target for future work rather than an established result.

theorem lssRegime_count : Fintype.card LSSRegime = 5 := by decide

theorem scale_ratio (k : ℕ) : scale (k + 1) / scale k = phi := by
  unfold scale
  have hpos : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  rw [div_eq_iff hpos.ne', pow_succ]
  ring

structure LargeScaleStructureCert where
  five_regimes : Fintype.card LSSRegime = 5
  phi_ratio : ∀ k, scale (k + 1) / scale k = phi
  scale_always_pos : ∀ k, 0 < scale k

noncomputable def largeScaleStructureCert : LargeScaleStructureCert where
  five_regimes := lssRegime_count
  phi_ratio := scale_ratio
  scale_always_pos := scale_pos

What this page does not claim

The physical existence of the five structures is not proved by the declaration. The production of these structures by known physics is not derived. The bridge from recognition mathematics to physical cosmology is not established.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/LargeScaleStructureFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: