Pith. sign in
module module moderate

IndisputableMonolith.Cosmology.Matter_Radiation_Equality_RS

show as:
view Lean formalization →

Recognition Science packaging of the matter-radiation equality epoch. It defines a non-negative domain cost on the equality surface, a positive canonical threshold, and an inhabited certificate that bundles those facts. Cosmologists working in RS-native units would cite the certificate when anchoring equality-scale arguments. The module is largely definitional, with short positivity and evaluation lemmas.

claimThe module defines a domain cost $C$ for matter-radiation equality, records its value on the equality locus and proves $C \ge 0$, fixes a canonical threshold $\theta_*>0$, and supplies an inhabited certificate packing these data for downstream cosmology.

background

Recognition Science works in native units with $c=1$ and a fundamental tick $\tau_0=1$ from the Constants layer. Cost structure is imported from the Cost module: the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) is the unique symmetric cost forced by the Recognition Composition Law, and domain-level costs are built from it.

Matter-radiation equality is the cosmological surface where the matter and radiation energy densities match. In this module that surface is treated as a recognition domain: a scalar domain cost measures departure from equality, and a single positive canonical threshold marks the RS-native equality scale against which later redshift or density ratios can be compared.

Sibling definitions therefore split into three layers: the domain cost and its elementary properties (evaluation at equality, non-negativity), the canonical threshold and its positivity, and a certificate record that inhabits those facts as a single object.

proof idea

Definition module with thin supporting lemmas. The domain cost is introduced by definition; its value on the equality locus is a direct evaluation lemma; non-negativity follows from the underlying Cost axioms (J-cost non-negative on the positive reals). The canonical threshold is a named positive constant, with positivity discharged by a short arithmetic or Constants fact. The certificate is a structure packing cost, threshold, and the proved inequalities; inhabitance is a constructor application assembling those pieces. No deep tactic proof or forcing-chain step lives here.

why it matters in Recognition Science

Gives cosmology a typed RS handle on the matter-radiation equality epoch so later density, redshift, or horizon arguments can cite one certificate rather than re-proving cost non-negativity and threshold positivity in place. It sits downstream of Constants ($\tau_0$ and the RS unit system) and Cost (J-cost and domain-cost infrastructure), and is the natural attachment point for equality-scale numerics once the phi-ladder mass and coupling machinery is in play.

No parent theorems currently list this module as a dependency in the graph, so it functions as a leaf certificate layer: ready for import by broader cosmological forcing or observational-closure developments, but not yet wired into a named parent theorem. It does not itself force $D=3$, the eight-tick octave, or the fine-structure band; those remain upstream landmarks.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)