theorem proved term proof

`fibonacci_compression_step`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 175theorem fibonacci_compression_step (a b : ℕ) (hab : a ≤ b) :
 176    totalCompressionRatio b / totalCompressionRatio a = phi ^ (b - a) := by

proof body

Term-mode proof.

 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. -/

depends on (16)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
phi_ne_zero in IndisputableMonolith.Constants decl_use
totalCompressionRatio in IndisputableMonolith.Flight.TeslaTurbine decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
cost in IndisputableMonolith.Foundation.MultiplicativeRecognizerL4 decl_use
cost in IndisputableMonolith.Foundation.ObserverForcing decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
phi_ne_zero in IndisputableMonolith.NumberTheory.PhiLadderLattice decl_use
phi_ne_zero in IndisputableMonolith.PhiSupport.Lemmas decl_use