x_reciprocity_log_identity
plain-language theorem explainer
The declaration proves that if an observable Q depends on wavenumber k and scale factor a only through the dimensionless combination X = k τ₀ / a, then its logarithmic derivatives obey ∂ ln Q / ∂ ln a = − ∂ ln Q / ∂ ln k. Model builders in the ILG framework cite this identity when switching between scale derivatives and wavenumber derivatives in reciprocity relations. The proof is a direct algebraic rearrangement of the linear X-reciprocity identity using field simplification and linear combination.
Claim. Let $Q(a,k) = Q̃(X)$ where $X = k τ₀ / a$. Then $(a/Q) ∂Q/∂a = −(k/Q) ∂Q/∂k$, provided $Q ≠ 0$ at the evaluation point and $Q̃$ is differentiable there.
background
The ILG module defines the dimensionless variable $X = k τ₀ / a$ via X_var, where τ₀ is the fundamental tick duration from Constants. A function Q(a,k) satisfies X-reciprocity when it factors as Q(a,k) = Q̃(X) for some Q̃. The upstream theorem x_reciprocity_identity states: if Q depends only on X then a ∂Q/∂a = −k ∂Q/∂k. This module develops reciprocity properties for observables controlled by X in the ILG setting.
proof idea
The proof invokes the linear identity x_reciprocity_identity, performs dsimp to unfold the let-binding for Q, applies field_simp under the positivity hypothesis hQpos, and finishes with linear_combination to rearrange into the logarithmic form.
why it matters
This supplies the logarithmic counterpart to the linear X-reciprocity identity in the ILG.Reciprocity module. It encodes the scale-wavenumber reciprocity that follows from dependence on X alone and supports derivative manipulations in ILG models. No downstream uses are recorded, but it completes the basic reciprocity toolkit alongside the linear form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.