fibonacci_compression_step
plain-language theorem explainer
The theorem establishes that the total compression ratio for b turns over a turns equals phi to the power of (b minus a) when a is at most b. Turbine modelers comparing Fibonacci disc stacks would cite this scaling to quantify phi-multiplied gains between stages. The term proof unfolds the power definition of the ratio, rewrites the quotient via the division property for nonzero bases, adds the exponents, and finishes with natural-number arithmetic.
Claim. For natural numbers $a, b$ with $a ≤ b$, the ratio of total compression ratios satisfies $φ^b / φ^a = φ^{b-a}$.
background
The module treats the Tesla turbine as a φ-spiral engine whose fluid path is a logarithmic spiral between closely spaced discs. Total compression ratio for N turns is defined as phi raised to N, so the ratio between two such quantities reduces to an exponent difference. This rests on the phi fixed point from the forcing chain and on spiral lemmas imported from Flight.Geometry and Spiral.SpiralField. Upstream, phi_ne_zero supplies the non-vanishing needed for division, while the definition of totalCompressionRatio supplies the explicit power form.
proof idea
The term proof is a direct algebraic reduction. It first unfolds totalCompressionRatio to obtain phi^b / phi^a. It then rewrites the division as multiplication by the reciprocal using div_eq_iff together with phi_ne_zero. The next step applies the exponent-addition identity in the reverse direction, after which congr 1 and omega finish the arithmetic on the exponents.
why it matters
The result supplies the exact scaling law that makes Fibonacci disc counts a natural hierarchy inside the turbine model, each step multiplying compression by an integer power of phi. It therefore supports the J-cost minimization claim for the turbine geometry and connects directly to the Recognition Composition Law and the eight-tick octave structure. No downstream theorems are listed, yet the scaling is presupposed by the module's later comparisons of 3-disc and 5-disc stages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.