module module

`IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability`

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

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

IndisputableMonolith module_import
IndisputableMonolith.Foundation.DomainBootstrap module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.AbsoluteFloorClosure module_import
IndisputableMonolith.Foundation.LogicAsFunctionalEquation module_import

declarations in this module (18)

def Distinguishability L43
theorem nonTrivial_of_distinguishability L48
theorem distinguishability_of_nonTrivial L71
theorem nonTrivial_iff_distinguishability L82
structure SatisfiesLawsOfLogicCanonical L91
theorem canonical_iff_existing L100
abbrev PositiveRatio L130
structure SatisfiesLawsOfLogicAbsoluteFloor L135
theorem distinguishability_of_absoluteFloor L145
theorem canonical_of_absoluteFloor L153
theorem existing_of_absoluteFloor L165
def constZero L185
theorem constZero_identity L188
theorem constZero_nonContradiction L192
theorem constZero_continuous L196
theorem constZero_scaleInvariant L201
theorem constZero_not_distinguishable L205
theorem constZero_not_nonTrivial L210