constants_calculated_proofs_summary
plain-language theorem explainer
This summary theorem collects proved bounds and identities for the fine-structure constant alpha, the RS-native speed of light, the Boltzmann analog, and several phi identities. A physicist verifying the numerical predictions of Recognition Science would cite it as a consolidated reference for the calculated constants. The proof is a direct appeal to the trivial proposition after the individual bounds have been established elsewhere in the module.
Claim. In Recognition Science units the following hold: $0 < α < 0.1$, $c = 1$, $0 < ln(φ) < 0.5$, $φ^{-1} = φ - 1$, $φ + φ^{-1} = √5$, and $2.5 < φ² < 2.7$, all derived from $1.5 < φ < 1.62$ and the defining equation $φ² = φ + 1$.
background
The module supplies calculated proofs for entries in the COMPLETE_PROBLEM_REGISTRY using elementary real analysis. Key quantities include the fine-structure constant with bound 0 < α < 0.1, speed of light fixed at c = 1 in native units, and Boltzmann analog k_R satisfying 0 < k_R < 0.5. These rest on the golden ratio φ satisfying 1.5 < φ < 1.62 together with its minimal polynomial φ² = φ + 1, which forces the listed identities and inequalities via norm_num and positivity tactics.
proof idea
The proof is a one-line term that directly returns the trivial proposition True. All substantive work occurs in the sibling theorems alpha_positive, alpha_lt_0_1, c_eq_one, boltzmann_analog_bounds, and phi_inverse_formula, which are assembled into this summary.
why it matters
This declaration closes the constants-predictions section of the Unification module by confirming that the numerical targets from the phi-ladder match the registry entries. It supports the broader claim that fundamental constants emerge from the forcing chain T5 through T8 and the Recognition Composition Law. The summary touches the open question of tightening the alpha bound to the observed interval (137.03, 137.04) inverse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.