X_reciprocity
plain-language theorem explainer
X-reciprocity encodes the relation that the logarithmic derivative of an observable with respect to scale factor at fixed wavenumber equals the negative of the derivative with respect to wavenumber at fixed scale, for any quantity depending on those variables only through X = k τ₀ / a. Cosmologists auditing ILG dark-energy kernels would cite this when verifying derivative consistency between scale and time domains. The definition is a direct equality statement with no further reduction steps.
Claim. Let $dQ_{dlna}$ and $dQ_{dlnk}$ denote the logarithmic derivatives of an observable $Q$ that depends on wavenumber $k$ and scale factor $a$ only through the combination $X = k τ_0 / a$. X-reciprocity is the statement $dQ_{dlna} = -dQ_{dlnk}$.
background
The BackreactionAudit module formalizes results from the paper on ILG Source-Side Kernel Tests Against Distances, Growth, and Lensing. It lists X-reciprocity among the core results together with zero Buchert backreaction and PPN safety in the large-X limit. X is the dimensionless ratio X = k τ₀ / a that controls the argument of ILG observables. The upstream reciprocity theorem from LedgerForcing states that the cost of an event equals the cost of its reciprocal.
proof idea
This is a definition that directly sets the proposition X_reciprocity to the equality dQ_dlna = -dQ_dlnk. The downstream theorem X_reciprocity_from_chain_rule applies it by unfolding the definition and confirming the equality via the ring tactic once the chain-rule values dX_dlna = -1 and dX_dlnk = 1 are substituted.
why it matters
X_reciprocity supplies the reciprocity clause required inside the BackreactionCert structure that certifies zero backreaction for ILG models. It implements the module's stated core result that scale slopes at fixed z mirror time slopes in the same k-bins. The definition connects to the Recognition Science forcing chain through the reciprocity lemma from LedgerForcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.