IndisputableMonolith.Cosmology.EtaBIntervalCert
Certifies rational bounds on φ^{44} and φ^{-44} from the Fibonacci–φ identity, then packages them as an interval certificate for the baryon-to-photon ratio η_B. Cosmology proofs that place the observed η_B on an RS φ-rung cite this enclosure. The work is elementary closed-form arithmetic plus comparison lemmas, not a derivation of the rung integer itself.
claimThe golden ratio obeys $\varphi^{n+1}=F_{n+1}\varphi+F_n$. Specializing at the rung integer $44$ yields explicit rational lower and upper bounds on $\varphi^{44}$ and $\varphi^{-44}$. Those bounds define a closed real interval that contains both the RS structural $\eta_B$ prediction (φ-power piece) and the observed baryon-to-photon ratio.
background
In Recognition Science the baryon-to-photon ratio $\eta_B$ is tied to a φ-ladder rung. Upstream BaryonAsymmetryDerivation splits cleanly: it is a theorem that $\eta_B>0$ follows from $J_{CP}>0$ (Jarlskog from Gray-code chirality) plus the Sakharov conditions, while the numerical magnitude remains a scaffold on a φ-rung hypothesis that does not yet match the observed number by itself.
φ is the self-similar fixed point forced at T6 of the unified forcing chain. Powers of φ admit the exact Fibonacci identity $\varphi^{n+1}=F_{n+1}\varphi+F_n$, which converts the transcendental power $\varphi^{44}$ into rational arithmetic Lean can certify by comparison.
This module sits between that structural scaffold and the exact-rung and prefactor modules. It supplies machine-checked enclosure at the integer 44; it does not justify why the integer is 44.
proof idea
Record the Fibonacci–φ identity, then specialize to obtain exact Fibonacci expressions for $\varphi^{44}$. Prove rational lower and upper bounds on $\varphi^{44}$ (and by reciprocal arithmetic on $\varphi^{-44}$) by evaluating those expressions and comparing. Assemble the bounds into the interval certificate for $\eta_B$, and check that the observational central value lies inside it. Auxiliary factorization lemmas relate 44 to flip and torsion factors used in rung bookkeeping downstream. No analytic number theory beyond the closed form is required.
why it matters in Recognition Science
Downstream, EtaBExactRungDerivation imports this certificate while closing the open-frontier item of deriving the integer $-44$ from $D=3$ alone by three independent routes that must agree. EtaBPrefactorDerivation imports it while treating the order-one prefactor $c_{RS}=(1-\varphi^{-8})^2$ honestly as a selected ansatz, not a derivation. Without a checked enclosure of the $\varphi^{-44}$ piece, those modules cannot claim the observed $\eta_B$ sits on the predicted rung. The module therefore turns the scaffold magnitude of the baryon-asymmetry derivation into a falsifiable interval claim tied to T6 (φ forced) and the cosmology side of the RS ladder.
scope and limits
- Does not derive the integer 44 from D = 3; that is deferred to the exact-rung module.
- Does not derive the order-one prefactor c_RS; only encloses the φ-power factor.
- Does not prove structural positivity η_B > 0; that lives in the upstream baryon-asymmetry module.
- Does not claim point equality with observation, only interval membership.
- Does not fix RS units or convert between τ_0 ticks and SI baryon-photon data.
used by (2)
depends on (2)
declarations in this module (14)
-
lemma
phi_sq_eq' -
lemma
phi_pow_fib -
lemma
phi_pow_44_fib -
theorem
phi_pow_44_lower -
theorem
phi_pow_44_upper -
lemma
phi_rpow_44 -
theorem
phi_pow_neg44_lower -
theorem
phi_pow_neg44_upper -
theorem
eta_B_interval -
theorem
observed_eta_in_interval -
theorem
forty_four_factorization -
theorem
rung_44_equals_flip_times_torsion -
structure
EtaBCert -
def
etaBCert