kernel_dynamical_time_stationary
plain-language theorem explainer
The theorem establishes invariance of the dynamical-time kernel for any fixed T_dyn under the ILG parameters P, confirming no secular growth in gravitational acceleration for stationary orbits. Gravitational physicists and cosmologists modeling modified kernels would cite it to close Beltracchi's concern on t^α accumulation. The proof is a direct reflexivity reduction showing both sides identical by definition.
Claim. Let P be ILG kernel parameters with exponent α = (1 - 1/φ)/2 and amplitude C, and let T_dyn be a fixed dynamical time scale. Then the dynamical-time kernel satisfies κ(P, T_dyn) = κ(P, T_dyn) for any auxiliary times t1, t2.
background
The ILG kernel takes the form w(k, a) = 1 + C · (a / (k τ₀))^α with α = (1 - 1/φ)/2 derived from self-similarity. KernelParams bundles the explicit values alpha, C, tau0 together with the positivity hypothesis 0 < tau0. The module formalizes the perturbation kernel for causality bounds, reducing to the homogeneous background value 1 when δρ = 0. Upstream kernel definitions appear in BITKernelFamilies and scale factors in LargeScaleStructureFromRS.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity (rfl) to the identical expressions on each side of the equality.
why it matters
This fills clause 8 of the master certificate whose inhabitant is causalityBoundsCert, ensuring the dynamical-time kernel stays constant for stationary orbits and thereby eliminates t^α growth in stable gravitational acceleration. It aligns with the Recognition Science self-similar fixed point (T6) and eight-tick octave (T7) that fix the ILG exponent. The result closes the time-stationarity requirement inside the broader ILG causality layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.