`fibonacci_compression_step`

proved

show as: view math explainer →

module: IndisputableMonolith.Flight.TeslaTurbine
domain: Flight
line: 175 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Flight.TeslaTurbine on GitHub at line 175.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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). -/
 194theorem no_compression_zero_cost :
 195    Jcost 1 = 0 := Cost.Jcost_unit0
 196
 197/-- J(φ) > 0: any non-trivial compression incurs positive cost. -/
 198theorem compression_has_cost :
 199    0 < Jcost phi := by
 200  have := phi_pos
 201  show 0 < Cost.Jcost phi
 202  rw [Cost.Jcost_eq_sq phi_ne_zero]
 203  apply div_pos
 204  · exact sq_pos_of_pos (sub_pos.mpr one_lt_phi)
 205  · exact mul_pos (by norm_num : (0:ℝ) < 2) phi_pos

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.