theorem
proved
tactic proof
base_shift_numerator_offset_forced
show as:
view Lean formalization →
formal statement (Lean)
350theorem base_shift_numerator_offset_forced
351 {n : ℚ}
352 (h : base_shift = 2 * (W : ℝ) +
353 (((((W + E_total : ℚ) + n) / (4 * E_passive)) : ℚ) : ℝ)) :
354 n = 0 := by
proof body
Tactic-mode proof.
355 have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
356 simp [base_shift]
357 have hfracR :
358 (((((W + E_total : ℚ) + n) / (4 * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
359 linarith [h, hcanon]
360 have hfracQ : (((W + E_total : ℚ) + n) / (4 * E_passive)) = ledger_fraction := by
361 exact_mod_cast hfracR
362 exact ledger_fraction_numerator_offset_forced hfracQ
363
364/-- With canonical `2W` term fixed, matching `base_shift` in the normalized
365 two-weight family `2W + (aW+bE)/(4E_p)` with `a+b=2` forces `(a,b)=(1,1)`. -/