The 8-connected bit-quad Euler formula for finite rasters: a Lean proof by vertex double counting

Working paper, not peer reviewed. Nothing in this record is field-validated. Scope and novelty. Project P1 aims to replace the assumed topological step (FaceCount) in Trees Cannot Cut (doi:10.5281/zenodo.21686446) with machine-checked theorems about finite rasters. Its first result, Gray's 1971 bit-quad formula for the Euler characteristic of an 8-connected binary image (IEEE Transactions on Computers C-20(5):551-561, doi:10.1109/T-C.1971.223289), is a Lean 4 formalization of a known formula, not a new result. We are not aware of an earlier machine-checked proof, but we have not searched exhaustively and claim no novelty. Until the remaining rungs (L2 and L3) are proved, the FaceCount assumption is not discharged. For a finite set B of pixels in Z^2, let K(B) be the union of the closed unit squares of B, regarded as a cubical complex with Euler characteristic V - E + F. Gray's bit-quad formula in its 8-connected form states 4*chi(K(B)) = Q1 - Q3 - 2*QD, where Q1, Q3 and QD count the 2x2 windows holding exactly one pixel, exactly three pixels, and exactly two diagonally opposite pixels of B. We give a Lean 4 proof, against Mathlib, of the sealed statement P1.BitQuad, which states this identity for every finite raster. The proof is a double count over the vertices of K(B). Each of F, E and V is written as a sum over vertices of indicators of translated sets. A single shift-counting lemma evaluates all eight such sums, and a pointwise identity is closed by a case split on the window patterns; only the 15 non-empty patterns can occur at a vertex. This is the first rung (L1) of a lemma ladder whose goal is to replace the topological hypothesis assumed in the machine-checked core of Trees Cannot Cut with a theorem about rasters. We also explain how L1 makes the change in chi under a single-pixel insertion local, which is the local half of the next rung, L2. Verification. a Lean 4 proof of P1.BitQuad, a statement fixed before the proof attempt, machine-checked against Mathlib and replayed through the Lean kernel using only the standard axioms Run record, certification page and reproducible package: https://github.com/jdhart81/viridis-research/tree/main/runs/2026-10-28_P1 AI use: this version was drafted by an AI research agent (Claude, by Anthropic) running the Viridis research engine. Formal claims are checked by the Lean 4 kernel and labelled by an automated verifier. Justin D. Hart directs the research and is the accountable author. No AI system is listed as an author.