IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4DAudit
IndisputableMonolith/Gravity/Analysis/ReggeBlochTransportedAllOrbitM2Eval4DAudit.lean · 57 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D
2
3/-!
4# Audit: transported all-orbit m² evaluation certificates
5-/
6
7open IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbitM2Eval4D
8
9#print axioms m2TransportedAllOrbitMoment_axisTTPlus_symbolDir
10#print axioms M2TransportedAllOrbitAxisSymbolDirEvalOpen_holds
11#print axioms m2TransportedAllOrbitMoment_decoyGauge_symbolDir
12#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_symbolDir
13#print axioms M2DistinctHingeAxisSymbolDirEvalOpen_holds
14#print axioms m2TransportedAllOrbitMomentDistinctHinge_decoyGauge_symbolDir
15#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_symbolDir
16#print axioms m2TransportedAllOrbitMoment_axisTTCross_symbolDir
17#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_symbolDir
18#print axioms M2DistinctHingeAxisTTCrossSymbolDirEvalOpen_holds
19#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_symbolDir
20#print axioms m2TransportedDistinctHinge_plus_cross_normalized_agree_symbolDir
21#print axioms m2TransportedOrbitMoment_t11_axis
22#print axioms m2TransportedOrbitMoment_t12_axis
23#print axioms m2TransportedOrbitMoment_t13_axis
24#print axioms m2TransportedOrbitMoment_t21_axis
25#print axioms m2TransportedOrbitMoment_t22_axis
26#print axioms m2TransportedOrbitMoment_t31_axis
27#print axioms m2TransportedOrbitMoment_t11_cross
28#print axioms m2TransportedOrbitMoment_t12_cross
29#print axioms m2TransportedOrbitMoment_t13_cross
30#print axioms m2TransportedOrbitMoment_t21_cross
31#print axioms m2TransportedOrbitMoment_t22_cross
32#print axioms m2TransportedOrbitMoment_t31_cross
33#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTPlus_e0Dir
34#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTCross_e0Dir
35#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTPlusNormalized_e0Dir
36#print axioms m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_e0Dir
37#print axioms Regge4DContinuumIsotropyBlockedOnAxisMode_status_false
38#print axioms axis_mode_plus_cross_disagree_e0Dir
39#print axioms phaseScaleDir_e0Dir
40#print axioms e0Dir_normSq
41#print axioms slotOrbitKerDot_axisTTPlus
42#print axioms slotOrbitKerDot_axisTTCross
43#print axioms m2TransportedOrbitSlotCoeffFull_eq_trunc_axisTTPlus
44#print axioms m2TransportedOrbitSlotCoeffFull_eq_trunc_axisTTCross
45#print axioms m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTPlus
46#print axioms m2TransportedAllOrbitMomentDistinctHingeFull_eq_trunc_axisTTCross
47#print axioms m2TransportedAllOrbitMomentDistinctHingeFull_axisTTPlus_e0Dir
48#print axioms m2TransportedAllOrbitMomentDistinctHingeFull_axisTTCross_e0Dir
49#print axioms m2TransportedAllOrbitMomentDistinctHingeFull_axisTTPlus_symbolDir
50#print axioms m2TransportedAllOrbitMomentDistinctHingeFull_axisTTCross_symbolDir
51#print axioms full_twojet_does_not_repair_e0_anisotropy
52#print axioms Regge4DFullTwoJetRestoresE0PlusVanishing_status_false
53#print axioms Regge4DFullTwoJetRestoresE0Isotropy_status_false
54#print axioms continuumFace_fullTwoJet_normalizedCross_e0Dir
55#print axioms full_twojet_does_not_flip_gap_action_recovery
56#print axioms reggeBlochFullTwoJetM2Eval4DStatus_flags
57