pith. sign in
module module moderate

IndisputableMonolith.Cosmology.LargeScaleStructureFromRS

show as:
view Lean formalization →

This module defines the large-scale structure regime and its certification objects in Recognition Science cosmology. It introduces LSSRegime along with scale, scale_ratio, scale_pos and LargeScaleStructureCert for hierarchical structure modeling. Cosmologists working from the phi-ladder would cite these when extending RS to cosmic scales. The module consists of definitions and basic properties.

claimDefinitions of the large-scale structure regime $\mathrm{LSSRegime}$, scaling functions $\mathrm{scale}$, $\mathrm{scale\_ratio}$, $\mathrm{scale\_pos}$, and certification $\mathrm{LargeScaleStructureCert}$ in RS cosmology.

background

The module sits in the cosmology domain and imports the RS time quantum from Constants, quoted as "The fundamental RS time quantum (RS-native). $\tau_0 = 1$ tick." It defines LSSRegime as the regime for large-scale structures using the phi-ladder for mass and scale hierarchies. The setting extends the unified forcing chain (T0-T8) and Recognition Composition Law to cosmological scales with RS-native units.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies foundational objects for large-scale structure in RS cosmology and is positioned to feed parent theorems on structure formation. It connects the forcing chain landmarks (T5 J-uniqueness, T6 phi fixed point, T8 D=3) to cosmological applications via the phi-ladder and mass formula.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)