theorem
proved
tactic proof
base_shift_kn_forced_under_passive_bound
show as:
view Lean formalization →
formal statement (Lean)
384theorem base_shift_kn_forced_under_passive_bound
385 {k n : ℕ} (hk : 0 < k) (hn_le : n ≤ E_passive)
386 (h : base_shift = 2 * (W : ℝ) +
387 (((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) : ℚ) : ℝ)) :
388 k = 4 ∧ n = 0 := by
proof body
Tactic-mode proof.
389 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
390 simp [base_shift]
391 have hfracR :
392 (((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
393 linarith [h, hcanon]
394 have hfracQ : ((((W + E_total + n : ℕ) : ℚ) / (k * E_passive)) = ledger_fraction) := by
395 exact_mod_cast hfracR
396 exact ledger_fraction_kn_forced_under_passive_bound hk hn_le hfracQ
397
398/-- Positivity-free packaged `base_shift` closure for integer perturbations:
399 under passive-edge band `n ≤ E_p`, matching
400 `2W + ((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0`
401 without explicit `k > 0`. -/