# Proof: The positive root of x² - x - 1 = 0 is exactly (1 + √5)/2

- **Generated**: 2026-03-28
- **Verdict**: **PROVED**
- **Audit trail**: [proof_audit.md](proof_audit.md) | [proof.py](proof.py)

## Key Findings

- Substituting φ = (1 + √5)/2 into x² - x - 1 yields exactly 0, verified via exact integer arithmetic over Q(√5) (A1).
- The quadratic formula independently derives the roots as (1 ± √5)/2; the positive root is (1 + √5)/2 ≈ 1.618034 (A2).
- (1 + √5)/2 > 0, confirming it is the positive root (A3).
- The other root, (1 - √5)/2 ≈ -0.618, is negative — there is exactly one positive root.

## Claim Interpretation

**Natural language**: "The positive root of x² - x - 1 = 0 is exactly (1 + √5)/2."

**Formal interpretation**: The equation x² - x - 1 = 0 has a unique positive real root, and that root equals (1 + √5)/2. This is exact algebraic equality — we verify both that substituting φ = (1 + √5)/2 into the polynomial yields identically 0, and that the quadratic formula produces this same value as the positive root. The symbolic argument involves no approximation; numerical checks serve only as supplementary confirmation.

## Evidence Summary

| ID | Fact | Verified |
|----|------|----------|
| A1 | Direct substitution: (1+√5)/2 satisfies x² - x - 1 = 0 | Computed: φ² - φ - 1 = 0 (exact via integer arithmetic over Q(√5)) |
| A2 | Quadratic formula yields (1+√5)/2 as the positive root | Computed: positive root = (1+√5)/2 = 1.618033988749895 |
| A3 | (1+√5)/2 is positive | Computed: True (1.618... > 0) |

## Proof Logic

The proof proceeds via two independent methods that converge on the same conclusion.

**Method 1 — Direct substitution (A1):** We represent φ = (1 + √5)/2 in the form (a + b√5)/c with integer coefficients a = 1, b = 1, c = 2. Then:

- φ² = (1 + √5)²/4 = (6 + 2√5)/4 = (3 + √5)/2
- φ² - φ = (3 + √5)/2 - (1 + √5)/2 = (2 + 0·√5)/2 = 1
- φ² - φ - 1 = 1 - 1 = 0

All arithmetic is exact (integer operations on rational and irrational coefficients). The √5 terms cancel exactly, leaving 0.

**Method 2 — Quadratic formula (A2):** For x² - x - 1 = 0 (a=1, b=-1, c=-1):

- Discriminant: b² - 4ac = 1 + 4 = 5
- Roots: x = (1 ± √5)/2

The positive root is x₁ = (1 + √5)/2, matching φ exactly. The negative root is x₂ = (1 - √5)/2 ≈ -0.618.

**Positivity (A3):** Since √5 > 0, we have 1 + √5 > 1 > 0, so (1 + √5)/2 > 0.

Both methods independently confirm that (1 + √5)/2 is a root of x² - x - 1 = 0, and it is positive.

## Counter-Evidence Search

- **Another positive root?** A degree-2 polynomial has at most 2 roots. The quadratic formula gives both: (1+√5)/2 ≈ 1.618 (positive) and (1-√5)/2 ≈ -0.618 (negative). No other positive root exists.
- **Floating-point masking?** The symbolic verification path uses only integer arithmetic on coefficients of {1, √5}. The irrational parts cancel exactly (coefficient = 0) and the rational remainder is exactly 0. No floating-point approximation is involved.
- **Wrong equation?** Verified that x² - x - 1 = 0 is the unique monic quadratic with integer coefficients having (1+√5)/2 as a root. The related equations x² + x - 1 and x² - x + 1 have different roots or no real roots, respectively.

## Conclusion

**PROVED.** The positive root of x² - x - 1 = 0 is exactly (1 + √5)/2. This is established by two independent methods: direct substitution using exact integer arithmetic over Q(√5) shows φ² - φ - 1 = 0, and the quadratic formula derives (1 + √5)/2 as the unique positive root. The value φ = (1 + √5)/2 ≈ 1.618034 is the golden ratio.

---
Generated by [proof-engine](https://github.com/yaniv-golan/proof-engine) v0.10.0 on 2026-03-28.