`constZero_continuous`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability
domain: Foundation
line: 196 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability on GitHub at line 196.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 193  intro x y _ _; rfl
 194
 195/-- Constant zero is continuous on the positive quadrant. -/
 196theorem constZero_continuous : ExcludedMiddle constZero := by
 197  unfold ExcludedMiddle
 198  exact continuousOn_const
 199
 200/-- Constant zero is scale-invariant. -/
 201theorem constZero_scaleInvariant : ScaleInvariant constZero := by
 202  intro _ _ _ _ _ _; rfl
 203
 204/-- Constant zero fails distinguishability. -/
 205theorem constZero_not_distinguishable : ¬ Distinguishability constZero := by
 206  intro ⟨_, _, _, _, h⟩
 207  exact h rfl
 208
 209/-- Constant zero fails non-triviality. -/
 210theorem constZero_not_nonTrivial : ¬ NonTrivial constZero := by
 211  intro ⟨_, _, h⟩
 212  exact h rfl
 213
 214/-! ## Summary
 215
 216Move 1 closure: distinguishability is an Aristotelian content, the
 217algebraic `NonTrivial` predicate is one of its consequences under
 218scale invariance, and the only operator that satisfies all the other
 219laws but fails distinguishability is the constant-zero operator. The
 220residual posit in `SatisfiesLawsOfLogic` is therefore reducible to a
 221genuinely Aristotelian commitment, and the framework can be stated
 222canonically using `SatisfiesLawsOfLogicCanonical`. -/
 223
 224end LogicAsFunctionalEquation
 225end Foundation
 226end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.