pith. machine review for the scientific record. sign in
theorem proved term proof

common_constants_fail_selection

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

formal statement (Lean)

 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

proof body

Term-mode proof.

 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

depends on (15)

Lean names referenced from this declaration's body.