IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrongAudit
IndisputableMonolith/Gravity/SevenGaps/HKTPointSplitStrongAudit.lean · 24 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong
2
3open IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitStrong
4open IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget
5
6#check HKTPointSplitTargetDynStrong
7#check HKTRigidityStatementPointSplitDynN2Strong
8#check quarticZeroMomTarget
9#check quarticZeroMomTarget_not_strong
10#check hamDynPointSplitTargetStrong
11#check hktPointSplitTargetDynStrong_two_nonvacuous
12#check strong_target_discriminates_decoy
13#check UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn
14#check unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam
15
16#print axioms hamAdvFrom_eq_computed
17#print axioms hamAdvTo_eq_computed
18#print axioms quarticZeroMomTarget_not_strong
19#print axioms hamDyn_mom_load_bearing_witness
20#print axioms hamDyn_kinetic_regular_witness
21#print axioms hktPointSplitTargetDynStrong_two_nonvacuous
22#print axioms strong_target_discriminates_decoy
23#print axioms unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam
24