IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4DAudit
IndisputableMonolith/Gravity/Analysis/ReggeBlochLocalIncidence4DAudit.lean · 19 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D
2import IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D
3
4/-!
5# Audit: Path B local-incidence fold
6-/
7
8#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D.orbitMeanLocalKernel_t11_eq_assembled_mean
9#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D.blochFoldAllMeanLocal_eq_distinctHinge
10#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D.m2MeanLocalAllOrbitMoment_eq_distinctHinge
11#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D.t11_member_sum_eq_fullStar
12#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D.Regge4DPathBPositionResolvedClosesEH_status_open
13#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidence4D.does_not_flip_gap_action_recovery
14#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D.pathB_vs_distinctHinge_witness_table
15#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D.meanLocal_pinned_face_ne_eh
16#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D.m2PathB_meanLocal_plus_cross_disagree_e0Dir
17#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D.pathB_positionResolved_does_not_close_eh
18#print axioms IndisputableMonolith.Gravity.Analysis.ReggeBlochLocalIncidenceM2Eval4D.does_not_flip_gap_action_recovery
19