Gravity Backreaction Audit X Reciprocity From Chain Rule

X-reciprocity

In the Recognition Science framework's model of gravity, the dimensionless variable X = k·τ₀/a controls the transition between a modified regime at small X and ordinary general relativity at large X. Here k is a spatial scale, a is the cosmic scale factor, and τ₀ is a constant. The theorem X_reciprocity_from_chain_rule proves a precise symmetry: for any observable that depends on (k, a) only through X, the logarithmic derivative with respect to the scale factor at fixed k equals the negative of the logarithmic derivative with respect to k at fixed a. In symbols: d(ln Q)/d(ln a)|_k = −d(ln Q)/d(ln k)|_a.

The proof is a direct application of the chain rule. Since ln X = ln k + ln τ₀ − ln a, the derivative of ln X with respect to ln k at fixed a is 1, and with respect to ln a at fixed k is −1. The theorem takes these two facts as hypotheses and concludes the reciprocity relation for any differentiable function Q(X). It is a formal, machine-checked statement in the framework's library of theorems.

The theorem does not claim that any particular physical observable actually has this property. It establishes a conditional statement: if an observable is a function of X alone, then reciprocity follows. Whether a real cosmological observable like the growth rate or the lensing statistic E_G is such a function of X is a separate, empirical question. The framework's library also contains a certificate structure that packages this theorem with the zero backreaction result and the PPN safety bound, but the certificate itself is a definition, not a proof of physical reality.

The practical consequence is a clean test. If a survey measures a scale-dependent signal and a time-dependent signal, and both are governed by the same X, then the two slopes must be opposite in sign and equal in magnitude. A violation of that relation would indicate that the observable is not purely X-dependent, or that the ILG model is wrong. The theorem gives the prediction; the data gives the verdict.

/-- X-reciprocity holds by construction for X-only observables. -/
theorem X_reciprocity_from_chain_rule (dQ_dX dX_dlna dX_dlnk : ℝ)
    (h_a : dX_dlna = -1) (h_k : dX_dlnk = 1) :
    X_reciprocity (dQ_dX * dX_dlna) (dQ_dX * dX_dlnk) := by
  unfold X_reciprocity
  rw [h_a, h_k]; ring

/-- X-reciprocity holds by construction for X-only observables. -/
theorem X_reciprocity_from_chain_rule (dQ_dX dX_dlna dX_dlnk : ℝ)
    (h_a : dX_dlna = -1) (h_k : dX_dlnk = 1) :
    X_reciprocity (dQ_dX * dX_dlna) (dQ_dX * dX_dlnk) := by
  unfold X_reciprocity
  rw [h_a, h_k]; ring

/-- X-reciprocity holds by construction for X-only observables. -/
theorem X_reciprocity_from_chain_rule (dQ_dX dX_dlna dX_dlnk : ℝ)
    (h_a : dX_dlna = -1) (h_k : dX_dlnk = 1) :
    X_reciprocity (dQ_dX * dX_dlna) (dQ_dX * dX_dlnk) := by
  unfold X_reciprocity
  rw [h_a, h_k]; ring

What this page does not claim

No physical observable is asserted to be X-dependent. No claim is made that the ILG model is the correct theory of gravity. The theorem does not establish that the backreaction scalar Q_D is zero in any real cosmological domain.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/BackreactionAudit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: