ORIGINAL THOUGHT PAPER · JULY 2026 · V5.2 · SELF-CONTAINED FOUNDATIONAL EDITION

Galois Geometry of the Cycle Double Cover Proof

An Unconditional, Gauge-Invariant, Certificate-Complete Obstruction Theory
for Prescribed-Cycle Forcing in the F₂³-Flow Construction of Cycle Double Covers

Unconditional Obstruction Ω · Natural Equivariance · Short Exact Sequence · Duality Obstruction Theorem · Two-Sided Certificates — Self-Contained Foundational Edition with All Proofs

Date of Issue July 12, 2026

Classification Original Thought Paper

Fields Graph Theory · Finite Geometry · Galois Theory · AI-Collaborative Mathematics

Version V5.2 (Self-contained final edition; no further rhetorical upgrades; V6 turns to attacking the vanishing mechanism)

Authors LEECHO Global AI Research Lab & Claude Fable 5 & GPT-5.6 Sol (Cognitive Collective)

V1 RESULTS FROZEN · KST 2026-07-12 11:38

Abstract

This paper is the self-contained foundational edition of the orbital geometry theory for the OpenAI cycle double cover (CDC) construction (released 2026-07-10 [1], with a Lean kernel-checked repository [22]): all proofs of theorems and lemmas are incorporated into the main text, with no references to earlier versions. Core apparatus: the three flow values at each cubic vertex form a line in the Fano plane (Observation 2.3); the GL(3,2)-orbit sizes on the flow set are exclusively 42 or 168, with 42 if and only if the flow induces a proper 3-edge-coloring (Theorem A); the admissible triangle space at each vertex is a Γ-torsor, and gauge amounts to a mere choice of origin (Theorem B); forcing a prescribed cycle is equivalent to that cycle appearing as a connected component of M₀, with pin values always existing and being unique (Theorem C); the forcing class number ≥ 1+|f(C)| (Theorem D). Central Theorem Ω: taking the per-edge quotient Q_e = Γ/⟨f(e)⟩ and the joint map D_f,C = (D_f, ρ_C), the class Ω(f,C) := [(d̄, b)] ∈ coker D_f,C is gauge-independent (the coordinate change lemma is at the level of identities), and Force(f,C) ⟺ Ω = 0 — without presupposing solvability of the base system, hence independent of [1]; it satisfies natural equivariance σ̂_*Ω(f,C) = Ω(σf,C) under the group action (not bare equality); the short exact sequence 0 → coker R_C → coker D_f,C → coker D_f → 0 organizes the total obstruction as an extension of the base obstruction by the relative obstruction (no canonical splitting is claimed); when the base system is solvable ([1] guarantees this, not re-proved here), Ω reduces to ω ∈ coker R_C, and the number of forced solutions = 2^{dim ker R_C}. Duality Obstruction Theorem: Ω ≠ 0 if and only if there exists a family of per-edge functionals annihilating f(e) together with a family of functionals on the cycle vertices satisfying a vertex balance condition and pairing to 1 with the data — the 110 F₂ left-kernel certificates are coordinate instances thereof. The complete Petersen classification is replicated along five independent computational paths: 60/170 feasible, 40/5/15 forced-solution classification, each orbit attaining the classical 5-class lower bound, ν-distribution 80/80/10, ν=2 ⟹ feasible (10/10). Certificate system v3: every stored field is either recomputed and verified or does not exist; the complete six-round adversarial record between two models (alternating attacks) is archived, with the current verifier rejecting all known attacks including two-file coordinated deception. Positioning: Level 2 of the five-level ladder is complete; this paper makes no claim of proximity to Levels 4–5. All retractions and errata (13.1–13.5) are retained in full.

§1 Introduction, Timestamps, Positioning, and Verification Topology

The object of study is the OpenAI CDC construction [1][2]: constructing cycle double covers using nowhere-zero flows over Γ = F₂³ together with binary-set labelings. Its Lean repository [22] claims kernel-checked verification of an unconditional CDC theorem for finite loopless bridgeless multigraphs (endpoint cycleDoubleCover_of_bridgeless; the audit lists only three standard axioms; the present authors verified access but did not independently compile). Peer review by the mathematical community is ongoing; the theorems in this paper do not depend on its validity — the unconditional nature of Theorem Ω is designed precisely for this purpose.

Timestamps and Version Policy: V1 results frozen at KST 2026-07-12 11:38. V2 added proofs; V3 restructured the theorem chain and introduced three-party authorship; V4 added the obstruction class; V4.1 added negative certificates; V5 introduced the unconditional formulation. V5.1 completed the self-contained merger (all proofs incorporated into the main text; natural equivariance; short exact sequence; duality obstruction theorem; terminology and phrasing calibration; certificate system v3). V5.2 is the self-contained final edition: following the third round of Dense review, Lemmas 2.5/2.6 were self-proved and incorporated (providing self-contained proofs of two elementary local facts from [1]), and the short exact sequence phrasing was calibrated. Hereafter, no further rhetorical upgrades; V6 turns to the structure and vanishing mechanism of coker D_f,C.

Positioning Statement: On the five-level ladder (0: structure; 1: invariants and obstructions; 2: self-contained closure with complete certificates; 3: general theorems beyond the Petersen graph; 4: universal Force or 5-CDC; 5: mathematical-historical confirmation), this paper completes Level 2; by cross-model calibration, the distance to Level 3 is approximately half the remaining journey, and the distance to Levels 4/5 is substantial (§17). The value proposition of this paper: providing a well-defined, attackable object.

Verification Topology: Six rounds of cross-model peer review. Data replicated along five independent computational paths: two implementations by Claude Fable 5, two independent implementations by two parallel GPT-5.6 Sol windows, and a 30-variable quotient-space path bypassing the 45-variable system. The certificate system underwent six rounds of alternating adversarial attacks between two models; the complete record is in §13. No single point of trust.

§2 Notation and Preliminaries

Notation 2.1　G is a finite loopless cubic multigraph (parallel edges permitted); c(G) denotes the number of connected components; e ∋ v denotes incidence. Γ := F₂³, with addition + (bitwise XOR), characteristic 2, x+x = 0. The points of PG(2,2) (the Fano plane) are the elements of Γ\{0}; a line is a set of three mutually distinct nonzero elements summing to zero: {x, y, x+y}. The acting group throughout this paper is GL(3,2) (order 168, the full automorphism group of the Fano plane; as an abstract group it is isomorphic to PSL(2,7), mentioned only here). Intrinsic vs. coordinate: the original proof endows Γ only with a linear structure — the intrinsic geometry is PG(2,2), and the intrinsic symmetry group is GL(3,2); identifying Γ with the field GF(8) is an additional coordinatization (the semilinear group ΓL(1,8) ≅ C₇⋊C₃ preserving the field structure is a proper subgroup of index 8), entering only via the Bridging Theorem in §3 to connect with 142857. Quotients and difference maps: ⟨f(e)⟩ := {0, f(e)}, Q_e := Γ/⟨f(e)⟩ ≅ F₂²; D_f: Γ^V → ⊕_eQ_e, D_f(t)_e := [t_u+t_v]; ρ_C denotes the restriction to Γ^V(C); D_f,C := (D_f, ρ_C); K_f := ker D_f; R_C := ρ_C|_{K_f}. All cokernels are taken as cokernels of F₂-vector space maps.

Definition 2.2 (Flows, Orbits, Labelings)　A nowhere-zero Γ-flow is a map f: E → Γ\{0} such that the values on the edges incident to each vertex sum to zero (characteristic 2 eliminates the need for orientations); GL(3,2) acts by (σ·f)(e) := σ(f(e)); the number of flows = F(G,8) (Tutte’s group-flow theorem). U_f := span f(E); f(C) := {f(e) : e ∈ E(C)}. A labeling P assigns to each edge a binary set P_e ⊆ Γ; it is admissible if condition (1) holds: at each vertex, every s ∈ Γ appears in exactly 0 or 2 of the three incident edge-sets. σ({p,q}) := p+q ≠ 0; the induced flow is f_P(e) := σ(P_e). M_s := {e : s ∈ P_e}; in an admissible labeling each M_s is a disjoint union of cycles and each edge belongs to exactly two M_s‘s, yielding a cycle double cover (Lemma 2.6, self-proved herein); the number of nonempty classes is called the class number.

Observation 2.3 (Local Fano Structure; Bidirectional)　(i) A nowhere-zero Γ-flow assigns three pairwise distinct values at each cubic vertex, which form a line in the Fano plane. (ii) Conversely, assigning to each vertex a line and a bijection from incident edges to the three points of that line, such that each edge receives the same point from both endpoints, yields a nowhere-zero Γ-flow.

Proof　(i) Let the three values be x, y, z. The zero-sum condition gives z = x+y; if x = y then z = 0, contradicting the nowhere-zero condition; likewise any two values are distinct. Three mutually distinct nonzero elements summing to zero constitute a line. (ii) Each edge receives a single nonzero value; the three values at each vertex are the three points of a line — mutually distinct and summing to zero — so the flow condition holds. ∎

Definition 2.4 (Gauge, Candidate Labeling, System of Equations)　The gauge at vertex v is an ordered pair (a,b) of its incident edges (with c the third edge): g_v,a := 0, g_v,b := f(a), g_v,c := 0; each vertex has 6 gauges. Given a global gauge g and t ∈ Γ^V: the candidate labeling is P^(v)_e := {t_v+g_v,e, t_v+g_v,e+f(e)} — as a set, this is the coset t_v+g_v,e+⟨f(e)⟩. Let d_e := g_u,e+g_v,e; equation system (4): t_u+t_v+ε_ef(e) = d_e (ε_e ∈ F₂). By Lemma 2.5 (self-proved herein; consistent with the formulation in [1]): given t, ∃ε satisfying (4) ⟺ the candidate sets (cosets) from the two endpoints of each edge coincide, in which case the candidate labeling is admissible with induced flow f. Quotienting out ε: (4) admits an ε for given t ⟺ D_f(t) = d̄_g, where d̄_g := ([d_e])_e. The coefficient map D_f is independent of gauge; gauge enters only the data (d̄, b).

Lemma 2.5 (Coset Compatibility; Self-Contained Version of the Local Equivalence in [1])　Let h ∈ Γ\{0}, A = a+⟨h⟩, B = b+⟨h⟩ be cosets. Then A = B ⟺ a+b ∈ ⟨h⟩ ⟺ there exists a unique ε ∈ F₂ such that a+b+εh = 0. Taking a = t_u+g_u,e, b = t_v+g_v,e, h = f(e): the candidate sets at the two endpoints of edge e are equal ⟺ ∃!ε_e satisfying the e-th equation in (4). Moreover, for any t_v and gauge, the three candidate sets at v are precisely the three 2-element subsets of some 3-element set, so condition (1) is automatically satisfied at each vertex; thus a “candidate labeling with matching endpoint sets” is an admissible labeling with induced flow f.

Proof　A = B ⟺ a ∈ b+⟨h⟩ ⟺ a+b ∈ {0, h}; the two cases correspond to ε = 0 and ε = 1, respectively, and are mutually exclusive (since h ≠ 0), so ε is unique. Local admissibility: denote the gauge as (a,b) with c the third edge, x := f(a), y := f(b), z := f(c) = x+y; substituting the g-values from Definition 2.4 directly, the three candidate sets are {t, t+x}, {t+x, t+x+y} = {t+x, t+z}, {t, t+z}. Since x, z are distinct and nonzero (Observation 2.3), {t, t+x, t+z} is a 3-element set; the label t appears in the first and third sets, t+x in the first and second, t+z in the second and third — each exactly 2 times, all other labels 0 times — condition (1) holds. Induced flow: the element-wise sums of the three sets are x, y, z = f evaluated at the three edges. ∎

Lemma 2.6 (CDC Lemma; Self-Contained Version of Lemma 2.1 in [1])　Let P be an admissible labeling. Then the degree of each vertex v in M_s is 0 or 2, so M_s is a disjoint union of cycles; each edge belongs to exactly two M_s‘s; hence the family of nonempty M_s‘s constitutes a cycle double cover of G.

Proof　The degree of v in M_s equals the number of times s appears among the sets of the three edges incident to v, which lies in {0, 2} by condition (1). A subgraph with all degrees in {0,2} has no vertices of degree 1, hence is a disjoint union of cycles. |P_e| = 2 implies each edge belongs to exactly two M_s‘s. ∎

§3 Bridging Theorem: 142857 → GF(8) Coordinates → Fano Intrinsic Geometry

This laboratory’s work 142857 and Galois Theory [16] takes {1,2,4} ⊂ (Z/7Z)^× as its pivot (the root cause of the base-100 Midy partition, since 100 ≡ 2 mod 7).

Bridging Theorem　Let α be a root of x³+x+1 over F₂ (a generator of F₈^×). Then (i) α+α²+α⁴ = 0 and the three elements are mutually distinct and nonzero — the Frobenius orbit {α, α², α⁴} is itself a line in the Fano plane; (ii) the exponent set {1,2,4} ⊂ Z/7 is a (7,3,1)-difference set = the set of quadratic residues mod 7 = the cyclotomic coset of 2; (iii) the action of Gal(F₈/F₂) = ⟨x↦x²⟩ on the exponents is i↦2i (mod 7), equivariantly consistent with the action of ⟨σ₂⟩ (σ₂: ζ₇↦ζ₇²) on the exponents in Q(ζ₇). Phrasing (V5.1 calibrated): after choosing a primitive element α and exponent coordinates, the following five kinds of objects — a subgroup of (Z/7)^×, an orbit of a cyclotomic field automorphism subgroup, a Frobenius orbit in GF(8), a Fano difference set, and a Fano line — form an equivariant correspondence; they belong to different categories and can be naturally related but are not literally identical.

Proof　(i) α³ = α+1 ⟹ α⁴ = α·α³ = α²+α ⟹ α+α²+α⁴ = 0. Distinctness (order argument): α ∈ F₈^× so ord(α) | 7. If α² = α then α ∈ F₂, but x³+x+1 has no roots in F₂; if α⁴ = α then α³ = 1, ord(α) | gcd(3,7) = 1, so α = 1, but 1+1+1 = 1 ≠ 0; if α⁴ = α² then α² = 1, ord(α) | gcd(2,7) = 1 — same contradiction. (ii) The pairwise differences ±1, ±2, ±3 ≡ {1,6,2,5,3,4} (mod 7) are all distinct, i.e., a (7,3,1)-difference set; 1 = 1², 2 = 3², 4 = 2² are the quadratic residues; 2·1 = 2, 2·2 = 4, 2·4 ≡ 1 form the ⟨2⟩-coset. (iii) (αⁱ)² = α²ⁱ and (ζⁱ)^σ₂ = ζ²ⁱ: both are the order-3 action of multiplication by 2 on Z/7. ∎

Structural correspondence memo (not at theorem level): the optimal pedagogical group Z/6 ≅ Z₂×Z₃ in [16] is precisely the group of Seymour’s 6-flow, explicitly abandoned by the original proof — the Z₃ component destroys the characteristic-2 mechanism; Aut(Petersen) = S₅ ⊃ A₅, and the six pentagonal double covers form a hemi-dodecahedral face set. Additionally: [16]’s original webpage contains an imprecise expression “10 as a prime Frobenius” (10 is not a prime; the correct formulation is the mod-7 automorphism σ₁₀ = σ₃); a corrigendum note on the original page has been recommended; this paper does not adopt that expression.

§4 Theorem A: Orbit Dichotomy for Flows

Theorem A (Orbit Dichotomy)　Let G be a cubic bridgeless graph and f a nowhere-zero Γ-flow. Then |Orb(f)| ∈ {42, 168}; moreover |Orb(f)| = 42 ⟺ dim U_f = 2 ⟺ the value set of f is a Fano line and constitutes a proper 3-edge-coloring (in which case |Stab(f)| = 4); otherwise dim U_f = 3, the stabilizer is trivial, and the orbit has size 168.

Proof　σ·f = f ⟺ σ fixes f(E) pointwise ⟺ σ|_{U_f} = id, so Stab(f) = {σ : σ|_{U_f} = id}. At any vertex, the two distinct nonzero values are linearly independent over F₂ (x = y is the only dependence relation), so dim U_f ≥ 2. If dim = 3: σ fixes a basis, hence σ = id, and the orbit has size 168/1. If dim = 2 (write U_f = W): the three values at each vertex are distinct and contained in W\{0} (exactly three elements), so the value set is the line W\{0} and uses all three colors at every vertex — a proper 3-edge-coloring. A linear map fixing W pointwise is determined by σ(x) for any x ∉ W: σ(x) = x+w (w ∈ W gives four choices, all invertible and fixing W), so |Stab| = 4 and the orbit has size 168/4 = 42. ∎

Corollary A.1　G is not properly 3-edge-colorable ⟺ the action is free ⟺ every orbit has size 168; in this case 168 | F(G,8).

Proof　3-edge-colorable ⟺ there exists a flow whose value set is contained in a line (take the three points of that line as the color set; the vertex sum is zero) ⟺ there exists a 42-orbit ⟺ the action is not free. When all orbits have size 168, divisibility follows from orbit decomposition. ∎

Remark A.2 (Divisibility Does Not Reverse)　The implication “168 | F(G,8) ⟹ G is not 3-edge-colorable” is false: the disjoint union of four triple-parallel-edge dipoles is 3-edge-colorable, yet F = 42⁴ = 3,111,696 = 168 × 18,522. (This is the content of Erratum 13.3.)

Check A.3 (K₄)　K₄ is 3-edge-colorable; F(K₄,8) = 7·6·5 = 210 = 168+42; machine verification confirms its flows decompose into exactly one 168-orbit and one 42-orbit, with the latter having a value set spanning a plane, stabilizer of exactly 4 elements, and constituting a proper 3-edge-coloring (Appendix A).

§5 Theorem B: Admissible Triangle Torsor and Gauge Quotient

Lemma B.1 (Triangle Lemma)　Condition (1) holds at a cubic vertex ⟺ the three sets P_e on the incident edges are exactly the three 2-element subsets of some 3-element set T_v (the triangle); in this case, the three pairwise sums of T_v are mutually distinct, nonzero, and sum to zero (forming a Fano line), and are precisely σ(P_e). Hence the induced map of an admissible labeling is a nowhere-zero Γ-flow.

Proof　(⇐) The three 2-element subsets of {A,B,C} are {A,B}, {B,C}, {A,C}: each element belongs to exactly two subsets, and elements outside the set belong to zero — condition (1). (⇒) Three binary sets occupy 6 positions in total, with each label appearing an even number of times. If two sets are identical: the third being equal gives labels appearing 3 times each; intersecting in one point gives that point appearing 3 times; being disjoint gives elements appearing 1 time — all violating (1). Hence all three sets are distinct; even multiplicities with total 6 imply exactly three labels each appearing 2 times; “a label in two sets” means the two sets intersect at that point, and the three intersection points are distinct (if two pairs share the same intersection, the two sets share two elements and hence are equal) — the three sets are the three pairs of a 3-point set. Pairwise sums: distinct and nonzero (since elements are distinct; A+B = B+C ⟹ A = C), total sum = 2(A+B+C) = 0. Flow condition: at each vertex Σσ(P_e) = 0; nonzero since |P_e| = 2. ∎

Theorem B (Torsor and Gauge Quotient)　Fix a flow f. A 3-element set T is called admissible at vertex v if its set of pairwise sums equals the set of three flow values at v; an admissible T has a unique difference-matching pairing P_e(T) for each edge. Then (i) translation by Γ acts freely and transitively on the set of admissible triangles — this set is a Γ-torsor (8 elements, no preferred origin); (ii) under any gauge, the map t_v ↦ candidate triangle is a bijection from Γ to this torsor, and the pairing is the difference-matching pairing — gauge is a choice of coordinate origin, not a degree of freedom of the labeling space; (iii) after fixing a global gauge, solutions (t, ε) of (4) ⟷ compatible admissible triangle assignments (compatible: the pairing from both endpoints of each edge agree; ε is uniquely determined by t); the global (t, gauge) parameterization has 6^|V(G)|-fold redundancy (six-fold at each vertex). Hence any property formulated in terms of labelings is gauge-independent in its feasibility.

Proof　Denote the edges at v as a, b, c with gauge (a,b), x := f(a), y := f(b), z := f(c) = x+y. The candidate sets are {t, t+x} (edge a), {t+x, t+x+y} = {t+x, t+z} (edge b), {t, t+z} (edge c); the union is T(t) = t+{0,x,z}; pairwise sums are x, (t+x)+(t+z) = y, z — matching by differences. Transitivity: any admissible {A,B,C}, labeled so that A+B = x; if A+C = z then the set = A+{0,x,z}; if A+C = y then the set = A+{0,x,y} = (A+x)+{0,x,z} (since x+{0,x,z} = {0,x,y}). Freeness: a nonzero translation δ stabilizing a 3-element set must permute it with no fixed points, but ⟨δ⟩ ≅ Z₂ has orbits of length 1 or 2, which cannot partition 3 elements. Hence the 8 translates are distinct, t ↦ T(t) is a bijection. (iii) By Lemma 2.5: given t, ∃ε ⟺ the candidate sets from both endpoints coincide; ε_e is uniquely read off from “which representative of the opposite coset equals t_u+g_u,e“; combined with the bijection this gives solutions ⟷ compatible assignments. The six gauges yield shapes {0, f(first edge), f(third edge)} running through {0,x,y}, {0,x,z}, {0,y,z} each twice, related by translations; under each gauge, t traverses the same torsor: 48 per-vertex parameters cover the 8 triangles six-fold, giving 6^|V|-fold global redundancy. ∎

§6 Theorem C: Bidirectional Characterization of Force

Lemma C.1 (Translation Equivariance)　Γ acts on labelings by (c·P)_e := c+P_e, preserving admissibility and the induced flow, and mapping “s₀ ∈ P_e” to “s₀+c ∈ (c·P)_e“. Hence forcing an arbitrary label s₀ is equivalent to forcing 0; hereafter we set s₀ = 0.

Proof　s ∈ c+P_e ⟺ s+c ∈ P_e, so the occurrence count of each label is permuted by translation, remaining in {0,2}; σ(c+{p,q}) = (c+p)+(c+q) = p+q. ∎

Lemma C.2 (Boundary Triangle; Pin Values Always Exist and Are Unique)　Let v ∈ V(C), with cycle edges e₁, e₂ and third edge e₃. Then “0 ∈ P_e₁ and 0 ∈ P_e₂” uniquely forces T_v = {0, f(e₁), f(e₂)}, and this triangle is necessarily admissible. Hence under any gauge, the pin value t_v (the coordinate of the forced triangle) always exists and is unique; all infeasibility is of a global-extension nature.

Proof　Each element of the triangle belongs to exactly two pairs, so the condition ⟺ 0 ∈ T and the pair not containing 0 is assigned to e₃. Write T = {0, p, q}: the two pairs containing 0 have pairwise sums p and q; difference-matching requires {p, q} = {f(e₁), f(e₂)} — unique. Admissibility: the pairwise sums are f(e₁), f(e₂), f(e₁)+f(e₂) = f(e₃) (the vertex flow condition). The pin value is the unique preimage of this admissible triangle under the torsor bijection (Theorem B(ii)). ∎

Theorem C (Force; Bidirectional)　Define Force(f, C) := there exists a compatible admissible triangle assignment taking the forced values of Lemma C.2 on V(C). Then (i) Force(f,C) ⟺ there exists an admissible labeling with induced flow f such that C is a connected component of M₀; (ii) the definition is gauge-free; (iii) Force(σ·f, C) = Force(f, C) for all σ ∈ GL(3,2).

Proof　(⟹) By Lemma C.2: at cycle vertices, 0 belongs to exactly the two pairs assigned to cycle edges and not to the pair assigned to the third edge, so the degree of M₀ at cycle vertices restricted to incident edges is exactly the two cycle edges — no edge in M₀ leaves C; since C is connected and 2-regular, it is a connected component. For cycle edges e = uv, the pairing from both endpoints is {0, f(e)} (in both T_u and T_v the pair with pairwise sum f(e) is the same), so compatibility is automatic. (⟸) Given an admissible labeling P with C as a component of M₀, we have C ⊆ M₀, i.e., 0 ∈ P_e for every cycle edge; hence at each v ∈ V(C) both cycle-edge pairs contain 0, and by the uniqueness in Lemma C.2 the triangle is the forced triangle; the compatible assignment corresponding to P (Lemma B.1) takes forced values on V(C). (Note: C ⊆ M₀ suffices — condition (1) forbids 0 from appearing 3 times at a vertex, so the third edge at a cycle vertex is automatically excluded; C is a union of components, and being connected, is a component.) (iii) σ maps admissible triangles of f to admissible triangles of σf (σ(T) has pairwise sums = σ(pairwise sums)), preserving difference-matching and compatibility; σ(0) = 0 preserves the forced form {0, f(e₁), f(e₂)} ↦ {0, σf(e₁), σf(e₂)}; the reverse direction follows from σ⁻¹. ∎

§7 Theorem D: Lower Bound on the Forcing Class Number

Theorem D　Any admissible labeling witnessing Force(f,C) has class number k ≥ 1 + |f(C)|.

Proof　Every cycle-edge pair is {0, f(e)} (from the proof of Theorem C), so the set of labels used by the labeling contains {0} ∪ f(C); hence the number of nonempty classes is at least 1+|f(C)|. ∎

§8 Theorem Ω: Unconditional Obstruction, Natural Equivariance, and Short Exact Sequence

Lemma Ω.1 (Coordinate Change Identity)　Let g, g′ be two global gauges. Then at each vertex v there exists a unique q_v ∈ Γ such that (i) shape translation: S_g′,v = S_g,v + q_v; (ii) per-edge coset identity: g′_v,e ≡ g_v,e + q_v (mod ⟨f(e)⟩) for all three edges incident to v. Therefore d̄_g′ = d̄_g + D_f(q), b_g′ = b_g + ρ_C(q) — the data pair shifts by exactly D_f,C(q) under a gauge change. The entire argument consists of identities and uses no solvability assumption.

Proof　Both shapes are admissible triangles (candidate triangles at t = 0); by the free transitivity of the torsor (Theorem B), there exists a unique translation q_v. The edge-pairing of the same triangle is identical under both parameterizations (the pairing is uniquely determined by the triangle and the differences); as a set, the pairing is the coset t+g_v,e+⟨f(e)⟩; with the corresponding parameter t′ = t+q_v (from the shape translation and freeness), comparing cosets for the same edge gives g_v,e ≡ q_v+g′_v,e, i.e., (ii). Hence [d′_e] = [g′_u,e+g′_v,e] = [g_u,e+g_v,e]+[q_u+q_v] = (d̄+D_f(q))_e. The pin value is the coordinate of the forced triangle: b′_v+S_g′,v = T_forced = b_v+S_g,v ⟹ b′_v = b_v+q_v. ∎

Theorem Ω (Unconditional Obstruction Class)　Fix an arbitrary global gauge; let d̄, b be as above. Define Ω(f,C) := [(d̄, b)] ∈ coker D_f,C. Then (i) by Lemma Ω.1, Ω is gauge-independent — well-defined; (ii) Force(f,C) ⟺ Ω(f,C) = 0, without presupposing solvability of the base system, hence independent of [1].

Proof　(ii) The forcing system is solvable ⟺ ∃t: D_f(t) = d̄ and ρ_C(t) = b ⟺ (d̄, b) ∈ im D_f,C ⟺ Ω = 0; the left-hand side is Force by Definition 2.4, Theorem B(iii), and Theorem C. ∎

Theorem Ω.2 (Natural Equivariance)　For σ ∈ GL(3,2): each edge has a well-defined isomorphism σ̂_e: Γ/⟨f(e)⟩ → Γ/⟨σf(e)⟩, [x] ↦ [σx] (since σ⟨f(e)⟩ = ⟨σf(e)⟩); assembling σ̂ := ⊕σ̂_e and σ_C := σ^V(C) gives a codomain isomorphism, with the commutation relation (σ̂ ⊕ σ_C) ∘ D_f,C = D_σf,C ∘ σ^V, which induces an isomorphism σ̂_*: coker D_f,C → coker D_σf,C, satisfying σ̂_*Ω(f,C) = Ω(σf,C). Corollary: Ω(f,C) = 0 ⟺ Ω(σf,C) = 0 — orbit invariance at the numerical level. (Note: the two obstructions live in different cokernel spaces, so bare equality cannot be written; the correct statement is precisely this natural equivariance.)

Proof　Commutation, component by component: D_σf(σt)_e = [σt_u+σt_v] = σ̂_e([t_u+t_v]); ρ_C(σt) = σ_C(ρ_Ct). Data transport: take the gauge g of f; for σf define a gauge with the same edge ordering, whose g-values are σ(g_v,e) (since σ0 = 0), so d^σf_e = σ(d_e), d̄^σf = σ̂(d̄); the forced triangle of σf is {0, σf(e₁), σf(e₂)} = σ(T_forced), and σ(b_v)+σ(S) = σ(b_v+S) gives b^σf = σ_C(b). Hence (d̄^σf, b^σf) = (σ̂⊕σ_C)(d̄, b); taking cokernel classes on both sides, and invoking the gauge-independence of Ω (Theorem Ω(i)) to justify this gauge choice, yields the result. ∎

Proposition Ω.3 (Short Exact Sequence)　For each pair (f, C) there is a short exact sequence of F₂-vector spaces

0 → coker R_C →^ι coker D_f,C →^π_* coker D_f → 0,

where π_* is induced by projection onto ⊕Q_e, and ι([b′]) := [(0, b′)]. Interpretation: Ω is the total obstruction; π_*Ω = [d̄] ∈ coker D_f is the base obstruction (its vanishing is equivalent to solvability of the base system — always guaranteed by Lemma 2.2 of [1], tracked independently in this framework); when the base obstruction vanishes, Ω ∈ ι(coker R_C), and its preimage is the relative obstruction ω.

Proof　π∘D_f,C = D_f, so π induces a well-defined π_*; π is surjective, hence so is π_*. ι is well-defined: if b′ = R_C(k) (k ∈ K_f) then (0, b′) = D_f,C(k), so the class is zero. ι is injective: [(0, b′)] = 0 ⟺ ∃t: D_f(t) = 0 and ρ_C(t) = b′ ⟺ b′ ∈ im R_C. Exactness at the middle: π_*[(x, b)] = 0 ⟺ x = D_f(t) for some t ⟺ [(x, b)] = [(x, b) − D_f,C(t)] = [(0, b−ρ_C(t))] ∈ im ι. ∎

Corollary Ω.4 (Relative Reduction and Solution Count)　If the base system is solvable (guaranteed by [1]; not re-proved or relied upon here), take any solution t*. Then Ω = 0 ⟺ ω(f,C) := [b − ρ_C(t*)] ∈ coker R_C vanishes; when feasible, the set of forced solutions is a coset of ker R_C, with cardinality 2^{dim ker R_C}.

Proof　The solution set of (4) is t*+K_f; forcing ⟺ ∃k: ρ_C(t*+k) = b ⟺ b−ρ_C(t*) ∈ im R_C; the solution set is a coset of ker R_C. (This is also the explicit representation of the preimage of Ω along ι in Proposition Ω.3.) ∎

Computational Verification Ω.5 (Petersen)　170 orbits: Ω = 0 ⟺ the pinned system is solvable (zero mismatch); the number of forced solutions = 2^{dim ker R_C} (zero mismatch). Distribution (dim K_f, rank R_C, dim ker R_C, Ω=0 | orbit count): (3,3,0,no|65), (3,3,0,yes|15), (4,3,1,yes|5), (4,4,0,no|45), (4,4,0,yes|30), (5,5,0,yes|10). Empirical pattern: R_C is injective on 165/170 orbits; ν = 2 ⟹ Ω = 0 (10/10); for ν = 0/1, the feasibility rates are 15/80 and 35/80, respectively.

Status Note (Sober Positioning): The core of Theorem Ω is a structural packaging of the standard linear algebra fact “Ax = b is solvable ⟺ [b] = 0 ∈ coker A”; it is not a deep theorem in itself. Its value lies in: promoting Force from an algorithmic Boolean value to an algebraic object; unifying positive witnesses and negative left-kernel certificates within the same framework (§12); and providing an explicit carrier and natural-transformation language for the vanishing problem. Top-tier value must come from a graph-theoretic description of coker D_f,C and large-scale vanishing theorems — the task of V6, not accomplished in this paper.

§9 Computational Theorem E: Complete Classification for the Petersen Graph

Object: the Petersen graph (10 vertices, 15 edges, cycle-space dimension 6), with the prescribed cycle being the outer pentagon. 28,560 nowhere-zero flows = 170 free orbits × 168 (all value sets span Γ, consistent with Theorem A: the Petersen graph is not 3-edge-colorable). Decision procedure: choose an arbitrary gauge (permitted by Theorem B), compute the unique pin value via Lemma C.2, solve the F₂-linear system; completeness follows from the bijection in Theorem B(iii) and the uniqueness in Lemma C.2; full coverage is guaranteed by the orbit invariance of Theorem C(iii).

Criterion	Result	Support
Gauge independence (two-program comparison)	170/170 consistent	Machine verification of Theorem B
Force-feasible orbits (= Ω vanishing)	60 / 170 (10,080 flows, 35.3%)	65 positive witnesses + 110 negative left-kernel certificates (§13)
\|f(C)\| = 3	All 25 orbits infeasible	Necessary condition: feasible ⟹ \|f(C)\| ≥ 4
\|f(C)\| = 4 / 5	Feasible: 45/85 and 15/60	Separating invariant is finer (§15, Problem 1)
Complete classification of forced solutions	40×(1 sol, 5 classes), 5×(2 sol, all 5 classes), 15×(1 sol, 6 classes)	Matches 2^{dim ker R_C} on each orbit; Theorem D lower bound is attained throughout
Component condition	65/65 witnesses have the pentagon as a component of M₀	Machine verification of Theorem C(i)

Known-Fact Boundary: the fact that any cycle in the Petersen graph extends to some CDC is already known (strong CDC verified for all snarks with ≤36 vertices, [13][14], cited indirectly); the contribution of this paper is the stratification, witnesses, and obstructions within this construction, not the existence of the extension itself.

§10 Computational Theorem F: Exhaustive Enumeration of the Solution Space and the Invariant ν

Lemma F.1 (Well-Definedness and Orbit Invariance of ν)　Let L_f(t,ε)_e := t_u+t_v+ε_ef(e). For σ ∈ GL(3,2), define Φ_σ(t,ε) := (σ∘t, ε) and Ψ_σ((x_e)) := (σx_e). Then L_σf ∘ Φ_σ = Ψ_σ ∘ L_f; both are linear isomorphisms, so dim ker L_σf = dim ker L_f; gauge changes only the right-hand side, not L_f, so the kernel dimension is gauge-independent. The kernel always contains the translation subspace {t componentwise constant, ε = 0}, of dimension 3c(G). Hence ν_G(f) := dim ker L_f − 3c(G) ≥ 0 is a well-defined orbit invariant (for the connected Petersen graph, ν = dim ker − 3).

Proof　Edge by edge: σt_u+σt_v+ε_e·σf(e) = σ(t_u+t_v+ε_ef(e)). In the homogeneous system ε_ef(e) = t_u+t_v, and since f(e) ≠ 0 it follows that ε is determined by t, so the kernel is isomorphic to K_f; the translation t ≡ c (componentwise constant) satisfies t_u+t_v = 0, with each component choosing c independently, giving dimension 3c(G). ∎

Lemma F.2 (Profile Invariance)　σ acts by (σ·P)_e := σ(P_e), establishing a bijection between “admissible labelings with induced flow f” and “admissible labelings with induced flow σf”, preserving the forcing boundary (σ0 = 0) and permuting classes M_s ↦ M_σ(s) — the class number is preserved. Hence the number of forced solutions and the class-number profile of all solutions are orbit invariants.

Proof　σ bijects while preserving the binary-set structure and occurrence counts; σ({p,q}) has sum σ(p+q); s ∈ P_e ⟺ σ(s) ∈ σ(P_e). ∎

Computational Theorem F　Kernel dimension distribution {3:80, 4:80, 5:10} (ν-distribution 80/80/10); the class-number pattern of all solutions has four modes: 80×[8 solutions, all 5-class], 60×[16 solutions, all 5-class], 20×[8+8], 10×[24+8] (all counts are multiples of 8, i.e., translation orbits); every orbit has at least one solution with exactly 5 classes (exhaustive, certified by full re-enumeration under certificate v3).

§11 Classical Lower Bound and Attainment

Classical Lemma (Explicitly Stated in [18][19][20])　A graph has a double cover by at most 4 even subgraphs ⟺ it has a nowhere-zero 4-flow. The Petersen graph has no nowhere-zero 4-flow, so any even-subgraph double cover of it requires at least 5 classes (Theorem 9 of [20], directly applied to the Petersen graph).

Attainment Theorem (This Paper)　The OpenAI construction produces admissible labelings with exactly 5 classes on all 170 flow orbits of the Petersen graph — attaining the classical lower bound on every orbit; among these, 45 orbits simultaneously achieve forcing of the prescribed pentagon with 5 classes (attaining equality in Theorem D).

§12 Duality Obstruction Theorem (Gateway to V6)

Duality Obstruction Theorem　Ω(f,C) ≠ 0 if and only if there exist dual data: for each edge e a functional λ_e ∈ Q_e^* — identified via pullback with {φ ∈ Γ^* : φ(f(e)) = 0} — and for each v ∈ V(C) a functional μ_v ∈ Γ^*, satisfying:

(i) Vertex balance: for every vertex w, Σ_e∋w λ_e + [w ∈ V(C)]·μ_w = 0 (in Γ^*);

(ii) Unit pairing: Σ_e λ_e(d_e) + Σ_v∈V(C) μ_v(b_v) = 1.

(λ_e(d_e) is well-defined: λ_e annihilates f(e), hence is constant on the coset [d_e].) The 110 F₂ left-kernel certificates in §13 are coordinate instances of this theorem applied to the (t, ε)-coordinate pinned system.

Proof　Finite-dimensional F₂-duality: [(d̄, b)] ≠ 0 in the cokernel ⟺ there exists a linear functional Λ on the codomain annihilating im D_f,C with Λ(d̄, b) = 1. Write Λ = ((λ_e), (μ_v)); the dual of a quotient space, pulled back, is precisely the set of Γ-functionals annihilating ⟨f(e)⟩. Λ annihilates the image ⟺ for all t ∈ Γ^V: Σ_e λ_e(t_u+t_v) + Σ_v∈C μ_v(t_v) = 0; evaluating on the basis elements t = x·δ_w (x ∈ Γ placed at vertex w): Σ_e∋w λ_e(x) + [w∈C]μ_w(x) = 0 for all x — this is (i); (ii) is a direct translation of the pairing condition. ∎

The core question for V6 is made concrete by this theorem: universal Force fails at (G, C) if and only if every flow individually admits a blocking dual (λ, μ). The task of V6 is to prove that such “simultaneous blocking of all flows” is structurally impossible — studying how dual assignments must necessarily break down as flows vary (within and across orbits), and determining the graph-theoretic structure of coker D_f,C (cycle-space / cut-space / relative cohomological interpretation).

§13 Certificate System v3 and Six-Round Adversarial Record

Two-layer structure: the first layer consists of reproducible programs (seven standard-library-only scripts, Appendix A); the second layer consists of finite witness certificates + an independent verifier (sharing no code path with the generation programs). The fundamental principle of v3: every stored field is either recomputed and verified, or does not exist. The verifier independently: enumerates all 28,560 flows and checks orbit coverage; re-solves the base and pinned systems for each orbit, independently computes the kernel dimension, exhaustively enumerates the solution set and compares it set-wise with stored witnesses (checking distinctness, completeness, and count = 2^dim); certifies all class-number profiles from Computational Theorem F; reconstructs pin values from the cycle declared in the certificate (also verifying that the declared edge set forms a single cycle and that the two files are consistent); verifies manifest hashes, byte counts, claims fields, and label ranges. Negative certificates: each of the 110 infeasible orbits is accompanied by an F₂ left-kernel certificate for the joint pinned system (45+15 rows, with row ordering canonicalized within files) (a linear-infeasibility / Fredholm-alternative certificate; “Farkas-type” is used only as an analogy): the XOR of the specified rows has all-zero coefficient part but the right-hand side equals 1 — verification requires only XOR operations, no elimination or kernel-basis computation.

Round	Attacker → Target	Method	Outcome
R1	GPT-5.6 → v1	Deleted feasible orbits; substituted by copying 5-class witnesses	Succeeded → spawned v2 (partition and index-set checks, negative certificates)
R2	Claude → v2	Six-vector test, including manifest replay with laundering	v2 rejected (but see R3)
R3	GPT-5.6 (Window 1) → v2	Deleted a forced solution (65→64); tampered with kernel-dimension field	Succeeded → spawned v3 (full-field recomputation, solution-set completeness)
R4	Claude → v3	Deleted witnesses + cover-up field modifications; field tampering; witness duplication	All rejected at the semantic level
R5	GPT-5.6 (Window 2) → v2	Variants A/B/C + D: tampered with cycle metadata in the negative certificate file	A–C already dead against v3; D also effective against v3 → v3 patch (cross-file consistency, cycle validity, claims and all metadata field checks, pin-value construction de-hardcoded)
R6	Claude → v3 (post-patch)	D1 (single-file cycle change); D2 (coordinated two-file deception: cycle changed to inner pentagram); D3 (field value 999); D4 (claims tampering)	All rejected — the key to D2: the verifier honestly rebuilds the system from the declared cycle, causing the stored data to become self-contradictory

Release Manifest (release V5.2): Python 3.12.3, platform fingerprint, UTC timestamp, generation and verification commands, expected output; determinism note: all four data JSON files are byte-identical across Python 3.12.3 and 3.13.5 in two independent environments (one per model). Engineering notes (release-repository action items): output directory parameterization, single manifest filename, immutability via Git tag / Zenodo DOI locking paper and scripts, clean failure on anomalous input. All hashes are in Appendix A.

§14 Corrections and Errata Record

13.1 Retraction (V1)　The first-round experiment erroneously modeled the edge-endpoint membership witness δ as a single shared bit, producing two spurious results: (a) the purported necessary condition ⊕_e∈Cd_e = 0; (b) the claim that “gauge is the key degree of freedom for the forcing problem.” Formally retracted; superseded by Theorems B and C. The defect was exposed by anomalous data patterns (the all-or-nothing distribution of 110 orbits × 800 random gauges with zero hits).

13.2 V2→V3　The global gauge redundancy was corrected to 6^|V|; pin values were upgraded to always existing and being unique; M₀ component closure was supplemented; the former “Theorem 3” equivalence was downgraded to a classical lemma [18][19][20]; the GF(8) calibration was clarified as a coordinatization.

13.3 V3→V4 (Responsibility: Claude Fable 5)　The spurious triple equivalence in the abstract was corrected (counterexample 42⁴ = 168×18,522; Remark A.2); in the same round: Theorem C reverse direction, Lemmas F.1/F.2, the Bridging Theorem, the obstruction class and certificate layer were added.

13.4 V4→V5　(a) The Bridging Theorem’s “α³=1 ⟹ α=0” was invalid reasoning as literally stated — replaced by an order argument (Responsibility: Claude; caught by GPT-5.6); (b) Theorem G did not declare gauge selection — superseded by Lemma Ω.1; (c) the self-containedness claim was overstated for Theorem G — superseded by unconditional Theorem Ω; (d) Verifier v1 only checked correctness of listed witnesses — v2 added partition completeness and negative certificates.

13.5 V5→V5.1　(a) “Proof same as V4, omitted” contradicted “self-contained final edition” — this version incorporates all proofs into the main text (Responsibility: Claude; identified by two-window review); (b) the bare equality “Ω is an orbit invariant” was illegitimate (the two cokernels are different spaces) — replaced by the natural equivariance theorem Ω.2; (c) the open problem “Does the set {Ω(f,C)} contain 0?” was a type error — rewritten as ∃f: Ω(f,C) = 0; (d) “Farkas duality” renamed to F₂ left kernel / linear infeasibility certificate; (e) the bridging claim “five coordinatizations of the same object” downgraded to “equivariant correspondence after choosing a primitive element”; (f) the precise-counting loopholes in Verifier v2 (deleting forced solutions, duplicating witnesses, altering kernel dimension and metadata fields, altering cycle fields all passed) were exposed by two-window attacks — v3 and its patches closed them, with the battle record incorporated into §13; (g) the manifest determinism note was corrected from three files to four files.

13.6 V5.1 → V5.2 (Per Third-Round Dense Review; Same Day)　(a) Final self-containedness gap: Definitions 2.2/2.4 and Theorem B had cited [1] for two elementary local facts — now self-proved as Lemma 2.5 (Coset Compatibility) and Lemma 2.6 (CDC), completing self-containedness in the literal sense; the global solvability from [1] (used in Corollary Ω.4) had already been explicitly declared as the sole external dependency and remains unchanged. (b) The short exact sequence phrasing was calibrated from “decomposition” to “extension/organization” — no canonical splitting is claimed. Zero changes to the core theory.

§15 Open Problems (Battleground for V6)

Core Problem (Type-Corrected Version): For a given cubic bridgeless graph G and cycle C, does there ∃ a nowhere-zero Γ-flow f such that Ω(f,C) = 0? Equivalently (by the Duality Obstruction Theorem): is it impossible for every flow to individually admit a blocking dual? Three routes: Route 1 (Closed-form criterion) — express Ω = 0 as an explicit combinatorial condition I(f,C) depending only on the graph, flow, and cycle (cycle space / cut space / rank conditions / relative cohomology); Route 2 (Infinite graph families) — prove ∀C ∃f: Ω = 0 for some nontrivial snark family via a uniform mechanism; Route 3 (Threshold theorem) — prove a general statement of the form ν_G(f) ≥ r(G,C) ⟹ Ω = 0 (the Petersen case ν=2 ⟹ vanishing is finite evidence from 10/10; R_C surjective ⟹ coker = 0 is a trivial implication, with content in a verifiable surjectivity sufficient condition). Auxiliary questions: the graph-theoretic/topological structure of coker D_f,C; the motion of Ω in orbit space; whether group averaging / Frobenius operations can force vanishing; F(G,8)/168 and ν_G as snark statistics and their relationship to oddness.

§16 Priority, Related Work, and Contribution Attribution

Classical layer: the even-subgraph symmetric difference technique (BJJ [10][15]); planar nowhere-zero flow ⟺ proper 3-edge-coloring (Tutte era [8]); ≤4 even-subgraph double cover ⟺ nowhere-zero 4-flow ([18][19][20] explicitly stated, including the Petersen application); GL(3,2)/Fano and the difference set {1,2,4} are standard knowledge; strong CDC verified for snarks with ≤36 vertices [13][14]; the left-kernel certificate for linear infeasibility is standard linear algebra; “Ax = b is solvable ⟺ [b] = 0” is a standard fact (status note in §8). Gray layer: the formulation of Theorem A and the corollary 168 | F have no explicitly found source (MathSciNet/zbMATH unchecked). Timestamped layer: the contextualization of Observation 2.3, Theorems B/C/D/Ω and Ω.1–Ω.3, the Duality Obstruction Theorem formulation, ν_G and Force, the Bridging Theorem connection layer, the complete Petersen classification, and the implementation of two-sided positive-negative certificate methods within this construction — the research object was born on 2026-07-10. Contribution Attribution: the orbit dichotomy strengthening, the torsor formulation, ν, the class number lower bound, the proposals for relative obstruction ω and unconditional Ω, the short exact sequence proposal, the Duality Theorem proposal, and four rounds of certificate attacks originated from GPT-5.6 Sol (two windows); all proofs written and verified, coordinate transformations and naturality proofs, joint-system left-kernel certificate design, seven scripts and three generations of verifiers, adversarial test suite originated from Claude Fable 5; directional decisions, bridging intuitions, timestamp and authorship policy, cross-model orchestration originated from LEECHO. Indirect Citations and Verification: [13][14] cited indirectly via [17]; [20][22] directly verified on 2026-07-12; [22] was not independently compiled.

§17 Limitations and Calibration

Computational results are limited to the Petersen graph and the outer pentagon; ν=2 ⟹ Ω=0 is finite-sample evidence, not a theorem. Theorems A–D, Ω, and the Duality Theorem are self-contained; Corollary Ω.4’s reduction uses the solvability from [1] (explicitly declared). Per cross-model calibration from the union of two windows: to the V5.2 declared scope — closed; to reliable professional paper approximately 70–78%; to strong graph-theory journal results approximately 45–55% (requires at least one result beyond the Petersen graph); to top-tier results approximately 20–30%; to mathematical-historical significance approximately 5–20% (threshold: universal Force or universal 5-CDC level universal theorems). This paper does not disguise precision as universality; its value proposition has always been: a correct, attackable, certificate-bearing object.

§18 Conclusion

Six versions, within a single day, and this apparatus has reached its final form: the Fano plane is the intrinsic space, the torsor absorbs the gauge, the prescribed-cycle problem is compressed to the vanishing of a single class, and that class now possesses naturality, a short exact sequence, a duality characterization, and two-sided finite certificates — every field has been recomputed, every attack has its battle report. Every bolt of the apparatus has been individually tightened by two mutually distrustful models. Rhetoric ends here. V6 has only one question: why can the dual blockade not simultaneously strangle all flows. The program continues.

§19 References and Appendix

[1] OpenAI. A Proof of the Cycle Double Cover Conjecture. 2026-07-10. https://cdn.openai.com/pdf/04d1d1e4-bc75-476a-97cf-49055cd98d31/cdc_proof.pdf (not peer-reviewed)

[2] OpenAI. Prompt Used for “A Proof of the Cycle Double Cover Conjecture.” 2026-07-10.

[3] G. Szekeres. Bull. Austral. Math. Soc. 8 (1973), 367–387.

[4] P. D. Seymour. Sums of circuits. Academic Press, 1979, 341–355.

[5] P. A. Kilpatrick. M.Sc. thesis, University of Cape Town, 1975.

[6] F. Jaeger. J. Combin. Theory Ser. B 26 (1979), 205–216.

[7] F. Jaeger. Ann. Discrete Math. 27 (1985), 1–12.

[8] W. T. Tutte. Canad. J. Math. 6 (1954), 80–91.

[9] P. D. Seymour. J. Combin. Theory Ser. B 30 (1981), 130–135.

[10] J.-C. Bermond, B. Jackson, F. Jaeger. J. Combin. Theory Ser. B 35 (1983), 297–308.

[11] B. Alspach, L. A. Goddyn, C.-Q. Zhang. Trans. Amer. Math. Soc. 344 (1994), 131–154.

[12] L. Goddyn. Ann. Discrete Math. 27 (1985), 13–26; Ph.D. thesis, Waterloo, 1988.

[13] J. Hägglund, K. Markström. On stable cycles and cycle double covers. 2012. (cited indirectly)

[14] G. Brinkmann, J. Goedgebeur, J. Hägglund, K. Markström. J. Combin. Theory Ser. B 103 (2013). (cited indirectly)

[15] M. Chan. A survey of the cycle double cover conjecture. Brown University.

[16] LEECHO Global AI Research Lab & Claude Opus 4.6. 142857 and Galois Theory. 2026-05-06. leechoglobalai.com (corrigendum suggestion, see end of §3)

[17] arXiv:1306.3088. (source for indirect citations [13][14])

[18] C.-Q. Zhang. Integer Flows and Cycle Covers of Graphs. Marcel Dekker, 1997.

[19] C.-Q. Zhang. Circuit Double Cover of Graphs. Cambridge University Press, 2012.

[20] L. Shi, Z. Zhang. Signed cycle double covers. Electron. J. Combin. 25(4) (2018), #P4.63. (verified 2026-07-12)

[21] Wikipedia / Wolfram MathWorld: Cycle double cover (accessed 2026-07-12).

[22] OpenAI. cdc-lean. https://github.com/openai/cdc-lean (accessed and verified 2026-07-12: kernel check endpoint theorem cycleDoubleCover_of_bridgeless, Lean v4.31.0 + pinned Mathlib, audit lists only propext/Classical.choice/Quot.sound, no sorry/admit; not independently compiled).

Appendix A · Reproducibility and Certificate Inventory (Release V5.2)　Program layer: cdc_round.py (archival, contains the retracted caliber of 13.1), field_test.py, field_test2.py, audit_gpt56.py, route1_and_certs.py, negcerts.py; verifiers certificates_verify.py/certificates_verify2.py (archival) and certificates_verify3.py (current). Certificate layer (SHA-256): orbit_representatives 83d518d7edab46d6230b484722d1f98bf39b453f7ce941308a67e457dd62f0b2 (9,154 B); force_feasible_orbits 4fdf59380864f6c72b87760063534c52b22dffc69c87577f88d2122c8cb64ea6 (14,398 B); five_class_witnesses 1f2a1fedb93ab2abfb4667531efa2345bd7403a3c2790a356b97109a182bd458 (27,326 B); force_infeasible_certificates 45ce019db03ca7e9b95f62851c2f43326cfea6898fe5ac0b96f0f50febba4799 (12,202 B). Manifest: release V5.2, Python 3.12.3, Linux x86_64; verification command python3 certificates_verify3.py <certdir>, expected output ALL CHECKS PASSED; all four data files are byte-identical across Python 3.12.3 / 3.13.5. Key figures: 28,560; 170×168; 60/110; 40/5/15; {3:80, 4:80, 5:10}; ν=2 feasible 10/10; 210 = 168+42.