growth_x_reciprocity
plain-language theorem explainer
The growth_x_reciprocity theorem shows that the normalized ILG growth factor Q(a, k) = D(a, k)/a obeys the reciprocity relation a ∂_a Q = −k ∂_k Q at fixed values of the other variable. Researchers deriving first-order corrections to the growth equation in Recognition Science cosmology would reference this identity when confirming consistency of the EdS-background solution. The proof proceeds by rewriting Q in terms of an auxiliary function Q_tilde of the single variable X = k τ₀ / a, verifying differentiability, and invoking the general x_rec
Claim. Let $D(a,k)$ be the ILG growth factor in an Einstein-de Sitter background. Define the normalized factor $Q(a,k) := D(a,k)/a$. Then for $a>0$ and $k>0$, $a$ times the partial derivative of $Q$ with respect to $a$ (at fixed $k$) equals $-k$ times the partial derivative of $Q$ with respect to $k$ (at fixed $a$).
background
The module derives the prefactor for the first-order ILG growth correction in an EdS background by substituting the ansatz $D = a(1 + B (a/(k τ_0))^α)$ into the growth ODE. KernelParams packages the model constants including the exponent α and the prefactor parameter C; growth_prefactor computes B from these. τ₀ is the fundamental tick duration supplied by Constants.tau0 and its positivity lemma. The upstream x_reciprocity_identity lemma from the Reciprocity module supplies the general algebraic relation specialized here to the explicit growth form.
proof idea
The proof extracts B via growth_prefactor, defines the auxiliary Q_tilde(x) = 1 + B (1/x)^α, and proves by field simplification that growth_eds_ilg P k' a' / a' equals Q_tilde(X_var k' a' P.tau0) whenever a' and k' are positive. Differentiability of Q_tilde at the evaluation point follows from composing differentiable operations (constant addition, multiplication by constant, and real-power). The claim is discharged by a direct call to the lemma x_reciprocity_identity on Q_tilde, a, and k.
why it matters
This theorem completes the verification of the X-reciprocity property for the explicit first-order ILG growth solution in EdS cosmology (Target C). It relies on the general reciprocity identity from the Reciprocity module and on the explicit construction of growth_eds_ilg. Within the Recognition Science framework it supports consistency checks for the phi-ladder-derived correction term, although the used_by count is currently zero and no parent theorem yet invokes it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.