module module

`IndisputableMonolith.Meta.LedgerUniqueness`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Patterns.GrayCode module_import

declarations in this module (17)

def phi L54
theorem phi_satisfies_fixed_point L57
theorem phi_unique_fixed_point L64
theorem cost_fixed_point_is_phi L93
def linkingNumber L109
def H_LinkingDimensionUniqueness L117
theorem Q3_unique_linking_dimension L121
theorem cube_uniqueness L136
def grayCodeCycleLength L153
theorem eight_tick_minimal L156
theorem no_shorter_cycle L162
theorem eight_tick_is_minimal L173
structure RSLedger L183
structure DiscreteConservativeSystem L189
theorem ledger_structure_unique L195
theorem complete_ledger_uniqueness L204
theorem rs_ledger_is_unique L229