structure
definition
PiFalsifier
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Mathematics.Pi on GitHub at line 305.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
302 1. π has no 8-tick connection
303 2. φ-π relationships don't hold
304 3. 8-tick doesn't converge to circle -/
305structure PiFalsifier where
306 no_8tick_connection : Prop
307 phi_pi_wrong : Prop
308 discrete_no_limit : Prop
309 falsified : no_8tick_connection ∧ phi_pi_wrong → False
310
311end Pi
312end Mathematics
313end IndisputableMonolith