Algebraic Lemma Toward Pick’s Theorem

The checked algebraic route proves one oriented edge identity by isolating its active lattice strip, cancelling vertical sign contributions, and telescoping floor and ceiling terms before summing the edge cases around a cyclic list.

These stages follow the checked source and explain the mathematical route. They summarize the argument; they are not a visualization of Lean's internal proof term.

1. 

   01

   One edge, two local contributions

   edgeWeight u v r = trapezoidArea u v

   A finite rectangular lattice surrounds one forest-green-to-cobalt oriented edge, while restrained gold halos mark the lattice points in the bounded collection. Beside it, the matching endpoint colors and direction bound a translucent trapezoid against a horizontal reference line. The stage isolates the local edge comparison before the later cyclic sum and contains no variable labels or formulas.

   Lean lemmas for this step

   • discreteAngle
   • latticeBox
   • trapezoidArea
   • edgeWeight
   • edgeWeight_eq_trapezoidArea

2. 

   02

   Only the active x-strip contributes

   Outside columns vanish; endpoint and interior columns have distinct weights

   The discrete-angle lemmas split lattice points by first coordinate. Columns beyond the edge's horizontal endpoint range contribute zero; the two endpoint columns and the strict interior columns have separate formulas that make the remaining finite sum explicit.

   Lean lemmas for this step

   • discreteAngle_pointSub_eq_zero_of_fst_lt_left
   • discreteAngle_pointSub_eq_zero_of_fst_lt_right
   • discreteAngle_pointSub_eq_left_endpoint
   • discreteAngle_pointSub_eq_right_endpoint
   • discreteAngle_pointSub_eq_interior

3. 

   03

   Cancel signs inside one vertical column

   Σᵧ discreteAngle ((x,y)-u) ((x,y)-v)

   Within a strict interior column, the sign of the point-cross expression changes at the edge crossing. Pairing the terms above and below that level cancels the vertical tails and reduces the column sum to the floor-and-ceiling contribution used next.

   Lean lemmas for this step

   • signRat_pointCross_pointSub_left_endpoint
   • signRat_pointCross_pointSub_right_endpoint
   • discreteAngle_pointSub_eq_interior_sign
   • horizontal_interior_column_sum

4. 

   04

   Telescope floor and ceiling contributions

   interior column sums telescope to the signed trapezoid

   The floor term from one active column pairs with the ceiling term in the next. Summing across the finite x-strip cancels the intermediate levels and leaves exactly the endpoint expression for trapezoidArea(u,v).

   Lean lemmas for this step

   • interior_column_floor_ceil_bounds
   • interior_column_sum_of_floor_ceil_bounds
   • interior_column_sum
   • interior_columns_sum
   • sum_floor_add_ceil_mul_div_Ioo

5. 

   05

   Assemble algebraic edge weights around one closed cycle

   polygonArea P = weightedLatticePointSum P r

   One eight-vertex cyclic lattice polygon is rendered once inside a complete finite lattice box. Each edge joins consecutive vertices, the final edge returns exactly to the first vertex, and one arrowhead per edge follows the same cyclic order. Vertical drops from all vertices to one horizontal reference level bound the translucent forest and cobalt trapezoid contributions. Every lattice point has identical neutral treatment; the pixels make no interior or boundary classification and assign no numerical weight. The exact algebraic edge-weight identity remains in HTML.

   Lean lemmas for this step

   • edgeWeight_eq_trapezoidArea_of_fst_eq
   • edgeWeight_eq_trapezoidArea_of_snd_eq
   • edgeWeight_eq_trapezoidArea_of_lt
   • edgeWeight_eq_trapezoidArea
   • polygonArea_eq_weightedLatticePointSum_of_edgeWeight_eq
   • algebraic_pick_lemma