IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTargetAudit
IndisputableMonolith/Gravity/SevenGaps/HKTCanonicalMomTargetAudit.lean · 25 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
2
3open IndisputableMonolith.Gravity.SevenGaps.HKTCanonicalMomTarget
4open IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong
5open IndisputableMonolith.Gravity.SevenGaps.FullTheoryLedger
6
7#check quarticBalancedStrongTarget
8#check not_HKTRigidityStatementPointSplitDynN2Strong
9#check HKTPointSplitTargetDynCanonicalMom
10#check hamDynPointSplitTargetCanonicalMom
11#check canonicalMom_excludes_balanced_quartic
12#check HKTRigidityStatementPointSplitDynN2Canonical
13#check hktCanonicalMomStatus_flags
14
15#print axioms not_HKTRigidityStatementPointSplitDynN2Strong
16#print axioms quarticBalanced_mom_load_bearing_witness
17#print axioms quarticBalanced_fails_canonical_mom
18#print axioms canonicalMom_excludes_balanced_quartic
19#print axioms hktPointSplitTargetDynCanonicalMom_nonvacuous
20#print axioms hktCanonicalMomStatus_flags
21
22example : fullTheoryBenchmarks.gap5_constraint_recovery = true := rfl
23example : ¬ HKTRigidityStatementPointSplitDynN2Strong :=
24 not_HKTRigidityStatementPointSplitDynN2Strong
25