rs_strong_field_phi_deviation_pos
plain-language theorem explainer
The RS strong-field deviation scale φ^{-44} is strictly positive. Gravity and strong-field phenomenology cite this as the algebraic lower bound that separates Recognition Science from pure GR's zero classical deviation. The proof unfolds the deviation definition and applies positivity of integer powers of φ.
Claim. The Recognition Science strong-field deviation scale satisfies $0 < \varphi^{-44}$, where $\varphi$ is the golden ratio fixed point.
background
Track 6.C of the quantum-gravity master plan asks for a structural discriminator between RS and pure GR in strong-field tests (S-stars, EHT shadow, LLR, Cassini Shapiro delay). Pure GR predicts zero classical deviation from Schwarzschild/Kerr; RS carries a φ-rational signature at the same rung-44 scale that forces the baryon asymmetry η_B = φ^{-44} on the cosmology ladder.
In this module the deviation is defined as rs_strong_field_phi_deviation := φ^{-44}. The constant φ is the self-similar fixed point forced at T6 of the unified forcing chain, and φ > 0 is standard. The integer power φ^k (here k = -44) is the same scale construction used on the phi-rung ladder in cosmology.
This positivity lemma is the elementary arithmetic fact that turns that definition into a strict inequality against GR's zero baseline.
proof idea
One-line term proof after unfolding. Expand rs_strong_field_phi_deviation to φ^{-44}, then apply Mathlib's zpow_pos to φ_pos (the fact φ > 0) at the integer exponent -44. No case split or induction is needed: every integer power of a positive real is positive.
why it matters
This is the strict lower bound that makes the structural discriminator work. Downstream, rs_strong_field_distinct_GR_prop_holds is literally this theorem; rs_strong_field_observable_shift_pos multiplies it by a positive channel factor; strong_field_one_statement packages (0 < deviation) ∧ discriminator ∧ Nonempty StrongFieldTestsDistinctFromGR; and strongFieldStructuralCert records deviation_pos := this result.
Together they inhabit the master-theorem hypothesis StrongFieldTestsDistinctFromGR and retire it from the conditional Gravity.MasterTheorem list (Session 97). The numerical scale φ^{-44} ≈ 1.97×10^{-10} sits below current strong-field precisions (~10^{-4}–10^{-6}) but is in reach of LISA, next-gen EHT, and BBO. The exact per-channel deviation pattern remains future physics work; only the algebraic non-zero signature is closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.