A sharp lower general-position bound for Cartesian products

We study the lower general-position number gp⁻(G), defined as the minimum cardinality of an inclusion-maximal vertex set containing no three vertices on a common geodesic. This paper disproves a conjectured lower bound for Cartesian products of graphs. For every integer r ≥ 6, we construct connected diameter-two graphs G and H with gp⁻(G) = r and gp⁻(H) ≥ r, while gp⁻(G □ H) = 5. Consequently, the conjectured inequality can fail by an arbitrarily large additive gap. We further establish the sharp universal inequality gp⁻(G □ H) ≥ min{5, gp⁻(G), gp⁻(H)} for all nonempty finite simple graphs. The universal bound is established through a mathematical reduction to metric equality patterns and an exact, reproducible finite obstruction computation. A separate Lean formalization certifies the fixed 319-vertex counterexample using actual shortest-path semantics, but does not formalize the universal theorem. Included materials (version 0.3): lower-gp-cartesian-v0.3.pdf — Complete research manuscript. lower-gp-cartesian-v0.3-latex-source.zip — LaTeX source and bibliography. lower-gp-cartesian-v0.3-reproducibility.zip — Verification programs, Lean source, certificates, reproducibility instructions, and verification records. Licensing: The manuscript and LaTeX source are licensed under Creative Commons Attribution 4.0 International (CC BY 4.0). Repository-owned verification software is covered by Apache License 2.0 where applicable. Other included materials retain their respective original licenses, as documented in the reproducibility archive. Research status: This is a publicly distributed research preprint, not an externally peer-reviewed publication. AI assistance in mathematical research, formal verification, software development, and manuscript preparation is disclosed in the manuscript.