module module

`IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracket`

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 (7)

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

IndisputableMonolith.Gravity.SevenGaps.DiracAlgebraContinuum module_import
IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketAudit module_import
IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketN module_import
IndisputableMonolith.Gravity.SevenGaps.DynamicStructureContinuumSmearing module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5ConstraintResidualDAG module_import
IndisputableMonolith.Gravity.SevenGaps.Gap5MomentumMagnitudeBridge module_import
IndisputableMonolith.Gravity.SevenGaps.HKTPointSplitTarget module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureFunctionBlocker module_import

declarations in this module (22)

def naiveDynamicHamW L39
def HamDyn L43
theorem HamDyn_eq_naive L49
def decoyPhasePoint L61
def decoyLapse L66
lemma decoyLapse_zero L69
lemma decoyLapse_one L72
lemma decoy_q_zero L75
lemma decoy_q_one L78
lemma zmod2_zero_sub_one L81
lemma zmod2_zero_add_one L84
def HamDynD L91
lemma hasFDerivAt_HamDyn L101
theorem pderivP_HamDyn L113
theorem pderivQ_HamDyn L134
theorem TypedResidual_naive_dynamic_HamW_decoy_fails L174
theorem differentiable_HamDyn L194
theorem bracket_HamDyn_HamDyn L200
def concreteDynamicHamiltonianConstruction L234
def TypedResidual_dynamic_bracket_concrete_two_site L241
theorem typedResidual_dynamic_bracket_concrete_two_site L244
theorem phaseSpaceDependentDiracPremise_two_site L249