`common_constants_fail_selection`

proved

show as: view math explainer →

module: IndisputableMonolith.PhiSupport.Alternatives
domain: PhiSupport
line: 190 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.PhiSupport.Alternatives on GitHub at line 190.

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

 187
 188/-- Bundle theorem: All tested common constants fail PhiSelection.
 189    This demonstrates that φ is not an arbitrary choice from among "nice" constants. -/
 190theorem common_constants_fail_selection :
 191  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.exp 1) ∧
 192  ¬IndisputableMonolith.RecogSpec.PhiSelection Real.pi ∧
 193  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 2) ∧
 194  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 3) ∧
 195  ¬IndisputableMonolith.RecogSpec.PhiSelection (Real.sqrt 5) := by
 196  exact ⟨e_fails_selection, pi_fails_selection, sqrt2_fails_selection,
 197         sqrt3_fails_selection, sqrt5_fails_selection⟩
 198
 199/-! ### Uniqueness emphasis
 200
 201Combined with phi_unique_pos_root from PhiSupport.lean, these results show:
 2021. φ is the ONLY positive solution to x² = x + 1 (constructive uniqueness)
 2032. Common alternatives (e, π, √2, √3, √5) all fail the criterion (exclusion)
 2043. Therefore φ is mathematically forced, not chosen by fitting
 205-/
 206
 207end Alternatives
 208end PhiSupport
 209end IndisputableMonolith

papers checked against this theorem

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