X_reciprocity_from_chain_rule
plain-language theorem explainer
The declaration shows that X-reciprocity holds by the chain rule for any observable Q depending on k and a solely through X = k tau_0 / a. Cosmologists studying backreaction in the ILG model cite this to confirm that scale and time derivatives mirror each other as required for consistency with the paper's kernel tests. The proof is a direct term-mode reduction: unfold the reciprocity predicate, substitute the fixed derivative values -1 and 1, and simplify the resulting equality with ring.
Claim. Assume an observable $Q$ depends on the combination $X = k tau_0 / a$ only. Given the chain-rule factors $dX / d ln a = -1$ and $dX / d ln k = 1$, the reciprocity relation $dQ / d ln a = - dQ / d ln k$ holds.
background
The module formalizes results from the ILG dark-energy paper, focusing on Buchert backreaction and X-reciprocity. X-reciprocity is defined for observables Q(k,a) that depend only through X: the scale derivative at fixed a equals minus the time derivative at fixed k. This arises because ln X = ln k + ln tau_0 - ln a, yielding d ln X / d ln k = 1 and d ln X / d ln a = -1. The local setting emphasizes that ILG produces zero Buchert backreaction Q_D = 0 as a potential-flow source modification, not a metric change. Upstream results supply foundational structures such as the PrimitiveDistinction theorem (mapping seven axioms to four structural conditions) and SimplicialLedger continuum identifications, though this theorem relies primarily on the local X_reciprocity definition.
proof idea
This is a term-mode proof consisting of unfolding the definition of X_reciprocity, rewriting the hypotheses that fix dX_dlna to -1 and dX_dlnk to 1, and applying the ring tactic to verify the equality.
why it matters
The result is used directly in the backreaction_cert theorem of the same module, which packages Q_D_zero, reciprocity, and ppn_ok into a single certificate. It fills the X-reciprocity slot required by the paper's ILG source-side kernel tests. Within Recognition Science, it reinforces the consistency of the forcing chain by ensuring derivative relations align with the self-similar phi-ladder structures without introducing additional backreaction terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.