expand_action_around_FRW
plain-language theorem explainer
The definition asserts that the action expansion around the FRW background holds identically for a given scale factor, scalar field, and parameters alpha and C_lag. Cosmologists working on tensor perturbations within the Recognition Science framework would reference it when constructing effective actions for gravitational waves. The implementation is a direct assignment to the true proposition, serving as a placeholder without invoking lemmas or reductions.
Claim. Let $a(t)$ be a positive scale factor and let $ψ$ be a scalar field on spacetime. For real parameters $α$ and $C_{lag}$, the expansion of the action around the FRW metric is the proposition that holds unconditionally.
background
ScaleFactor is the structure consisting of a function $a : ℝ → ℝ$ together with the positivity condition $∀ t, 0 < a t$, representing the cosmological scale factor in the FRW metric. ScalarField is the structure that assigns a real value to each point in four-dimensional spacetime via a map from (Fin 4 → ℝ) to ℝ. C_lag is defined as $φ^{-5} ≈ 0.09$, the lag coupling constant taken from the eight-tick resonance. This declaration appears in the ActionExpansion module of the relativity section, which imports geometry, fields, FRW cosmology, and tensor decomposition to treat gravitational-wave actions.
proof idea
The declaration is realized by a direct definition that sets the target proposition to True. No upstream lemmas are applied and no tactics are used; it functions as a one-line placeholder.
why it matters
This definition supplies the interface for action expansion around FRW backgrounds that later supports quadratic tensor terms in the gravitational-wave module. It connects the scale factor from large-scale structure derivations and the lag coupling from eight-tick resonance to the cosmological perturbation sector of Recognition Science. It fills the slot needed for deriving effective actions while the explicit expansion formula remains to be supplied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.