action_form_verified
plain-language theorem explainer
The declaration supplies a proposition asserting that the gravitational wave action expansion takes verified form when given a scale factor, a transverse-traceless tensor perturbation, and real parameters alpha with the lag coupling. Researchers deriving tensor mode dynamics from the Recognition Science framework would reference this when confirming the quadratic action around FRW. The verification proceeds by direct assignment to the constant true proposition.
Claim. Let $a(t)$ be a positive scale factor, let $h_{TT}(t,i,j)$ be a transverse traceless tensor field, and let $α, C_{lag}$ be real numbers. The action form is then verified.
background
ScaleFactor provides the positive real-valued function $a(t)$ central to the FRW background metric. TensorPerturbation requires the tensor $h_{TT}$ to obey transversality (vanishing sum over one index) and tracelessness (vanishing spatial trace). The lag coupling $C_{lag}$ is defined as $φ^{-5}$ and arises from the eight-tick resonance. The scale function supplies $φ^k$ values for discrete wavenumbers from large-scale structure analysis. This definition appears in the gravitational wave action expansion module, which assembles quadratic tensor terms using imported results on geometry, fields, cosmology, and tensor decomposition.
proof idea
The body of the definition is the constant proposition True. No upstream lemmas are invoked. The verification holds unconditionally for any inputs of the stated types.
why it matters
This marks the verified action form for gravitational waves in the Recognition Science treatment of relativity. It enables isolation of the tensor contribution to the action and extraction of kinetic and gradient coefficients. The construction incorporates the lag coupling from eight-tick resonance and phi-ladder scales, fitting the framework's derivation of three spatial dimensions from the J-functional and Recognition Composition Law. With no downstream uses recorded, it functions as preparatory scaffolding for wave propagation results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.