module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LatticeKindRule`

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.Gravity.SevenGaps.Gap2DynamicsKindRule module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule module_import

declarations in this module (20)

structure LatticeCost L76
def strain L84
def toLetterCost L88
def pairMagLattice L104
theorem pairMagLattice_strain_vertex L123
theorem pairMagLattice_mag_reads_count L137
def incidencePhiLattice L149
theorem incidencePhiLattice_toLetterCost_eq L168
theorem incidencePhiLattice_not_countsOnly L190
theorem lattice_does_not_force_counts_only L202
def LatticeChargesCountsOnly L221
theorem lattice_forces_flux_unit L239
def magReadsIncidenceLattice L250
theorem magReadsIncidenceLattice_strain_edge L278
theorem magReadsIncidenceLattice_strain_exceeds_flux L293
theorem dual_premise_conjuncts_independent L304
structure LatticeIndex L336
def latticeIndex L355
theorem index_lattice_not_forced L364
theorem index_dynamics_open L366