theorem proved term proof

`backreaction_cert`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 117theorem backreaction_cert : BackreactionCert where
 118  Q_D_zero := buchert_backreaction_zero

proof body

Term-mode proof.

 119  reciprocity := X_reciprocity_from_chain_rule
 120  ppn_ok := ppn_safety_bound
 121
 122end
 123
 124end BackreactionAudit
 125end Gravity
 126end IndisputableMonolith

depends on (5)

Lean names referenced from this declaration's body.

reciprocity in IndisputableMonolith.Foundation.LedgerForcing decl_use
BackreactionCert in IndisputableMonolith.Gravity.BackreactionAudit decl_use
buchert_backreaction_zero in IndisputableMonolith.Gravity.BackreactionAudit decl_use
ppn_safety_bound in IndisputableMonolith.Gravity.BackreactionAudit decl_use
X_reciprocity_from_chain_rule in IndisputableMonolith.Gravity.BackreactionAudit decl_use