IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4DAudit
IndisputableMonolith/Gravity/Analysis/ReggeBlochTransportedAllOrbit4DAudit.lean · 23 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D
2import IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
3
4/-!
5# Audit: transported all-orbit fold + orbit covering perm
6-/
7
8open IndisputableMonolith.Gravity.Analysis.ReggeBlochOrbitTransport4D
9open IndisputableMonolith.Gravity.Analysis.ReggeBlochTransportedAllOrbit4D
10
11#print axioms orbitCoveringPerm_covers
12#print axioms orbitCoveringPerm_t11_eq_slotTransportPerm
13#print axioms orbitCoveringPerm_spec
14#print axioms classDot_pushforward
15#print axioms phasedClassDot_pushforward
16#print axioms slotOrbitDeficitKer_t11
17#print axioms slotOrbitAreaCov_t11_eq
18#print axioms blochFoldOrbit_t11
19#print axioms m2TransportedOrbitMoment_t11
20#print axioms m2TransportedOrbitSlotCoeffFull_eq_trunc_of_ker0
21#print axioms m2TransportedOrbitSlotCoeffFull_smul
22#print axioms reggeBlochTransportedAllOrbit4DStatus_flags
23