kappa_bounds
The theorem establishes that the RS-native Einstein gravitational coupling κ equals 8φ⁵ lies strictly between 85.6 and 90.4. Researchers working on zero-parameter gravity derivations would cite this interval to anchor the coupling constant within the Recognition framework. The proof imports the φ⁵ bounds lemma and scales the interval by eight via linear arithmetic.
claim$85.6 < 8φ^5 < 90.4$, where φ denotes the golden ratio and the prefactor 8 counts the vertices of the three-dimensional cube.
background
The module supplies machine-verified numerical intervals for every derived physical quantity in Recognition Science. Each result is an algebraic inequality proved from the golden-ratio identities φ² = φ + 1 and the Recognition Composition Law, without floating-point evaluation. The local setting is the master certificate that collects all such bounds into a single verified structure. Upstream, phi_fifth_bounds states that 10.7 < φ⁵ < 11.3, with the explicit identity φ⁵ = 5φ + 3 used to obtain the interval from the tighter bounds on φ itself.
proof idea
The proof is a one-line wrapper. It obtains the φ⁵ interval from phi_fifth_bounds, splits the target conjunction with constructor, and scales both sides by eight using nlinarith.
why it matters in Recognition Science
The bound feeds directly into NumericalPredictionsCert and the zero-parameter gravity model. It realizes the eight-tick octave (T7) and three spatial dimensions (T8) by fixing the vertex count V = 2³ = 8. The interval is chosen to bracket the conventional 8π value after conversion to SI units, closing one link in the forcing chain from the Recognition Composition Law to observable gravitational strength.
scope and limits
- Does not derive the value of G from experiment.
- Does not claim equality between 8φ⁵ and 8π.
- Does not extend the bound to other coupling constants.
- Does not address renormalization or running of κ.
formal statement (Lean)
123theorem kappa_bounds : (85.6 : ℝ) < 8 * phi ^ 5 ∧ 8 * phi ^ 5 < (90.4 : ℝ) := by
proof body
Term-mode proof.
124 have h5 := phi_fifth_bounds
125 constructor
126 · nlinarith [h5.1]
127 · nlinarith [h5.2]
128
129/-! ## Planck constant: ℏ = φ⁻⁵ -/
130
131/-- ℏ = φ⁻⁵ ∈ (0.088, 0.093): the reduced Planck constant in RS-native units. -/