Analytic Spread for a Pair of Cycles

Let (C_n) and (C_m) be cycles, and let ( Hn,m) be the generalized hyperconnectivity—equivalently, Jacobian—matrix associated with the edge-pair (2×2) minors defining (JC_n,C_m). Over every field of characteristic zero, we prove that [nullity Hn,m= 12 n+ 12 m,] and that its kernel is generated by the evident alternating parity vectors whenever they exist. Consequently, [(JC_n,C_m)=nm- 12 n- 12 m,] resolving Conjecture 6.8 of Landsittel and Nevo, “Analytic Spread via Linear Matroids,” arXiv:2607.07458v1. The proof uses an exponential one-parameter specialization. A transfer-pencil calculation and monic-gcd lemma settle all cases containing an even cycle. In the odd–odd case, a retained graph decomposes into odd-unicyclic components with an attached tail; a signless-incidence determinant and a (2×2) Schur coefficient establish full rank. This deposit contains the manuscript, exact supporting checkers, mathematical and custody mutation tests, a deterministic network-free replay, and a substantial partial Lean 4.22.0 formalization of uniform algebraic and combinatorial sublemmas. The Lean material is not presented as a complete formal proof of the theorem. This work was developed as part of the conjecture-prover and autoformalization project of Stanford Lean Club. OpenAI GPT-5.6 Sol Ultra provided substantial research and proof-development assistance. The human author directed the project, required independent audits and exact replay, and assumes responsibility for the claims and presentation. The manuscript and documentation are licensed under CC BY 4.0. Python and Lean source, checker output, and certificate data are licensed under the MIT License, as specified in the archive’s LICENSE file. Proof-and-replay archive SHA-256: 358c08edf4d1f84bb293d7a8d925216bfb81b7fd42995814b847b7db4b2c76e5