pith. machine review for the scientific record. sign in
theorem proved tactic proof

base_shift_weight_split_forced

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

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

depends on (15)

Lean names referenced from this declaration's body.