C_lag_RS
C_lag_RS fixes the lag coupling constant in the ILG weight kernel to the RS-native value phi to the power minus five. Lab-scale gravity tests and flight propulsion models cite this when evaluating predicted deviations from Newtonian weight. The definition is a direct one-line assignment via the real power function on the golden-ratio constant.
claim$C_{lag}^{RS} := phi^{-5}$
background
The Flight.GravityBridge module links the ILG weight kernel from Gravity.ILG to flight schedules. The kernel takes the form w_t(T_dyn, tau_0) = 1 + C_lag * ((T_dyn/tau_0)^alpha - 1), where tau_0 is the recognition tick and alpha = (1 - phi^{-1})/2. C_lag_RS supplies the fixed coupling derived from the self-similar fixed point phi rather than a free parameter. Upstream, EightTickResonance.C_lag defines the identical quantity as phi^{-1} raised to the fifth power.
proof idea
One-line definition that applies Real.rpow to phi and the exponent -5.
why it matters in Recognition Science
This definition supplies the locked coupling used by rsLabPrediction and RunningCoupling in the same module, and by weight_rs, alpha_RS, and C_lag_RS in ClusterLensing. It implements the RS claim that the lag constant equals phi^{-5} (approximately 0.09) and feeds the eight-tick resonance structure for constants. The downstream rsLabPrediction doc-comment notes that the resulting lab-scale deviation would be large if the null hypothesis fails, providing a direct falsification route.
scope and limits
- Does not derive phi from the forcing chain inside this module.
- Does not compute numerical values or error estimates for C_lag_RS.
- Does not address possible scale dependence of the coupling.
- Does not prove positivity or boundedness of the weight function.
Lean usage
def rsLabPrediction : LabScalePrediction := mkLabPrediction typicalLabPeriod_seconds tau0_seconds ilg_alpha C_lag_RSformal statement (Lean)
163def C_lag_RS : ℝ := Real.rpow phi (-5)
proof body
Definition body.
164
165/-- With C_lag = φ⁻⁵ and typical lab scales, the predicted deviation is:
166 w - 1 = φ⁻⁵ * ((0.06 / 7.3e-15)^0.191 - 1)
167 ≈ 0.09 * 315
168 ≈ 28
169
170 This would be a LARGE effect if true! The null hypothesis would fail.
171-/