Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-01
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A finite rectangle cover admits grid control with arbitrarily small volume excess

Statement

If Q is a closed nondegenerate rectangle and E⊆Q is covered by finitely many axis-parallel rectangles of total volume V, then for every η>0 there is a grid of Q such that the cells meeting E have total volume below V+η.

Facts & Assumptions

Proof

technique · constructive
1.1

Intersect each covering rectangle with Q. Each nonempty intersection is a closed coordinate rectangle Rj⊆Q with volume no larger than the original rectangle. If some Rj=Q, the one-cell grid already has total meeting-cell volume vol⁡(Q)≤V<V+η, so assume otherwise. Move every coordinate face of each Rj that is not already a face of Q outward by a positive margin, staying inside Q, so that the resulting rectangle Rj+ has volume increase below a prescribed share of η. Continuity of the finite volume product and finiteness make the total increase below η; because no Rj equals Q, at least one face of every Rj moves, and the finite set of chosen margins has a positive least member.

L1L2givenchoose
2.1

Insert every endpoint of every Rj+ into the coordinate grids, then refine to mesh smaller than the least margin using For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε. If a closed cell meets Rj, each of its coordinate intervals lies inside the corresponding enlarged interval: away from a face of Q this follows from the mesh-margin bound, while at a face of Q there is no cell on the outside. Hence that cell lies in Rj+.

step 1.1L2construct
3.1

Assign each cell meeting E to one Rj that it meets. By step 2.1 it lies in the aligned rectangle Rj+. Splitting the iterated sums bounds the assigned cells' total volume by ∑jvol⁡(Rj+)<V+η.

step 2.1L2given
4.1

The constructed grid has the asserted control.

step 3.1discharge-construct∎

Depends on

Used by

Dependency tree · two levels

51 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources