`IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketAudit`

IndisputableMonolith/Gravity/SevenGaps/DynamicStructureBracketAudit.lean · 23 lines · 0 declarations

Explainer status: ready · generated 2026-08-17 03:46:13.184066+00:00

   1import IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
   2
   3/-!
   4# Axiom audit: Wave C2 R0+R1 dynamic structure bracket
   5
   6Headline theorems must print within
   7`[propext, Classical.choice, Quot.sound]`.
   8-/
   9
  10open IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket
  11open IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker
  12
  13#check TypedResidual_naive_dynamic_HamW_decoy_fails
  14#check bracket_HamDyn_HamDyn
  15#check typedResidual_dynamic_bracket_concrete_two_site
  16#check concreteDynamicHamiltonianConstruction
  17#check phaseSpaceDependentDiracPremise_two_site
  18
  19#print axioms TypedResidual_naive_dynamic_HamW_decoy_fails
  20#print axioms bracket_HamDyn_HamDyn
  21#print axioms typedResidual_dynamic_bracket_concrete_two_site
  22#print axioms phaseSpaceDependentDiracPremise_two_site
  23

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