IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloserAudit
IndisputableMonolith/Gravity/Analysis/Regge4DTransportedAlgebraicCloserAudit.lean · 32 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.Analysis.Regge4DTransportedAlgebraicCloser
2
3/-!
4Axiom / honesty audit for `Regge4DTransportedAlgebraicCloser`.
5Expected footprint: `[propext, Classical.choice, Quot.sound]`.
6-/
7
8namespace IndisputableMonolith
9namespace Gravity
10namespace Analysis
11namespace Regge4DTransportedAlgebraicCloserAudit
12
13open Regge4DTransportedAlgebraicCloser
14
15#print axioms finiteTransportedSymbol_eq_blochFoldAll
16#print axioms continuumSymbolIs_unique_limit
17#print axioms finiteTransportedSymbol_eq_orbit_sum
18#print axioms finiteTransportedSymbol_smul
19#print axioms finiteTransportedSymbol_zero
20#print axioms t11_foldAlong_m2_tendsto_axisTTPlus
21#print axioms t11_foldAlong_m2_tendsto_decoyGauge
22#print axioms oneOrbitRayNormalizedCoeff_axisTTPlus
23#print axioms oneOrbit_ray_normalized_ne_eh_coefficient
24#print axioms transported_targets_eq_preflight
25#print axioms regge4DTransportedAlgebraicCloserStatus_flags
26#print axioms banked_does_not_inhabit_eh_or_flip_gap
27
28end Regge4DTransportedAlgebraicCloserAudit
29end Analysis
30end Gravity
31end IndisputableMonolith
32