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

- **Generated**: 2026-03-28
- **Reader summary**: [proof.md](proof.md)
- **Proof script**: [proof.py](proof.py)

## Claim Specification

| Field | Value |
|-------|-------|
| Subject | the equation x² - x - 1 = 0 |
| Property | positive root equals (1 + √5)/2 |
| Operator | == |
| Operator note | Exact algebraic equality. We verify that substituting φ = (1 + √5)/2 into x² - x - 1 yields exactly 0 (symbolically), and independently derive the positive root via the quadratic formula to confirm it equals (1 + √5)/2. Numerical verification uses tolerance for floating-point, but the symbolic argument is exact. |
| Threshold | True |

*Source: proof.py JSON summary*

## Fact Registry

| ID | Key | Label |
|----|-----|-------|
| A1 | — | Direct substitution: (1+√5)/2 satisfies x² - x - 1 = 0 |
| A2 | — | Quadratic formula yields (1+√5)/2 as the positive root |
| A3 | — | (1+√5)/2 is positive |

*Source: proof.py JSON summary*

## Full Evidence Table

### Type A (Computed) Facts

| ID | Fact | Method | Result |
|----|------|--------|--------|
| A1 | Direct substitution: (1+√5)/2 satisfies x² - x - 1 = 0 | Direct substitution with exact integer arithmetic over Q(√5) | φ² - φ - 1 = 0 (exact) |
| A2 | Quadratic formula yields (1+√5)/2 as the positive root | Quadratic formula: x = (-b ± √(b²-4ac)) / 2a with a=1, b=-1, c=-1 | Positive root = (1+√5)/2 = 1.618033988749895 |
| A3 | (1+√5)/2 is positive | Direct evaluation: (1+√5)/2 > 0 | φ = 1.618033988749895 > 0 |

*Source: proof.py JSON summary*

## Computation Traces

```
A1: Substitution of φ into x² - x - 1: phi**2 - phi - 1 = 1.618033988749895 ** 2 - 1.618033988749895 - 1 = 0.0000
A1 symbolic verification: φ² - φ - 1 = 0 (exact integer arithmetic)
  φ² = (1+√5)² / 4 = (6 + 2√5) / 4 = (3 + 1√5) / 2
  φ² - φ = (2 + 0√5) / 2 = 2/2 = 1
  φ² - φ - 1 = 1 - 1 = 0  ✓
A2: Discriminant b² - 4ac: b_coeff**2 - 4 * a_coeff * c_coeff = -1 ** 2 - 4 * 1 * -1 = 5
A2: Positive root via quadratic formula: (-b_coeff + math.sqrt(discriminant)) / (2 * a_coeff) = (--1 + math.sqrt(5)) / (2 * 1) = 1.6180
A2: Negative root via quadratic formula: (-b_coeff - math.sqrt(discriminant)) / (2 * a_coeff) = (--1 - math.sqrt(5)) / (2 * 1) = -0.6180
A3: (1+√5)/2 is positive: 1.618033988749895 > 0 = True
Final: all sub-results confirm the claim: True == True = True
```

*Source: proof.py inline output (execution trace)*

## Adversarial Checks (Rule 5)

| # | Question | Verification Performed | Finding | Breaks Proof? |
|---|----------|----------------------|---------|---------------|
| 1 | Could there be another positive root we're missing? | A degree-2 polynomial has at most 2 roots (Fundamental Theorem of Algebra). The quadratic formula gives both roots: (1+√5)/2 ≈ 1.618 and (1-√5)/2 ≈ -0.618. Only one root is positive. Verified computationally: root_negative < 0. | The other root is (1-√5)/2 ≈ -0.618034, which is negative. Only one positive root exists. | No |
| 2 | Could floating-point error make the substitution appear to be zero when it isn't? | The proof uses exact integer arithmetic for the symbolic verification: representing φ as (1 + 1·√5)/2 and computing φ² - φ - 1 using rational coefficients of {1, √5}. The irrational parts cancel exactly (coefficient = 0) and the rational remainder is exactly 0. No floating-point arithmetic is involved in the symbolic path. | Symbolic verification uses only integer/rational arithmetic. Result is exactly 0, not approximately 0. | No |
| 3 | Is the equation x² - x - 1 = 0 the correct equation (not x² + x - 1 or x² - x + 1)? | Checked: x² - x - 1 evaluated at φ = (1+√5)/2 gives 0. If the equation were x² + x - 1, the roots would be (-1 ± √5)/2, and the positive root would be (-1+√5)/2 ≈ 0.618, not (1+√5)/2. If the equation were x² - x + 1, discriminant = 1-4 = -3 < 0, no real roots. | The equation x² - x - 1 = 0 is the unique monic quadratic with integer coefficients having (1+√5)/2 as a root (up to scaling). | No |

*Source: proof.py JSON summary*

## Hardening Checklist

- **Rule 1**: N/A — pure computation, no empirical facts
- **Rule 2**: N/A — pure computation, no empirical facts
- **Rule 3**: `date.today()` used for generated_at timestamp
- **Rule 4**: CLAIM_FORMAL with operator_note provided, explaining exact algebraic equality and the dual verification approach
- **Rule 5**: Three adversarial checks: uniqueness of positive root, floating-point vs symbolic exactness, equation correctness
- **Rule 6**: N/A — pure computation, no empirical facts. Cross-check uses mathematically independent methods (direct substitution vs quadratic formula)
- **Rule 7**: `compare()` and `explain_calc()` imported from computations.py; no hard-coded constants
- **validate_proof.py result**: PASS (14/14 checks passed, 0 issues, 0 warnings)

*Source: author analysis*

## Generator

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