IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureStatusBindingAudit

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureStatusBinding
   2
   3/-!
   4# Axiom audit: measure status retraction (2026-07-26)
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8
   9Renamed from the Wave C1 R6 binding audit. The audited theorems now record
  10that the two measure-side status Bools are `false` and that the R6 witness is
  11parameter-inert, rather than that the Bools are `true`.
  12-/
  13
  14open IndisputableMonolith.Gravity.SevenGaps.Gap2MeasureStatusBinding
  15open IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure
  16open IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight
  17
  18#check gap2_measure_status_retracted
  19#check history_discharge_is_prior_theorem_rewritten
  20#check historyMeasure_is_parameter_inert
  21#check historyCarrier_equiv_plainCarrier
  22#check historyMeasure_is_the_old_measure
  23#check continuum_limit_still_open
  24#check gap2_rollup_closed_after_flag9
  25#check status_substrate_measure_open
  26#check status_counting_principle_open
  27
  28#print axioms gap2_measure_status_retracted
  29#print axioms history_discharge_is_prior_theorem_rewritten
  30#print axioms historyMeasure_is_parameter_inert
  31#print axioms historyCarrier_equiv_plainCarrier
  32#print axioms historyMeasure_is_the_old_measure
  33#print axioms continuum_limit_still_open
  34#print axioms gap2_rollup_closed_after_flag9
  35#print axioms status_substrate_measure_open
  36#print axioms status_counting_principle_open
  37