BackreactionCert
plain-language theorem explainer
BackreactionCert bundles three conditions confirming that ILG yields zero Buchert backreaction, obeys X-reciprocity for derivatives of X-only observables, and meets PPN safety bounds at the paper's quoted thresholds. Cosmologists testing modified-gravity or dark-energy models against growth, lensing, and local gravity data would cite it to document consistency with GR limits. The declaration is a plain structure definition that assembles the three fields without any proof steps.
Claim. A certificate asserting $Q_D = 0$ for the Buchert backreaction scalar, the reciprocity relation $dQ/d$ln$a = -dQ/d$ln$k$ for any observable depending on $X = k$tau$_0/a$ under the increments $dX_a = -1$, $dX_k = 1$, and the PPN safety bound holding for $X_mathrm{safe} = 3 times 10^{24}$ and $epsilon = 10^{-5}$.
background
The module formalizes results from the ILG dark-energy paper. ILG alters only the source density (rho_b to w rho_b) while leaving the metric and expansion rate unchanged, so the velocity field remains irrotational potential flow and the Buchert scalar Q_D vanishes identically. X-reciprocity follows because any observable Q(X) satisfies ln X = ln k + ln tau_0 - ln a, forcing the logarithmic derivatives at fixed a and fixed k to be exact negatives of each other.
proof idea
The declaration is a structure definition with an empty proof body. It directly records the three fields: the constant zero from buchert_Q_D_ilg, the implication that invokes X_reciprocity on the scaled increments, and the proposition ppn_safe instantiated at the numerical bounds supplied by the paper.
why it matters
BackreactionCert supplies the type for the downstream theorem backreaction_cert, which constructs an explicit instance using buchert_backreaction_zero, X_reciprocity_from_chain_rule and ppn_safety_bound. It encodes the three core claims of the module (zero backreaction for potential-flow sources, X-reciprocity, and recovery of GR in the large-X limit) and thereby anchors the gravity sector of Recognition Science to the T8 spatial-dimension and RCL consistency requirements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.