base_shift_numerator_offset_forced

formal source

 347
 348/-- With canonical `2W` term fixed, matching `base_shift` in the numerator-offset family
 349    `2W + ((W+E)+n)/(4E_p)` forces `n = 0`. -/
 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
 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)`. -/
 366theorem base_shift_weight_split_forced
 367    {a b : ℚ}
 368    (hsum : a + b = 2)
 369    (h : base_shift = 2 * (W : ℝ) +
 370      ((((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive)) : ℚ) : ℝ)) :
 371    a = 1 ∧ b = 1 := by
 372  have hcanon : base_shift = 2 * (W : ℝ) + (ledger_fraction : ℝ) := by
 373    simp [base_shift]
 374  have hfracR :
 375      ((((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive)) : ℚ) : ℝ) = (ledger_fraction : ℝ) := by
 376    linarith [h, hcanon]
 377  have hfracQ : ((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive)) = ledger_fraction := by
 378    exact_mod_cast hfracR
 379  exact ledger_fraction_weight_split_forced hsum hfracQ
 380