`IndisputableMonolith.Gravity.RecordFluxBoostHeatAudit`

IndisputableMonolith/Gravity/RecordFluxBoostHeatAudit.lean · 14 lines · 0 declarations

Explainer status: pending

   1import IndisputableMonolith.Gravity.RecordFluxBoostHeat
   2
   3/-!
   4Axiom audit for conditional posted-record heat to null stress transport.
   5-/
   6
   7open IndisputableMonolith.Gravity.RecordFluxBoostHeat
   8
   9#print axioms exteriorStepHeat_cast_eq_sum_channelDelta
  10#print axioms quadContr_cutEventStress_eq_sq_mul_heat
  11#print axioms matchesPostedBoostHeat_of_attachment
  12#print axioms zero_covectors_fail_nonzero_posted_heat
  13#print axioms recordFluxBoostHeatCert
  14

source mirrored from github.com/jonwashburn/shape-of-logic