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

phi_is_optimal_compression

show as:
view Lean formalization →

The golden ratio satisfies the fixed-point equation φ = 1 + 1/φ, establishing it as the unique self-similar compression ratio greater than 1 that sustains itself under iteration. Engineers and Recognition Science researchers modeling Tesla turbines cite this to justify φ-scaled disc spacing and spiral pitch as minimum J-cost configurations. The proof is a short algebraic reduction that invokes the quadratic identity φ² = φ + 1, clears the denominator by field simplification, and closes with linear arithmetic on non-negative squares.

claimThe golden ratio satisfies the fixed-point equation $φ = 1 + 1/φ$.

background

In the Tesla Turbine module the fluid path is a logarithmic spiral whose engineering parameters (disc gap, pitch κ) are optimized when they follow φ-scaling to minimize J-cost. J-cost is the derived cost of a recognition event or multiplicative recognizer comparator; the Recognition Composition Law supplies the functional equation whose fixed point is φ. Upstream lemmas establish φ ≠ 0 and the quadratic identity φ² = φ + 1; the local setting builds on Flight.Geometry and Spiral.SpiralField for the φ-spiral lemmas that feed the master certificate.

proof idea

The term proof first obtains φ ≠ 0 from phi_ne_zero, then substitutes the quadratic identity from phi_sq_eq. Field simplification removes the denominator 1/φ and nlinarith closes the equality by combining the identity with the non-negativity of φ².

why it matters in Recognition Science

This supplies point 6 of the master theorem tesla_turbine_master, which certifies the Tesla turbine as a φ-spiral engine. It realizes the T6 landmark of the UnifiedForcingChain in which phi is forced as the self-similar fixed point, and it directly justifies why J(φ) is the minimum non-trivial compression cost under repeated application of the map x ↦ 1 + 1/x.

scope and limits

formal statement (Lean)

 213theorem phi_is_optimal_compression :
 214    phi = 1 + 1 / phi := by

proof body

Term-mode proof.

 215  have hphi_ne : phi ≠ 0 := phi_ne_zero
 216  have hphi_sq : phi ^ 2 = phi + 1 := phi_sq_eq
 217  field_simp [hphi_ne]
 218  nlinarith [hphi_sq, sq_nonneg phi]
 219
 220/-! ## §5. Master Certificate -/
 221
 222/-- **MASTER THEOREM: Tesla Turbine as φ-Spiral Engine**
 223
 224    1. Optimal disc spacing: gap = 2δ√φ gives velocity ratio = φ
 225    2. κ = 1 spiral pitch gives per-turn ratio = φ
 226    3. Step ratio depends only on pitch and angle, not base radius
 227    4. Fibonacci disc counts provide φ-scaled compression hierarchy
 228    5. J(φ) is the minimum non-trivial compression cost
 229    6. φ is the unique optimal compression fixed point -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (19)

Lean names referenced from this declaration's body.