IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKillAudit
IndisputableMonolith/Gravity/SevenGaps/HKTVacuumSectorKillAudit.lean · 29 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill
2
3open IndisputableMonolith.Gravity.SevenGaps.HKTVacuumSectorKill
4open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
5open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
6
7#check vacuumShiftCanonicalMomTarget
8#check not_HKTRigidityStatementPointSplitDynN2Canonical
9#check HKTRigidityModVacuumStatementN2
10#check vacuumShift_satisfies_modVacuum
11#check hamDyn_satisfies_modVacuum
12#check Note_modVacuumKilledInC4
13#check hktVacuumSectorKillStatus_flags
14
15#print axioms not_HKTRigidityStatementPointSplitDynN2Canonical
16#print axioms vacuumShift_satisfies_modVacuum
17#print axioms hamDyn_satisfies_modVacuum
18#print axioms hktVacuumSectorKillStatus_flags
19
20example : fullTheoryBenchmarks.gap5_constraint_recovery = true := rfl
21example : hktVacuumSectorKillStatus.canonicalMomRigidityKilled = true := rfl
22example : hktVacuumSectorKillStatus.modVacuumRigidityOpen = false := rfl
23example : hktVacuumSectorKillStatus.gap5ConstraintRecovery = false := rfl
24
25-- Mod-vacuum statement remains DEFINED here; C4 kills it in
26-- `HKTKineticNormalizedRigidity`.
27#check HKTRigidityModVacuumStatementN2
28#check HKTRigidityStatementPointSplitDynN2Canonical
29