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

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

 188theorem ledger_fraction_numerator_offset_forced
 189    {n : ℚ}
 190    (h : (((W + E_total : ℚ) + n) / (4 * E_passive) = ledger_fraction)) :
 191    n = 0 := by

proof body

Tactic-mode proof.

 192  have hW : W = 17 := mass_topology_counts.2.2
 193  have hE : E_total = 12 := mass_topology_counts.1
 194  have hEp : E_passive = 11 := mass_topology_counts.2.1
 195  have hraw : ((29 : ℚ) + n) / 44 = (29 : ℚ) / 44 := by
 196    simpa [ledger_fraction, hW, hE, hEp, add_assoc, add_comm, add_left_comm,
 197      mul_comm, mul_left_comm, mul_assoc] using h
 198  nlinarith [hraw]
 199
 200/-- In the normalized two-weight family `(aW + bE)/(4E_p)` with total weight `a+b=2`,
 201    canonical matching forces `(a,b) = (1,1)`. -/

used by (1)

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

depends on (20)

Lean names referenced from this declaration's body.