Pith. sign in

IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumAudit

IndisputableMonolith/Gravity/SevenGaps/DiracAlgebraContinuumAudit.lean · 34 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   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

source mirrored from github.com/jonwashburn/shape-of-logic