C_lag_RS
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.