pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Cosmology.TensorToScalarRatioFromRS

show as:
view Lean formalization →

The module assembles definitions and lemmas that extract the tensor-to-scalar ratio r directly from the Recognition Science phi-ladder and J-cost relations. Cosmologists comparing inflation models to CMB data would cite the resulting bounds and certification. The module structure consists of an algebraic identity for phi squared, followed by positivity, upper-bound, and interval lemmas that together certify the ratio.

claimThe RS tensor-to-scalar ratio is the quantity $r = 2/phi^2$ obeying $0 < r < 1$ and lying inside a narrow observational band derived from the golden-ratio fixed point.

background

The module operates inside the cosmology domain of Recognition Science and imports the fundamental time quantum tau_0 = 1 tick from Constants. It employs the J-cost function obeying the Recognition Composition Law together with the phi-ladder that assigns mass and energy scales via phi raised to integer rungs. The local setting is the tail of the forcing chain T5-T8 that fixes phi as the self-similar point and D = 3 spatial dimensions.

proof idea

This is a definition module, no proofs. It collects an equality phi2_eq, the positivity lemma r_pos, the strict upper bound r_lt_one, the interval statement r_band, and the wrapper certification TensorRatioCert.

why it matters in Recognition Science

The module supplies the concrete value of the tensor-to-scalar ratio that enters cosmological observables downstream of the T6 phi fixed point and the eight-tick octave. It therefore links the core Recognition Science forcing chain to CMB constraints on primordial gravitational waves. No downstream theorems are yet recorded.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)