phi_disc_spacing_optimal
plain-language theorem explainer
The theorem shows that setting the disc gap g to 2δ√φ for positive boundary-layer thickness δ produces a velocity ratio of exactly φ across the gap. Fluid dynamicists modeling Coandă momentum transfer in bladeless turbines would cite this to achieve the golden-ratio profile that minimizes J-cost. The proof reduces the squared ratio algebraically to √φ via field simplification and then applies the square-root squaring identity under positivity of φ.
Claim. Let $φ$ denote the golden ratio. For $δ > 0$, if the gap satisfies $g = 2δ√φ$, then the velocity ratio across the gap, defined by $(g/(2δ))^2$, equals $φ$.
background
In the Tesla turbine model, fluid spirals inward through gaps of width g between discs, with boundary-layer thickness δ. The velocityRatio definition computes the centerline-to-disc velocity ratio as $(g/(2δ))^2$ for a parabolic profile. The module frames all engineering parameters (gap, pitch, disc count) as φ-scaled to minimize J-cost, where J is the Recognition Science cost $J(x) = (x + x^{-1})/2 - 1$ derived from the multiplicative recognizer and observer forcing structures. Upstream results supply the velocityRatio definition and the J-cost structures from PhiForcingDerived and ObserverForcing.cost.
proof idea
The tactic proof begins by simplifying the velocityRatio definition. It introduces non-zero hypotheses for δ and 2δ, proves the ratio g/(2δ) equals √φ by field_simp, rewrites the expression, and concludes with the exact application of Real.sq_sqrt using positivity of φ.
why it matters
This supplies the first clause of the tesla_turbine_master theorem and is invoked by phi_spacing_Jcost to equate J-cost at the optimum to J(φ) ≈ 0.118, the minimum non-trivial interaction cost on the φ-ladder. It realizes the module's claim that disc spacing follows φ-scaling and connects to the forcing chain where φ is the self-similar fixed point (T6) and J-uniqueness (T5) forces the cost minimum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.