tesla_turbine_master
plain-language theorem explainer
The master theorem asserts that Tesla turbine disc spacing of 2δ√φ yields velocity ratio φ, step ratios are invariant under base-radius scaling, J(φ) > 0, and φ satisfies its self-similar fixed-point equation. Fluid-dynamicists and RS engineers modeling bladeless turbines cite it to justify φ-scaling in gap and pitch design. The proof is a term-mode exact that packages four prior lemmas into the conjunction.
Claim. The conjunction holds: (∀ δ > 0, velocity ratio across gap 2δ√φ equals φ) ∧ (∀ c, r₀, θ, Δθ, P with c ≠ 0 and r₀ ≠ 0, step ratio at scaled radius c r₀ equals step ratio at r₀) ∧ (J(φ) > 0) ∧ (φ = 1 + 1/φ).
background
The module models Tesla's 1913 bladeless turbine as a φ-spiral engine: fluid spirals inward between parallel discs with gap g, transferring momentum via boundary-layer adhesion. Jcost is the Recognition Science cost function Cost.Jcost; velocityRatio and stepRatio are the velocity and per-turn compression ratios defined via the logarithmic spiral in Flight.Geometry and SpiralField. Upstream lemmas establish the φ-optimal gap (phi_disc_spacing_optimal), radius-scale invariance of stepRatio (stepRatio_invariant_under_r0), positivity of J(φ) (compression_has_cost), and the fixed-point equation (phi_is_optimal_compression).
proof idea
Term proof via exact that supplies a 4-tuple: the first component is phi_disc_spacing_optimal δ hδ; the second is the imported stepRatio_invariant_under_r0 applied to the scaled radius; the third is compression_has_cost; the fourth is phi_is_optimal_compression.
why it matters
This is the master certificate collecting the four core properties that make the Tesla turbine a φ-spiral engine, directly supporting the module's claim that φ minimizes J-cost for compression and spacing. It instantiates the self-similar fixed point (T6) and eight-tick octave structure from the forcing chain, with φ as the minimum non-trivial stable step. No downstream uses are recorded yet; it closes the local engineering model in the Flight domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.