x_reciprocity_identity
plain-language theorem explainer
The X-reciprocity identity states that if Q depends only on the dimensionless variable X = k τ₀ / a then a times the partial derivative of Q with respect to a equals minus k times the partial with respect to k. Workers on ILG growth equations cite this when establishing scaling symmetries for the growth factor. The proof applies the chain rule twice to the compositions defining the partials and reduces the resulting algebraic expression with field simplification and ring tactics.
Claim. If a function Q(a, k) depends on a and k only through the dimensionless variable X = k τ₀ / a, i.e., Q(a, k) = Q̃(X) for a differentiable function Q̃, then a (∂Q/∂a) = -k (∂Q/∂k).
background
The ILG module defines the dimensionless variable via X_var(k, a, tau0) = k * tau0 / a. Module documentation identifies this as the central ILG dimensionless variable X = k * tau0 / a. Upstream results include multiple definitions of tau0 as the fundamental tick duration, derived from hbar, G and c in RS-native units, together with structures for nuclear densities and ledger factorization that justify the use of such ratios. Any Q expressible as a function of X alone obeys the stated derivative relation under the given differentiability assumption.
proof idea
The tactic script sets X to the value of X_var and defines f_a and f_k as the reparameterized maps. It rewrites each as a composition, invokes deriv_comp with the supplied differentiability of Q_tilde and the inner function's differentiability (established by const_div or div_const), then simplifies the inner derivatives. The two results are inserted into the goal and the equality is obtained by field_simp and ring.
why it matters
This identity is applied in growth_x_reciprocity to verify the relation for the ILG growth factor D and in x_reciprocity_log_identity to derive the logarithmic counterpart. It encodes the scaling invariance forced by dependence on the single variable X, aligning with the phi-forcing and self-similar structure in the Recognition framework. The theorem is fully proved with no remaining hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.