base_shift_weight_split_forced

formal source

 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
 381/-- Packaged `base_shift` closure for integer numerator/denominator perturbations:
 382    under passive-edge band `n ≤ E_p`, matching
 383    `2W + ((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0`. -/
 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
 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