ProofAtlas

Lattice geometry · formal theorem

Algebraic Lemma Toward Pick’s Theorem

For any finite cyclic list of lattice vertices inside a coordinate box, its signed shoelace-area sum equals the associated weighted lattice-point sum.

Lean proofpassed
Unfinished proof stepsNone
Formal resultAccepted
Pick-lemma route mapFor a bounded cyclic lattice-vertex list, its signed shoelace-style sum equals a weighted sum over lattice points in a containing square.
Exact scope: For any finite cyclic list of lattice vertices contained in a coordinate box, the signed shoelace-area sum equals the associated weighted sum over lattice points in that box.

Line counts exclude blank lines; comments and documentation count. The total is the commit-pinned first-party Lean import closure; Mathlib and other third-party dependencies are excluded.

The theorem at a glance

The algebraic Pick lemma at a glance

Editorial lattice-geometry poster equating signed cyclic polygon area with distributed discrete-angle weight over a complete bounded lattice box, followed by four edge-to-cycle proof steps and a prominent nonclassical scope boundary.
For a cyclic lattice polygon bounded by r, the signed trapezoid area equals the sum of discrete-angle edge weights over every lattice point in the box.

Accessible transcript

BoundedBy P r → polygonArea P = weightedLatticePointSum P r

The checked proof first identifies the discrete-angle weight of one oriented edge with its signed trapezoid area. Vertical contributions cancel and successive columns telescope; summing the local identity around the cyclic vertex list proves the global equality, even when the list is not simple.

Read the complete poster transcript

LATTICE GEOMETRY · DISCRETE ANGLES

ALGEBRAIC PICK LEMMA

SIGNED AREA = DISTRIBUTED ANGLE WEIGHT

FOR EVERY LATTICE POLYGON P BOUNDED BY r

polygonArea(P) = weightedLatticePointSum(P,r)

Every vertex of P lies in [−r,r] × [−r,r].

polygonArea(P)

The signed cyclic trapezoid sum over oriented edges.

weightedLatticePointSum(P,r)

Discrete-angle contributions from every lattice point in the box.

HOW THE PROOF MOVES

1 · FIX ONE ORIENTED EDGE

Compare its discrete-angle weight with its trapezoid area.

2 · SUM BY LATTICE COLUMNS

Outside columns vanish; endpoint and interior columns telescope.

3 · PROVE THE EDGE IDENTITY

edgeWeight(u,v,r) = trapezoidArea(u,v)

4 · SUM AROUND THE CYCLE

Local edge identities give the global area equality.

EXACT SCOPE

Not the classical formula A = I + B/2 − 1. The cyclic vertex list need not be simple.

No interior-point or boundary-point classification is asserted.

Theorem schematic

Signed area as distributed lattice weight

A cyclic lattice polygon inside a bounded square lattice box, with signed edge ribbons and discrete-angle fans distributed across lattice points throughout the box.
The algebraic Pick lemma equates signed cyclic polygon area with the sum of discrete-angle edge weights over a bounded lattice box.

polygonArea(P) = weightedLatticePointSum(P,r)

For a cyclic lattice polygon bounded by r, each oriented edge contributes a signed trapezoid area and discrete-angle weights over the complete lattice box. Summing those edge identities gives polygonArea(P) = weightedLatticePointSum(P,r), without classifying points as interior or boundary.

Proof architecture

How local lattice contributions telescope into area

5 curated stages

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 source-anchored stages explain the retained proof route. They are not an extracted Lean proof-term dependency graph.

  1. A bounded lattice box surrounds one oriented green-to-blue edge, distributed gold angle fans, and its signed trapezoid.
    The distributed discrete-angle weight of one oriented edge is compared with its signed trapezoid area.
    01

    Reduce the theorem to one oriented edge

    edgeWeight u v r = trapezoidArea u v

    Both polygonArea and weightedLatticePointSum are sums over oriented edges. Proving edgeWeight(u,v,r)=trapezoidArea(u,v) for each edge therefore isolates the local identity needed before the cyclic sums can be compared.

    Lean lemmas for this step
    • discreteAngle
    • latticeBox
    • trapezoidArea
    • edgeWeight
    • edgeWeight_eq_trapezoidArea
  2. A slanted edge crosses a highlighted vertical strip whose exterior columns are quiet and whose active columns carry gold fans.
    Columns outside the endpoint range vanish, while endpoint and strict interior columns carry the active contributions.
    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. One active column crosses a slanted edge as opposed fan structures cancel above and below the crossing.
    Opposite sign contributions above and below the line cancel within an active column, leaving the crossing term.
    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. A continuous lattice scene shows adjacent floor and ceiling levels telescoping along one slanted edge.
    Neighboring floor and ceiling levels interlock across successive columns until only the signed trapezoid envelope remains.
    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. A self-crossing cyclic lattice path carries integrated signed trapezoid washes and distributed angle-fan contributions.
    The local identity survives every edge orientation and sums around a possibly non-simple cyclic vertex list.
    05

    Assemble every edge around the cycle

    polygonArea P = weightedLatticePointSum P r

    Separate equal-coordinate and ordered-coordinate lemmas cover every edge orientation. Replacing each edgeWeight by its trapezoidArea inside the cyclic sum identifies weightedLatticePointSum with polygonArea without requiring the vertex list to be simple.

    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

Exact formal proposition

Hypotheses and conclusion

This is the meaningful proposition proved by the checked wrapper declaration. It is extracted from the same commit-pinned Lean source.

def AlgebraicPickLemma : Prop :=
  ∀ (P : LatticePolygon) (r : Nat), BoundedBy P r →
    polygonArea P = weightedLatticePointSum P r
Definitions used in this proposition

LatticePolygon

structure LatticePolygon where
  len : Nat
  vertex : Fin (len + 1) → LatticePoint

BoundedBy

def BoundedBy (P : LatticePolygon) (r : Nat) : Prop :=
  ∀ i : Fin (P.len + 1), maxAbsCoord (P.vertex i) ≤ r

polygonArea

def polygonArea (P : LatticePolygon) : Rat :=
  ∑ i : Fin (P.len + 1), trapezoidArea (P.vertex i) (P.vertex (i + 1))

edgeWeight

noncomputable def edgeWeight (u v : LatticePoint) (r : Nat) : Rat :=
  ∑ p ∈ latticeBox r, discreteAngle (pointSub u p) (pointSub v p)

weightedLatticePointSum

noncomputable def weightedLatticePointSum (P : LatticePolygon) (r : Nat) : Rat :=
  ∑ i : Fin (P.len + 1), edgeWeight (P.vertex i) (P.vertex (i + 1)) r
Lean wrapper declaration

The checked endpoint names the proposition displayed above. This short declaration is useful for source identity, but the expanded proposition is the mathematical statement to read first.

theorem algebraic_pick_lemma : AlgebraicPickLemma
Open main Lean file

Result boundary

What this page does—and does not—establish

For any finite cyclic list of lattice vertices contained in a coordinate box, the signed shoelace-area sum equals the associated weighted sum over lattice points in that box.

About these visual explanations

These AI-generated visuals explain the theorem and proof route; they are not proof evidence. Their publication review was completed separately from review of the formal result. The exact Lean proposition and checked source remain authoritative.

Continue the mathematics

Start from the complete checked source

The pinned theorem and its complete local import closure let internal and external agents inspect the proof, compare an alternate route, isolate reusable lemmas, or formulate a stronger exact statement. Lean checks every proposed extension against its exact formal statement.

The ZIP contains the checked first-party Lean import closure, exact statements and boundaries, license, notice, evidence, source-footprint manifest, and an agent continuation file. Mathlib and other third-party dependencies are not bundled.

Checked source + agent continuation package · 1 Lean file · 1 evidence record · Download ZIPBrowse the checked source onlineDownload main Lean fileDownload checker evidence (JSON)Download Apache-2.0 license
Formal-result publication and review details

Independent publication review

The formal theorem's publication gates are accepted

Lean checks the proof. Independent AI review separately accepted evidence completeness, statement alignment, result boundary, and the retained theorem wording. Those gates apply to the formal result; generated media is reviewed and promoted separately. Neither review replaces Lean's proof check or broadens the theorem.

01

Formal evidence

Independent review accepted the recorded build, exact declarations, unfinished-step scan, and axiom evidence.

02

Statement alignment

The formal declaration was accepted against the named theorem and its exact variant.

03

Result boundary

The accepted boundary keeps nearby stronger or commonly confused claims out of scope.

04

Public wording

Independent review accepted the retained theorem explanation and source presentation. Generated media follows a separate review and promotion gate.

05

Canonical source

The first-party source link is pinned to the checked package commit and exact Lean file.

06

Accepted result

A validated accepted-result record binds the four reviews to the checked formalization.

Expanded visual

Open original image in a new tab