IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumAudit
IndisputableMonolith/Gravity/SevenGaps/DiracAlgebraContinuumAudit.lean · 34 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum
2
3/-!
4# Axiom audit: Wave C2 R4 dynamic bracket shape continuum
5
6Ledger name `dirac_algebra_continuum_limit` is held free pending HamDynN
7binding repair. Audit the real rate-`h` / shape theorems.
8
9Headline theorems must print within
10`[propext, Classical.choice, Quot.sound]`.
11-/
12
13open IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum
14
15#check continuumWronskian
16#check continuumMomentumFlux
17#check continuumDiracDensity
18#check sampledDynamicBracketSum
19#check discrete_wronskian_mvt
20#check wronskian_rate_h_tendsto
21#check forward_diff_mvt
22#check forward_density_uniform
23#check dynamic_bracket_shape_continuum_limit
24#check frozen_structure_differs_from_dynamic_id
25#check frozen_continuum_density_differs_from_dynamic
26
27#print axioms discrete_wronskian_mvt
28#print axioms wronskian_rate_h_tendsto
29#print axioms forward_diff_mvt
30#print axioms forward_density_uniform
31#print axioms dynamic_bracket_shape_continuum_limit
32#print axioms frozen_structure_differs_from_dynamic_id
33#print axioms frozen_continuum_density_differs_from_dynamic
34