rs_strong_field_phi_deviation
plain-language theorem explainer
The RS strong-field deviation scale is fixed as φ^{-44}, the same rung-44 forcing that sets the baryogenesis ratio η_B. Gravity and strong-field phenomenology cite it as the algebraic signature that separates RS from pure GR's zero baseline. It is a one-line definition: raise the golden-ratio constant to the integer power -44.
Claim. The structural Recognition Science strong-field deviation is the real number $\varphi^{-44}$, where $\varphi$ is the RS golden-ratio constant (self-similar fixed point of the forcing chain).
background
Track 6.C of the quantum-gravity master plan asks for structural discriminators on strong-field tests (S-stars near Sgr A*, EHT shadow, Cassini Shapiro delay, lunar laser ranging). Pure GR predicts zero extra deviation in the RS accounting; RS must supply a positive, φ-rational signature that can later be specialized per channel.
The module closes only the algebraic half of that requirement. The scale chosen is the same rung-44 forcing already used for baryogenesis in the φ-rung ladder: η_B = φ^{-44} (eta_B_rung_val = -44). Here φ is the unique self-similar fixed point forced at T6 of the unified forcing chain; powers of φ are the native discrete scales of the theory.
The definition therefore names a single real: φ raised to the integer power -44. Downstream propositions only need positivity of this number and channel factors multiplying it; they do not re-derive the rung.
proof idea
Pure definition, no proof obligations. The body is the term Constants.phi ^ (-44 : ℤ): the RS constant φ (from the constants module) evaluated at the integer exponent -44 via real zpow. Noncomputable only because real exponentiation is noncomputable in the ambient library.
why it matters
This constant is the numeric spine of Track 6.C's structural discriminator. It feeds rs_strong_field_phi_deviation_pos (0 < φ^{-44}), the proposition rs_strong_field_distinct_GR_prop (strict positivity vs pure GR's zero), and the channel-wise observable shifts rs_strong_field_observable_shift, which multiply a positive channel factor by this scale.
Those pieces assemble into strong_field_one_statement and the certificate StrongFieldStructuralCert, which inhabit the master-theorem hypothesis StrongFieldTestsDistinctFromGR and retire it from the conditional gravity master theorem. The shared rung with η_B ties strong-field gravity to the cosmology ladder rather than introducing an ad hoc gravity-only scale.
What remains open is channel-specific physics: the exact precession, shadow, or Shapiro pattern in each dataset is not derived here; only the structural positivity that discriminates from pure GR is shipped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.