lambda_8
plain-language theorem explainer
The definition assigns the constant value 8 to the 8-tick coupling scale λ_8 in RS-native units. Cosmologists addressing the σ₈ tension would cite it when inserting recognition strain into late-time structure growth. The assignment follows at once from the eight-tick octave period in the forcing chain.
Claim. $λ_8 := 8$, the 8-tick coupling scale in Mpc below which the recognition strain $Q(k) = J(k/k_8)$ becomes appreciable.
background
The module treats the σ₈ tension by showing that recognition strain Q, accumulated over 8-tick cycles, suppresses growth below a characteristic scale. In RS-native units the fundamental time quantum is the tick τ₀ = 1, and the wavenumber tied to the coupling scale is k_8 = 2π/λ_8. The upstream scale function returns powers of phi, while the tick definition supplies the base time unit used to convert the eight-tick period into a length.
proof idea
One-line definition that directly binds the numeral 8 to λ_8, matching the eight-tick octave length stated in the module comment.
why it matters
The definition supplies the fixed coupling scale that enters the strain formula and the suppression relation σ₈^RS = σ₈^CMB · (1 - Q/Q_max). It instantiates the eight-tick octave (T7) of the forcing chain and closes the link between the recognition operator and the observed 5 % suppression reported in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.