gradient_coefficient
plain-language theorem explainer
gradient_coefficient supplies the prefactor multiplying spatial gradient terms when the gravitational wave action is expanded around an FRW background. It takes the scale factor a(t) and multiplies by a linear correction 1 + 0.01 α C_lag, where C_lag is the RS lag coupling. Workers deriving tensor wave equations in Recognition Science cosmologies would reference this expression when isolating quadratic contributions. The definition is a direct algebraic extraction from the ScaleFactor structure with no lemmas or reductions.
Claim. The gradient coefficient at cosmic time $t$ equals $a(t) (1 + 0.01 α C_lag)$, where $a(t)$ is the scale-factor function supplied by the FRW ScaleFactor structure.
background
ScaleFactor is the structure holding a positive function $a : ℝ → ℝ$ that encodes the cosmological expansion. C_lag is the constant φ^{-5} ≈ 0.09 taken from the eight-tick resonance module and represents the lag coupling derived in Recognition Science. The related scale definition returns φ^k for integer rung k and supplies the phi-ladder values used throughout the framework.
proof idea
The definition binds a := scale.a t and returns the product a * (1 + 0.01 * α * C_lag). It is a one-line algebraic wrapper that performs only structure projection and arithmetic.
why it matters
The definition supplies the explicit gradient prefactor inside the GW action expansion, supporting sibling declarations such as action_quadratic_tensor and action_form_verified. It directly imports the lag coupling C_lag from EightTickResonance, thereby embedding the T7 eight-tick octave into the relativistic action. No downstream theorems are yet recorded, indicating the object remains part of the scaffolding for full action verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.