module module

`IndisputableMonolith.Masses.ExcitationOrdering`

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

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

IndisputableMonolith.Masses.TorsionForcing module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Masses.GenerationTorsionBridge module_import

declarations in this module (35)

inductive CubeCell L62
def subcellCount L75
theorem subcellCount_vertex L80
theorem subcellCount_edge L81
theorem subcellCount_face L82
theorem edge_dim_lt_face_dim L85
theorem vertex_dim_lt_edge_dim L90
def passiveCoupling L100
theorem passiveCoupling_vertex L105
theorem passiveCoupling_edge L106
theorem passiveCoupling_face L107
theorem passiveCoupling_edge_pos L109
theorem passiveCoupling_face_pos L110
def cwCumulativeTorsion L120
theorem cwTorsion_first L125
theorem cwTorsion_second L126
theorem cwTorsion_third L127
theorem cwTorsion_eq_generationTorsion L130
theorem first_increment_is_passive_edges L143
theorem second_increment_is_faces L149
theorem cwTorsion_cubeAdmissible L156
theorem Jcost_strict_mono_pos L169
def excitationCost L187
theorem excitationCost_ground L190
theorem excitationCost_pos_of_ne_zero L194
theorem excitationCost_strictMono L202
theorem excitation_cost_ordering L211
structure ExcitationOrderingTheorem L240
theorem excitation_ordering_holds L258
theorem edge_is_minimal_nontrivial_excitation L275
theorem ordering_is_dimensional_not_numerical L292
theorem cwTorsion_incremental L302
theorem cwTorsion_has_filtration L308
theorem excitation_ordering_implies_filtration L314
theorem excitation_ordering_certificate L337