module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerSiteBlindness`

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.GaugeCountingInevitableReasons module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.RecognitionLedger module_import
IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker module_import

declarations in this module (20)

abbrev twoPointOneEdge L62
instance instSubsingletonAutOneEdge L76
theorem autCard_twoPointOneEdge L97
theorem mu_twoPointOneEdge L102
def siteSymCard L114
theorem cost_offDiag_fin2 L121
theorem every_perm_is_siteSym L131
theorem siteSymCard_fin2 L142
theorem no_siteSymmetry_measure L163
theorem witnesses_agree_on_ledger_disagree_on_measure L188
def uniformLedger L216
theorem uniformLedger_offDiag L228
theorem encoding_unconstrained L236
theorem value_route_is_encoding_choice L253
def uniformLedger3 L281
theorem uniform3_siteSym L295
def dcost L304
def distinctLedger L316
theorem swap01_not_siteSym_distinct L327
theorem siteSymmetry_is_chosen_by_the_encoding L349