module module

`IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBinding`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuumBindingAudit module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintCloseStatus module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum module_import
IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketN module_import

declarations in this module (17)

def sampledPhasePoint L40
def sampledLapse L44
def wrapSucc L48
def periodicSampledDynamicBracketSum L52
def continuumLatticeBracket L61
lemma zmod_val_of_lt L70
lemma wrapSucc_lt L74
lemma zmod_succ_val L80
lemma sum_zmod_eq_sum_range L94
theorem bracket_HamDynN_eq_periodicSampled L106
theorem continuumLatticeBracket_eq_periodic L121
def Periodic1 L135
lemma wrapSucc_eq_succ_or_zero L141
theorem periodicSampled_eq_sampled_of_periodic L150
theorem scaled_continuumLatticeBracket_eq_scaled_sampled L169
theorem dirac_algebra_continuum_limit L184
theorem dirac_algebra_continuum_limit_hamDynN L199