backreaction_cert
plain-language theorem explainer
The backreaction certificate asserts that ILG yields zero Buchert backreaction, obeys X-reciprocity for opposing scale and wavenumber slopes, and satisfies the stated PPN safety bounds. Workers on source-side modifications to FLRW cosmology would cite it to separate background evolution from late-time source weighting. The proof is a term-mode construction that directly populates the three fields of the certificate structure from three prior lemmas.
Claim. The ILG model satisfies the backreaction certificate: the Buchert parameter $Q_D$ equals zero, X-reciprocity holds whenever the scale-factor differential slope is $-1$ and the wavenumber differential slope is $+1$, and the PPN safety condition is met at the bounds $3e24$ and $1e-5$.
background
The module formalizes results from the dark-energy paper on ILG source-side kernel tests. Core definitions include the Buchert backreaction parameter $Q_D$, which vanishes when ILG acts only as a potential-flow source modification rather than a metric change, and X-reciprocity, which equates scale slopes at fixed redshift to wavenumber slopes in matching $k$-bins. PPN safety requires that the post-Newtonian parameters remain within GR limits in the large-$X$ regime where the equation-of-state parameter $w$ approaches 1. Upstream, the reciprocity theorem from LedgerForcing states that the cost of an event equals the cost of its reciprocal, while the sibling lemma buchert_backreaction_zero records that $Q_D=0$ implies ILG leaves the background FLRW evolution unaltered and that late-time anomalies arise from source weighting alone.
proof idea
Term-mode construction that directly supplies the three fields of the BackreactionCert structure. The $Q_D$ zero field is taken from the reflexivity lemma buchert_backreaction_zero. The reciprocity field is taken from the chain-rule lemma X_reciprocity_from_chain_rule, which unfolds the definition and reduces the slope conditions by ring. The PPN field is taken from the norm_num construction in ppn_safety_bound.
why it matters
This declaration packages the three central ILG properties (zero Buchert backreaction, X-reciprocity, PPN safety) into a single reusable certificate. It supplies the formal backbone for the E_G factorization and monotonicity results that appear as sibling definitions in the same module. The construction closes the source-modification versus metric-modification distinction required by the dark-energy paper and aligns with the Recognition Science emphasis on ledger reciprocity and potential-flow sources rather than geometric backreaction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.