`IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTargetAudit`

IndisputableMonolith/Gravity/SevenGaps/HKTPointSplitTargetAudit.lean · 26 lines · 0 declarations

Explainer status: ready · generated 2026-08-17 16:08:42.470936+00:00

   1import IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget
   2
   3open IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget
   4
   5#check HKTPointSplitTargetDyn
   6#check HKTRigidityStatementPointSplitDynN2
   7#check unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam
   8#check unsplit_mom_ham_no_smooth_local_witness
   9#check UnsplitMomHamNoSmoothNearestNeighborWitnessHamDyn
  10#check forced_unsplit_partial_relation_impossible
  11#check hamDynPointSplitTarget
  12#check hktPointSplitTargetDyn_two_nonvacuous
  13#check bracket_MomDyn_MomDyn
  14#check bracket_MomDyn_HamDyn
  15#check DgenSym_eq_zero_two
  16#check zero_density_fails_nondegenerate
  17
  18#print axioms forced_unsplit_partial_relation_impossible
  19#print axioms unsplit_mom_ham_no_smooth_nearestNeighbor_witness_frozenHam
  20#print axioms unsplit_mom_ham_no_smooth_local_witness
  21#print axioms bracket_MomDyn_MomDyn
  22#print axioms bracket_MomDyn_HamDyn
  23#print axioms hktPointSplitTargetDyn_two_nonvacuous
  24#print axioms DgenSym_eq_zero_two
  25#print axioms zero_density_fails_nondegenerate
  26

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