module module

`IndisputableMonolith.Foundation.DistinctionToT4`

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.Foundation.LedgerFloorT0Bridge module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.TMinus1ForcedFromDistinction module_import
IndisputableMonolith.Foundation.UnifiedForcingChain module_import

declarations in this module (22)

abbrev ForcedQuotient L45
def forcedQuotientBoolEquiv L49
instance forcedQuotientConfigSpace L59
theorem forcedQuotientBoolEquiv_emp L122
theorem forcedQuotientBoolEquiv_join L129
def forcedQuotientRecognitionCost L145
theorem forcedQuotientRecognitionCost_transport L170
theorem forcedQuotient_recognition_work_constraint L178
structure T0_FromDistinction L188
theorem distinction_forces_T0 L219
structure T1_FromDistinction L242
theorem distinction_T0_to_T1 L260
theorem distinction_forces_T1 L272
structure T2_FromDistinction L280
theorem distinction_T1_to_T2 L303
theorem distinction_forces_T2 L352
structure T3_FromDistinction L360
theorem distinction_T0_T2_to_T3 L386
theorem distinction_forces_T3 L400
structure DistinctionToT0_Spine L419
theorem distinction_forces_T0_spine L440
theorem distinction_forces_T0_to_T3 L452