kinetic_coefficient
plain-language theorem explainer
This definition supplies the time-dependent prefactor multiplying the kinetic term in the quadratic action for tensor modes on an expanding background. Cosmologists working in Recognition Science would cite it when isolating the effective inertia of gravitational waves or computing their energy density. The implementation is a direct algebraic expression that cubes the scale factor and applies a small linear correction from the lag coupling.
Claim. Let $a(t)$ be the scale factor. The kinetic coefficient at cosmic time $t$ equals $a(t)^3(1 + 0.01α C_{lag})$, where $α$ is a dimensionless parameter and $C_{lag}$ is the lag coupling constant.
background
The ScaleFactor structure consists of a positive real-valued function $a:ℝ→ℝ$ that encodes the cosmic expansion history. The lag coupling $C_{lag}$ is defined as $φ^{-5}≈0.09$, the RS-derived value from the eight-tick resonance. This definition belongs to the module that expands the gravitational action around an FRW background to isolate tensor contributions, importing the scale-factor structure and the lag constant from upstream modules.
proof idea
It is a one-line wrapper that projects the scale-factor function from the ScaleFactor structure at the supplied time $t$, cubes the result, and multiplies by the perturbative factor linear in $α$ and $C_{lag}$. No additional lemmas are invoked beyond the field access.
why it matters
The definition supplies the leading time dependence required for the quadratic tensor action in the GW sector. It incorporates the lag coupling from EightTickResonance and the scale factor from FRWMetric, serving as an intermediate block for the action expansion and verification steps in the same module. It connects to the T7 eight-tick octave through the origin of $C_{lag}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.