TurbineGeometry
plain-language theorem explainer
TurbineGeometry encodes the core parameters of a Tesla turbine as a stack of N discs separated by uniform gap g, with outer radius R_outer and inner exhaust radius R_inner obeying strict positivity and ordering. Fluid-dynamic modelers and Recognition Science engineers optimizing boundary-layer adhesion would cite this as the base object before deriving φ-scaled spacing or pitch. The declaration is a plain structure with four fields and four embedded positivity constraints.
Claim. A turbine geometry consists of a natural number $N$ of discs, gap $g>0$, outer radius $R_o>0$, and inner radius $R_i>0$ satisfying $R_i<R_o$.
background
The module treats the Tesla turbine as a φ-spiral engine whose fluid path is a logarithmic spiral. Fluid enters tangentially at the outer radius and spirals inward through the gaps, transferring momentum by boundary-layer adhesion (Coandă effect). The supplied DOC_COMMENT states: 'The Tesla turbine uses a stack of N parallel discs with uniform gap g. Fluid enters tangentially at the outer radius and spirals inward.' MODULE_DOC adds that optimal disc spacing is proportional to φ times boundary-layer thickness δ, while spiral pitch κ=1 yields per-turn compression exactly φ.
proof idea
This is a structure definition. It introduces the four fields numDiscs, discGap, outerRadius, innerRadius together with the four positivity and ordering constraints gap_pos, outer_pos, inner_pos, inner_lt_outer.
why it matters
The structure supplies the geometric substrate for every later result in the module, including phi_disc_spacing_optimal, spiral_pitch_one_is_phi, and the master certificate tesla_turbine_master. It embeds the Recognition Science φ-ladder and J-cost minimization directly into turbine engineering parameters, linking the eight-tick octave and RCL to concrete disc-gap and compression ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.