`ImaginaryUnitFalsifier`

definition

show as: view math explainer →

module: IndisputableMonolith.Mathematics.ImaginaryUnit
domain: Mathematics
line: 225 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.ImaginaryUnit on GitHub at line 225.

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

 222    1. i² ≠ -1 (impossible, it's definitional)
 223    2. Physics didn't need complex numbers (many alternatives tried, all failed)
 224    3. 8-tick structure not fundamental -/
 225structure ImaginaryUnitFalsifier where
 226  i_squared_not_neg1 : Prop
 227  physics_no_complex : Prop
 228  eight_tick_not_fundamental : Prop
 229  falsified : i_squared_not_neg1 → False  -- This is definitionally false
 230
 231end ImaginaryUnit
 232end Mathematics
 233end IndisputableMonolith

papers checked against this theorem

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