compression_3_discs

formal source

 160def totalCompressionRatio (N : ℕ) : ℝ := phi ^ N
 161
 162/-- Compression ratios at small disc counts (Fibonacci-adjacent). -/
 163theorem compression_3_discs : totalCompressionRatio 3 = phi ^ 3 := rfl
 164theorem compression_5_discs : totalCompressionRatio 5 = phi ^ 5 := rfl
 165theorem compression_8_discs : totalCompressionRatio 8 = phi ^ 8 := rfl
 166
 167/-- The ratio between consecutive Fibonacci-count compressions is φ.
 168    φ^{F_{n+1}} / φ^{F_n} = φ^{F_{n+1} - F_n} = φ^{F_{n-1}}.
 169
 170    This means stepping from a 5-disc to an 8-disc turbine
 171    multiplies the compression by φ³ = φ⁵/φ² = φ^(8-5).
 172
 173    The Fibonacci disc counts form a natural hierarchy where each
 174    step up in complexity provides φ-scaled improvement. -/
 175theorem fibonacci_compression_step (a b : ℕ) (hab : a ≤ b) :
 176    totalCompressionRatio b / totalCompressionRatio a = phi ^ (b - a) := by
 177  simp only [totalCompressionRatio]
 178  rw [div_eq_iff (pow_ne_zero a phi_ne_zero)]
 179  rw [← pow_add]
 180  congr 1
 181  omega
 182
 183/-! ## §4. J-Cost of the Turbine -/
 184
 185/-- The efficiency of a Tesla turbine stage is inversely related to
 186    the J-cost of its compression ratio.
 187    For a single-turn κ=1 stage: J(φ) = φ − 3/2 ≈ 0.118.
 188    This is the minimum non-trivial cost on the φ-ladder. -/
 189theorem single_turn_Jcost :
 190    Jcost phi = (phi + phi⁻¹) / 2 - 1 := by
 191  simp only [Jcost, Cost.Jcost]
 192
 193/-- J(1) = 0: a turbine with no compression has zero cost (trivial). -/