alphaRS_pos
plain-language theorem explainer
The RS-native factor α_RS = φ⁵/(8π) is strictly positive. Anyone assembling the unit bridge from κ_rs to the BMV phase rate cites this to discharge the positivity field of UnitBridgeTheorem. The proof unfolds the definition and applies positivity of real powers of φ and of π.
Claim. Let $\alpha_{\mathrm{RS}} := \varphi^5/(8\pi)$, where $\varphi$ is the golden ratio. Then $0 < \alpha_{\mathrm{RS}}$.
background
This module is Gravity IV: the unit bridge from the dimensionless RS coupling κ_rs to the SI BMV entangling phase rate (Theorem 4 of Gravity from Recognition IV). In RS-native units one has ħ = φ⁻⁵ and G = φ⁵/π, so G/ħ = φ¹⁰/π is fixed by φ alone.
The sibling definition α_RS := φ⁵/(8π) is the conversion factor that makes the identity κ_rs · α_RS = G/ħ hold when κ_rs = 8 φ⁵. The κ_rs band (85.6, 90.4) from ZeroParameterGravity then propagates linearly into the native BMV phase rate. Positivity of α_RS is the elementary arithmetic prerequisite for packaging that identity into the unit-bridge structure.
φ itself is the self-similar fixed point forced at T6 of the unified forcing chain; the powers of φ that appear in G and ħ are the standard RS-native normalizations (c = 1, ħ = φ⁻⁵, G = φ⁵/π).
proof idea
Tactic proof. Unfold α_RS to φ⁵/(8π). Obtain 0 < φ⁵ from Real.rpow_pos_of_pos applied to the positivity of φ. Obtain 0 < 8π from Real.pi_pos and linarith. Conclude with div_pos on the two strict inequalities.
why it matters
Feeds directly into unitBridgeTheorem, which packages three facts: α_RS > 0, the identity κ_rs · α_RS = G/ħ, and the SI closed form of the BMV phase rate factored through κ and α. Without positivity the UnitBridgeTheorem record cannot be inhabited.
In the broader framework this is a load-bearing arithmetic step of the quantum-channel gravity story: the dimensionless κ_rs band converts to a dimensionful tabletop phase rate only after α_RS is known to be a positive scalar. The SI side remains conditional on an ExternalCalibration anchor (the named open frontier of the dimensional bridge); this lemma itself is unconditional and closed.
It sits downstream of the RS-native constants (G, ħ in powers of φ) and upstream of the SI BMV rate factorization used in experimental comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.