eta_exponent
plain-language theorem explainer
The definition computes the real exponent n such that the observed baryon-to-photon ratio satisfies η = φ^{-n}. Cosmologists testing Recognition Science baryogenesis models would cite it when checking whether the asymmetry sits on the φ-ladder. It is a direct one-line definition that evaluates the ratio of logarithms of the reciprocal observed η and of phi.
Claim. Let η denote the observed baryon-to-photon ratio and φ the golden ratio. The exponent n is defined by n = log(1/η) / log(φ).
background
Recognition Science derives the baryon asymmetry η = n_B / n_γ from CP violation inside the eight-tick phase structure. The observed value is fixed by eta_observed at 6.1 × 10^{-10}. The fundamental time quantum is the tick, with one octave equal to eight ticks. The module COS-007 targets derivation of η ~ 10^{-10} from the φ-structure and links it to the Sakharov conditions via intrinsic asymmetry in the 8-tick phases.
proof idea
This is a direct definition that applies the real logarithm to the reciprocal of eta_observed and divides by the real logarithm of phi. No lemmas or tactics are invoked beyond the built-in Real.log function.
why it matters
The definition supplies the numerical test for whether the matter-antimatter asymmetry lies on the φ-ladder, addressing the open question of deriving n from first principles. It connects to the modular discriminant construction in the Ramanujan bridge, where the exponent aligns with the directed flux count of 24. It draws on the eight-tick octave and the self-similar fixed point phi from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.