Jcost
plain-language theorem explainer
Jcost aliases the core J-cost function for local use in Tesla turbine disc-gap analysis. Engineers optimizing boundary-layer flow under Coandă adhesion cite it to apply φ-scaling that minimizes velocity-profile cost. The declaration is a direct noncomputable abbreviation with no added structure or computation.
Claim. Let $J: (0,∞) → ℝ$ be the J-cost function calibrated on the multiplicative group of positive reals. Then Jcost denotes this same function for use in the Tesla turbine geometry.
background
The Tesla turbine consists of a stack of parallel discs with fluid entering tangentially and spiraling inward through uniform gaps, transferring momentum via boundary-layer adhesion. J-cost measures the energetic penalty associated with the resulting velocity profile across each gap, drawing on the Recognition Composition Law that governs cost addition under multiplication and division of arguments. The module interprets the 1913 patent through φ-scaling, where disc spacing, spiral pitch, and disc count are chosen to minimize this cost.
proof idea
One-line wrapper that aliases IndisputableMonolith.Cost.Jcost.
why it matters
The alias supplies the J-cost primitive required by sibling results such as phi_disc_spacing_optimal and phi_spacing_Jcost, which establish that φ-ratio gaps minimize flow cost. It links the Flight domain to the foundational J-uniqueness step (T5) and the Recognition Composition Law. No open questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.