IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceSilenceVerdictProbe

   1import IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceSilenceVerdict
   2
   3/-!
   4# Outside-module probe for Gap2 incidence-silence verdict
   5-/
   6
   7open IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceSilenceVerdict
   8open IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation
   9open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
  10
  11#check fixedKindTotals_not_forced_in_letter_cost
  12#check ledger_does_not_force_countsOnly
  13#check incidenceSilenceVerdictCert
  14#check namedFurtherPremises
  15
  16example :
  17    CostSizeBlind pairCost ∧ ¬ FixedKindTotals pairCost :=
  18  ⟨fixedKindTotals_not_forced_in_letter_cost.2.1,
  19    fixedKindTotals_not_forced_in_letter_cost.2.2⟩
  20
  21example : fullTheoryBenchmarks.gap2_measure_derived = true :=
  22  gap2_measure_derived_unmoved
  23
  24example : IncidenceSilenceVerdictCert :=
  25  incidenceSilenceVerdictCert
  26
  27example :
  28    namedFurtherPremises.schedule_law =
  29      "CountsOnlySchedule: law about the actual posting run, not the space of runs" :=
  30  rfl
  31