IndisputableMonolith.Unification.ConstantsPredictionsProved
This module proves positivity, bounds, and related properties for the fine-structure constant α and auxiliary constants such as the Boltzmann analog in Recognition Science units. Researchers deriving physical constants from the phi-forcing chain would cite these results to close the no-free-parameters claim. The module consists of direct statements that apply lemmas from the imported Constants, Alpha, GapWeight, and PhiForcing modules.
claim$α > 0$, $α < 0.1$, and $α$ bounds together with positivity and bounds on the Boltzmann analog and $c = 1$.
background
The module sits inside the Unification domain and imports the RS time quantum $τ_0 = 1$ tick from Constants, the 8-tick gap weight $w_8$ (with $f_{gap} = w_8 · ln(φ)$) from GapWeight, and the self-similarity argument that forces $φ$ from a discrete ledger with J-cost from PhiForcing. These upstream results supply the J-cost structure and the eight-tick octave needed to compute α without adjustable parameters. The module therefore assembles the concrete predictions that follow once φ and the gap weight are fixed.
proof idea
The module aggregates multiple small proved declarations (alpha_positive, alpha_lt_0_1, alpha_bounds, boltzmann_analog_formula, c_eq_one, etc.). Each declaration is a direct application of the imported lemmas on positivity, ordering, and the explicit formulas for α and the Boltzmann analog; no complex tactic scripts or additional hypotheses appear.
why it matters in Recognition Science
The module supplies the proved constant predictions required by the unification pipeline, directly addressing the α band (137.030, 137.039) and the positivity of derived quantities. It closes the calculated claims that follow from T5–T8 of the forcing chain and the Recognition Composition Law once the gap weight and φ are in place. No downstream uses are recorded yet.
scope and limits
- Does not compute a numerical central value for α beyond the stated bounds.
- Does not treat constants outside the listed sibling declarations.
- Does not include experimental comparisons or error estimates.
- Does not extend the forcing chain beyond the imported modules.
depends on (4)
declarations in this module (16)
-
theorem
alpha_positive -
theorem
alpha_lt_0_1 -
theorem
alpha_bounds -
theorem
c_eq_one -
theorem
c_positive -
theorem
boltzmann_analog_formula -
theorem
boltzmann_analog_positive -
theorem
boltzmann_analog_lt_half -
theorem
boltzmann_analog_bounds -
theorem
phi_inverse_formula -
theorem
phi_plus_inverse_eq_sqrt5 -
theorem
phi_sq_gt_2_5 -
theorem
phi_sq_lt_2_7 -
structure
ConstantsPredictionsCert -
theorem
constants_predictions_cert_exists -
theorem
constants_calculated_proofs_summary