phiPsiCouplingStub
plain-language theorem explainer
This definition supplies a placeholder instance for phi-psi coupling facts inside the relativity fixtures. Developers maintaining the trust boundary between stubbed hypotheses and production code would cite it. The implementation introduces the parameters ng, alpha, C_lag and x then refines the difference field to zero via simp and norm_num.
Claim. The noncomputable definition supplies an instance of the structure containing the phi-minus-psi difference function by setting that difference to zero for any parameters ng, alpha, lag coupling $C_{lag} = phi^{-5}$, and variable $x$.
background
The module Relativity.NewFixtures supplies stub instances for hypothesis classes introduced to replace sorries. These live outside production namespaces to keep the trust boundary clear. Upstream, C_lag is the RS-derived lag coupling defined by $C_{lag} := phi^{-5} approx 0.09$. The stub uses this constant to populate the coupling structure without further computation.
proof idea
The definition is a one-line wrapper that applies intro to the four arguments ng, alpha, C_lag, x, then refines the structure field to the pair containing zero. The two subgoals are discharged by simp and norm_num.
why it matters
This stub closes a hypothesis interface in the relativity fixtures, allowing downstream code to compile while the trust boundary remains explicit. It draws the lag parameter from the eight-tick resonance result C_lag in Gravity.EightTickResonance. The declaration touches the open question of replacing the trivial zero difference with a derivation from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.