NestedDot: A Formally Verified Alternative to QR Code's Binary Design

The NestedDot system replaces QR code's binary grid with nested colored dots and 8-valued logic labels, achieving higher information density through hierarchical encoding. Formalized entirely in Lean 4 with verified mathematical proofs, it represents a rare convergence of formal computer science and practical barcode design. While not seeking to replace QR codes, NestedDot demonstrates how formal methods can unlock new paradigms in 2D symbology, expanding beyond binary assumptions.