phi_is_optimal_compression
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.