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

ledger_fraction_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)

 202theorem ledger_fraction_weight_split_forced
 203    {a b : ℚ}
 204    (hsum : a + b = 2)
 205    (h : ((a * (W : ℚ) + b * (E_total : ℚ)) / (4 * E_passive) = ledger_fraction)) :
 206    a = 1 ∧ b = 1 := by

proof body

Tactic-mode proof.

 207  have hW : W = 17 := mass_topology_counts.2.2
 208  have hE : E_total = 12 := mass_topology_counts.1
 209  have hEp : E_passive = 11 := mass_topology_counts.2.1
 210  have hlin : (a * 17 + b * 12) / 44 = ((17 + 12 : ℚ) / 44) := by
 211    simpa [ledger_fraction, hW, hE, hEp] using h
 212  have hcross : (a * 17 + b * 12) * 44 = ((17 + 12 : ℚ) * 44) := by
 213    exact (div_eq_div_iff (by norm_num : (44 : ℚ) ≠ 0) (by norm_num : (44 : ℚ) ≠ 0)).mp hlin
 214  have hnum : a * 17 + b * 12 = (17 + 12 : ℚ) := by
 215    nlinarith [hcross]
 216  have ha : a = 1 := by nlinarith [hsum, hnum]
 217  have hb : b = 1 := by nlinarith [hsum, hnum]
 218  exact ⟨ha, hb⟩
 219
 220/-- Joint Diophantine forcing for integer numerator/denominator perturbations of the
 221    ledger fraction: under passive-edge band `n ≤ E_p`, canonical matching in
 222    `((W+E)+n)/(kE_p)` forces `k = 4` and `n = 0`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.