`IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4DAudit`

IndisputableMonolith/Gravity/Analysis/OrderSensitiveHistoryResponse4DAudit.lean · 18 lines · 0 declarations

Explainer status: ready · generated 2026-08-16 00:57:41.946378+00:00

   1import IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D
   2
   3/-!
   4Axiom audit for OrderSensitiveHistoryResponse4D. Load-bearing finite gate must
   5report the base triple (or a subset). Reject silent `sorryAx`.
   6-/
   7
   8open IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D
   9
  10#print axioms fingerprint_separates_cfgAB
  11#print axioms historyResponse_separates_cfgAB
  12#print axioms finiteCertificate_cfgAB
  13#print axioms edgeAction_separates_cfgAB
  14#print axioms responseDiff_cfgAB_not_in_MetricEdgeImage
  15#print axioms orderSensitive_finite_gate_cfgAB
  16#print axioms decoy_depthOne_blind
  17#print axioms discovery_pair_is_certificate_cfgAB
  18

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