Let Jn (n≥3) denote the standard flower graph (an Isaacs flower snark for odd n≥5). Working within the labeling language of the OpenAI cycle-double-cover construction [1] (Condition (1); see [V5.2]), this paper proves the Main Theorem: for every n≥4 and every even subgraph H of Jn, there exists a valid labeling P such that H ⊆ M0(P); the exceptional set for n=3 consists of exactly 2 symmetry orbits (12 words). In particular, for every cycle C of every flower snark, there exists a nowhere-zero Γ-flow f with Force(f,C) and obstruction Ω(f,C)=0 — universal forcing holds over the infinite family. The proof follows a computer-assisted four-pillar structure: (i) hand-written semantic lemmas (word⟺even-subgraph bijection, parity lemma, petal-filling characterization with exhaustiveness, Sym7 equivariance and pair-class composition, relation-machine semantics); (ii) the complete finite state space — 3,417 reachable relation states, 13,668 transitions, BFS to empty frontier; (iii) the finite theorem check — exactly 20 rejecting states (8 from the degenerate J1, 12 being precisely the J3 exceptions), with the length-≥4 reachable set (3,250 states) disjoint from the rejecting set; (iv) cross-certification against an independent CSP oracle sharing no generation logic — exact word-by-word agreement on all 128/512/2,048 words of lengths 3/4/5 (including 12 NONE results), and lengths 6/7 upgraded to fully exhaustive in audit round R1 by the collaborator’s independent oracle (8,192 + 32,768 words, zero mismatches). Supporting results include: the triangle vanishing theorem (for all cubic bridgeless graphs), the selector exact sequence 0→Γc(G)→Kf→Sf→0, the Kempe swap lemma, and exact universal-forcing ledgers for nine finite graphs (including a complete census of all 57 cycles of the Petersen graph with the 60/40/10/5 uniform profile, and all 2,048 even subgraphs of J5 (2,047 non-empty)). The three state representations (4711/3417/18 and 49/42/18) are formally reconciled: the minimal state count is an invariant of the language, and the three numbers correspond to three different languages, with no contradiction. Status: computer-assisted theorem, pending file-by-file adversarial audit signature from the collaborator; priority literature search pending.
§1 Introduction, Positioning, and Verification Topology
This paper establishes the Level-III main theorem of the obstruction programme initiated in [V5.2]: a general result for an infinite graph family beyond Petersen. The objects of study are the labelings in the construction of [1]: each edge receives a two-element set Pe ⊆ Γ = F23, subject to Condition (1), which requires that at every vertex each label appears in exactly 0 or 2 of the three incident edges. The class family {Ms} of valid labelings forms a cycle double cover ([V5.2] Lemma 2.6, self-proved). Forcing a designated cycle C, Force(f,C), is equivalent to the vanishing of the obstruction Ω(f,C) ([V5.2] Theorem Ω), which in turn is equivalent to the existence of a valid labeling with C ⊆ M0 ([V5.2] Theorem C; C ⊆ M0 is automatically a component). This paper pushes the quantifiers to their limit: not one cycle, but every even subgraph; not one graph, but the entire infinite family.
Verification topology: The theorem is interlocked by two machines sharing zero code — an exact CSP oracle (graph-by-graph, labeling-by-labeling search) and a relation-transition machine (algebraic composition) — and cross-read by two mutually adversarial models (Claude Fable 5 and GPT-5.6 Sol). The original claims from sessions five through seven (GPT-5.6, of which the numerical results from sessions five and six were self-acknowledged as expository narrative) were independently reconstructed, sharpened, and proved through two rounds of closure in this paper; the skeleton of the “49-state automaton” claim was confirmed, and its theorem scope was strengthened by this paper (n≥5 → n≥4).
Status declaration: The theorem in this paper is a computer-assisted theorem (in the Appel–Haken paradigm): hand-written semantic layer + finite exhaustive layer + independent certification layer. Two pending items are explicitly stated: the collaborator’s file-by-file adversarial audit signature on the evidence package; MathSciNet/zbMATH-level priority search (§8).
§2 Framework Review ([V5.2])
This paper requires only the labeling layer of [V5.2] together with the following facts: the local characterization of validity (Lemma B.1: a vertex is valid ⟺ its three pairs are the three 2-element subsets of some 3-element set; two pairs determine the third, which equals their symmetric difference); the coset compatibility lemma (Lemma 2.5); the CDC lemma (Lemma 2.6); Theorem C (Force ⟺ C is a component of M0 for some valid labeling ⟺ C ⊆ M0); Theorem D (forcing class count ≥ 1+|f(C)|); and the obstruction framework Df, Df,C, Ω(f,C), RC together with Force ⟺ Ω=0. Validity is a purely combinatorial condition — invariant under every label permutation fixing 0 (Sym7, order 5040); this symmetry, far larger than the flow-layer GL(3,2), is the engine driving every quotient in this paper.
§3 General Structural Theorems
Theorem 3.1 (Triangle Vanishing) Let G be a cubic bridgeless graph, C a triangle in G with G/C loop-free, and f any nowhere-zero Γ-flow. Then Ω(f,C) = 0 — every triangle is forced by every flow.
Proof. Denote the edge values on the triangle by a, b, c (pairwise distinct and nonzero: equal values on adjacent cycle edges would force a zero exit edge). The exit edges carry values o1, o2, o3 equal to a+c, a+b, b+c. The forcing data is completely pinned: the triangle Tvi at each vertex is unique, and the three exit-edge pairs are {a,c}, {a,b}, {b,c}. The contraction G/C is cubic and bridgeless (bridgeless: every cycle in G containing oi maps to a closed walk through oi in G/C), and the flow descends to f′. Forcing extension on G ⟷ “pinning the single vertex w* with triangle T* = {a,b,c}” on G/C: T* is feasible (pairwise sums equal the three flow values at w*); the difference pairs are exactly those three exit-edge pairs; the interface is identical edge-by-edge outside. A single-vertex pinning is always satisfiable: the base system is solvable ([1] Lemma 2.2, the sole external input claimed by this programme), and ker contains the 3-dimensional global translation, whose restriction to any single vertex surjects onto Γ. ∎
Theorem 3.2 (Selector Exact Sequence) Let G be cubic and connected (the general case has c(G) components), and f a nowhere-zero flow. Define Sf := {ε ∈ F2E : Σe∈Z εe f(e) = 0 for every cycle Z} (the f-isotropic selector subspace). Then there is an exact sequence 0 → Γc(G) → Kf → Sf → 0 (Kf = ker Df; the left arrow is component-wise constant translation; the right arrow maps k ↦ ε, where εe := [ku+kv = f(e)]). Corollary: νG(f) = dim Sf.
Proof. Well-definedness: k ∈ Kf ⟹ ku+kv ∈ {0, f(e)}, and telescoping the difference along any cycle yields zero ⟹ ΣZ∩S f(e) = 0. Kernel: ε = 0 ⟺ k is constant on each component. Surjectivity: given ε ∈ Sf, the 1-form ωe := εef(e) has zero cycle-sum everywhere ⟹ ω is a tension (on each connected component it admits a potential t, unique up to a constant), and t ∈ Kf. ∎
Remark (Petersen selector dissection, machine-exact). The 110 nonzero selectors of the Petersen graph fall into exactly three types: 8-edge type ×60, 10-edge type ×30, and 12-edge (value-class union) type ×20 (whose complements are 3-edge matchings); none belongs to the cut space. The combinatorial identity of ν thereby acquires a fingerprint (certificates in the appendix).
Lemma 3.3 (Kempe Swap) Let P be a valid labeling and s ≠ s′. Then Ms Δ Ms′ is an even subgraph; swapping s ↔ s′ along any connected component Z of this even subgraph yields a valid labeling, and the induced flow changes to f + (s+s′)·1Z (still nowhere-zero).
Proof. Every edge of Z contains exactly one of s, s′; the swap exchanges the occurrence counts of s and s′ at each vertex in pairs, leaving the {0,2} values of Condition (1) intact; pair-sums shift edge-by-edge by s+s′; nowhere-zero follows from “each edge contains exactly one of the two.” ∎
Dynamical Negative Result (recorded in good faith) A naïve Kempe random/greedy hill-climbing with “count of C-edges missing 0” as potential failed 0/48 on hard classes of J5, and achieved only 1/10 even on easy classes — solutions reachable by forward construction (§5’s CSP and relation machine) are unreachable by local 0-swaps. Lemma 3.3 is retained as a structural tool; the improvement argument pathway is demoted.
§4 Exact Ledgers for Finite Graphs
The following are exact verification ledgers for universal forcing (∀C ∃f: Ω=0); all entries are exhaustive decisions unless otherwise noted. This section provides peripheral corroboration for the main theorem and is not central to it.
Graph
Scope
Result
K4
All 7 cycles
All pass; triangles 210/210 forced by every flow (instance of Theorem 3.1); 4-cycles feasible ⟺ |f(C)|=2
Triangular Prism
All 14 cycles
All pass; both C3 and C4: 1050/1050 forced by every flow
K3,3
All 15 cycles
All pass
Petersen
All 57 cycles × 170 orbits
All pass; perfectly uniform census: 5/6/8/9-cycles have exactly 60/40/10/5 feasible orbits (Aut = S5 transitive on each length ⟹ uniformity is a theorem; the sequence itself is new information: longer cycles leave thinner margins)
Tietze
All 100 cycles
All pass (witness from sampling pool)
J5
All 2,048 even subgraphs (including the empty set; 2,047 non-empty) (⊋ all 1,444 cycles)
All pass (constructed on-site; snark property verified by exact coloring search)
J7
Short cycles: 21 classes exhaustive + 212 random long-cycle classes
All pass (lengths up to 27 = n−1)
Deep data for the Petersen graph with a designated pentagon (60/110 stratification, forcing solutions 40/5/15, ν-distribution, positive and negative certificates) can be found in [V5.2] and its release V5.2 certificate package.
Attachment declaration: The generation scripts and data for this section (v6_scan / v6_session series) belong to the finite-ledger attachment and are not listed in the main theorem’s certificate package manifest; the proof of the main theorem does not depend on any entry in this section.
§5 Main Theorem: The Flower-Graph Infinite Family
5.1 Precise Definition of Jn (Convention Lock)
Definition 5.1 n ≥ 3. Vertices Ai, Bi, Ci, Di (i ∈ Zn). Spokes: ai = AiBi, bi = AiCi, ci = AiDi. Cut edges: βi = BiBi+1, γi = CiDi+1, δi = DiCi+1 (subscripts mod n). All petals follow the same rule with no special twist edges; for odd n≥5, Jn is the Isaacs flower snark [6]. Cut i := {βi, γi, δi}; Petal i owns spokes a,b,ci and cut i. Word convention: a word = n letters o0…on−1 ∈ (F23)n, where oi is the 0-demand bit of cut i (in β,γ,δ order); word length = number of petals = n, with no closing letter and closure being implicit. J1 (contains loops) falls outside the loopless-multigraph framework and is recorded only as a degenerate case; J2 is a multigraph and lies within the framework.
5.2 Words ⟺ Even Subgraphs
Lemma 5.2 (Bijection) The map H ↦ (oi) (cut trace) is a bijection between the set of even subgraphs of Jn and the set of constant-parity words; the inverse map is given by cut bits + induced spokes: ai ∈ H ⟺ oi−1β ⊕ oiβ; bi ∈ H ⟺ oi−1δ ⊕ oiγ; ci ∈ H ⟺ oi−1γ ⊕ oiδ.
Proof. Translate the vertex-degree parity condition vertex by vertex: Bi is incident to ai, βi−1, βi ⟹ the ai-bit is forced by the XOR of the two β-bits; Ci is incident to bi, δi−1, γi (δi−1 terminates at Ci, γi originates from Ci); Di follows analogously. The parity condition at Ai ⟺ the sum of the three spoke bits is even ⟺ (oi−1β⊕oiβ)+(oi−1δ⊕oiγ)+(oi−1γ⊕oiδ) = |oi−1|+|oi| ≡ 0 ⟺ adjacent letters have the same parity. Hence the cut trace of an even subgraph has constant parity and completely determines H; conversely, a constant-parity word yields via the inverse map an edge set with even degree at every vertex. The two maps are mutually inverse. ∎
Lemma 5.3 (Parity Lemma) In the three pairs of any triangle, each label appears 0 or 2 times; hence the sum of the 0-demand bits of a petal’s three spokes is necessarily even. Words with a parity jump are unrealizable — the semantic origin of the automaton’s dead state D.
Proof. Every element of a 3-element set belongs to exactly two of its 2-element subsets. The three spoke pairs are the three pairs of the Ai-triangle, and 0 appears in exactly 0 or 2 of them. ∎
Lemma 5.4 Fix the pair configuration L = (Lβ, Lγ, Lδ) at cut i−1 and the target R = (Rβ, Rγ, Rδ) at cut i. Petal i admits a valid internal labeling (spoke pairs pa, pb, pc) if and only if there exist three pairs (pa, pb, pc) from a triangle (56×6 possibilities) such that Rβ = pa ⊕ Lβ, Rγ = pb ⊕ Lδ, Rδ = pc ⊕ Lγ, with each union having cardinality 3. Exhaustiveness: This parameterization enumerates all valid labelings of the petal — vertex validity ⟺ the three pairs are the three 2-element subsets of a 3-element set ([V5.2] Lemma B.1); two pairs determine the third (the third = XOR, if and only if the two share exactly one label, i.e., union of size 3); hence the R-components at Bi, Ci, Di are forced by (spokes, L), while Ai is the triangle condition. No normalization reduction is applied. The 0-demand (left guaranteed by the upstream, right according to oi, spokes by the induced bits from Lemma 5.2) acts as a per-pair filter. Notation: The ⊕ in this lemma denotes the symmetric difference of two-element sets (which remains a two-element set when the two sets share exactly one element; under 8-bit masks this coincides numerically with bitwise XOR), distinguished from the vector addition in Γ.
5.5 Sym7 Equivariance and Pair-Class Composition
Lemma 5.5 (i) Validity and 0-demand are invariant under the label permutation group Sym7 fixing 0; the petal image map is equivariant. (ii) Configurations (sequences of three pairs) have exactly 66 orbits under Sym7 (first-appearance relabeling × 23 intra-pair flips, taking the minimum as the complete invariant). (iii) All reachable relations are Sym7-invariant (by induction: the initial identity relation is invariant + equivariant composition preserves invariance), and hence can be represented without loss as sets of diagonal orbit pair-classes (12-slot first-appearance relabeling × 26, with the complete invariant defined analogously); composition on class representatives with canonical renormalization gives exact relation composition — expand the representatives’ images and canonicalize class by class, with no information loss. In practice, 3,810 pair-classes occur.
Proof. (i) Condition (1) is a statement about occurrence counts, and 0 is fixed, so demand bits are invariant. (ii)(iii) Completeness of the first-appearance canonical form: two sequences are Sym-equivalent ⟺ they have the same label-coincidence pattern; intra-pair order ambiguity is resolved by taking the flip-minimum; the pair-class version is analogous for 12 slots. Exactness of composition: an invariant relation = the union of its classes; (L,R) ∈ 𝒮, R′ ∈ images(R) ⟹ the full orbit (σL, σR′) ∈ 𝒮∘T (by equivariance), so the class expansion is exhaustive. ∎
5.6 Relation-Machine Semantics
Proposition 5.6 Define start(o0) := the class-set of {(Q,Q) : Q ⊨ o0}; compose(𝒮, oj−1, oj) := the class-expansion of the one-petal image; closes(𝒮, on−1, o0) := ∃ a class representative (L,R) such that L ∈ images(R; on−1, o0). Then for a word w: closes(composen−1(start)) = true ⟺ there exists a valid labeling on the closed flower Jn satisfying the w-demand. The empty relation is preserved throughout (empty ⟹ permanently empty ⟹ reject).
Proof. By structural induction: after k steps, the class-set is exactly the class partition of {(Q0, Qk) : there exists an open-chain labeling satisfying the demands of the first k petals, with cut 0 taking Q0 and cut k taking Qk} — the base case follows from the definition of start and the convention that “the demand at cut 0 is re-verified at the interface of the closing petal (petal n−1…0)”; the inductive step follows from the exhaustiveness of Lemma 5.4 and the exactness of composition from Lemma 5.5(iii). The closes predicate checks precisely that petal n (with demand (on−1, o0)) connects Qn−1 back to the same Q0. ∎
5.7 Finite State Census and 5.8 Rejecting State Classification
Fact 5.7 (Machine Census) A state := (first letter, last letter, relation class-set). Starting from 8 initial states, BFS along same-parity letter transitions converges at empty frontier: 3,417 reachable states, 13,668 transitions (canonical machine SHA-256 1e7e14e7fd98384b1ba6a58ed54b7cead35f1337eff8bfc96c96d906c5023186, v1; v2 incorporates per-state rel_size — both values were co-signed via full regeneration from scratch in audit round R2). Acceptance (closes) is an intrinsic property of each state.
Proposition 5.8 (Rejecting State Dissection) There are exactly 20 rejecting states: 8 at depth 1 (length-1 words, corresponding to the degenerate J1 — contains loops, outside the theorem’s scope, recorded in good faith); 12 at depth 3, precisely the 12 exceptional words of J3, each with a replayable witness word (certificate: reject_witnesses.json). All length-2 words (multigraph J2) are accepted.
5.9 Main Theorem
Main Theorem (Universal Forcing for the Flower-Graph Infinite Family) For every n ≥ 4 and every even subgraph H of Jn, there exists a valid labeling P satisfying Condition (1) such that H ⊆ M0(P). Corollary 1: For every cycle C of every flower snark (odd n≥5), there exists a nowhere-zero Γ-flow f with Force(f,C) and Ω(f,C)=0 — universal forcing holds over the infinite family; C appears as a whole cycle in the 0-class of a CDC produced by the construction. Corollary 2 (Boundary): The exceptional set for n=3 consists of exactly two symmetry orbits (§5.11).
Proof. By Lemma 5.2, the proposition reduces to: every constant-parity word of length ≥4 is accepted. By Proposition 5.6, acceptance is exactly determined by the relation machine; by Fact 5.7, the state space is complete; acceptance is an intrinsic property of each state. Finite check: the set of states reachable at length ≥4 (forward closure from depth 4 onward, 3,250 states) and the 20 rejecting states have empty intersection (verifier check [3]). Hence all words of length ≥4 are accepted — established for all n at once. Corollary 1 follows from [V5.2] Theorem C (C ⊆ M0 ⟹ component ⟹ Force) and the fact that the induced flow is nowhere-zero (Lemma 2.6 path). ∎
5.10 Two Hand-Written Pearls
Lemma 5.10a (Dead Orbit) A configuration with all three pairs identical, (q,q,q), cannot be the output of any petal. Proof: The three triangle pairs must each share exactly one element with q, giving Σ|pair∩q| = 3; but every element of T∩q belongs to exactly 2 pairs ⟹ 2|T∩q| = 3, a contradiction. ∎
Proposition 5.10b (Intrinsic Nature of the σ-Twist) Within the all-0 kernel 𝒢 := {configurations whose three pairs all contain 0}, the spoke pairs pa = Lβ⊕Rβ etc. necessarily do not contain 0 (0 cancels out); hence a 𝒢-chain exists only when all spoke demands are zero, i.e., oi = σ(oi−1) where σ = γδ-coordinate transposition — σ-alternation is the necessary and sufficient rhythm for remaining in the all-0 kernel. The τ-acceptance in the collaborator’s convention is the orbit-system bookkeeping of this phenomenon.
5.11 The n=3 Exception Theorem
Theorem 5.11 Among the 128 constant-parity words of J3, exactly 12 are unrealizable, forming two orbits under rotation/reflection/γδ-transposition (6 each): representatives ((001),(001),(111)) and ((011),(101),(101)); 6 in each parity class. The complete table is in the certificate j3_exceptions.json; the oracle and the relation machine agree word-by-word.
§6 Formal Reconciliation of Three Representations
The minimal state count is an invariant of the language, not of the theorem. Three languages, three minimal counts, no contradiction:
Language
Word Convention
Minimal Automaton
Lplain (this paper)
Word = n letters, closure implicit, no length threshold
18 = 17 classes + INIT (includes parity dead-sink; two parity-split accepting sinks absorbing 2,097+1,288 raw states; 6 two-letter “danger memory” classes dedicated to detecting the 12 J3 assassins; complete congruence map and quotient table in the certificates)
Lscoped (collaborator’s convention)
Word contains a closing letter (n+1 letters); acceptance from the 6th letter onward ⟺ scope n≥5
49 = 1 dead + 8×6 (skeleton independently reconstructed and confirmed by this paper, differing by ε-state bookkeeping)
Ltight-scoped
Same as above; acceptance from the 5th letter onward ⟺ tight scope n≥4
42(+ε)
Language conversion proposition: w ∈ Lplain ∧ |w| ≥ 5 ⟺ w·c(w) ∈ Lscoped, where c(w) is the orbit-system closing form of w’s first letter (directly inter-translatable via the σ-bookkeeping of §5.10b and the definitions). State-count layers: 4,711 = the reachable states of the collaborator’s raw relation encoding (their internal product, not audited by us, non-load-bearing — the semantics of this paper are independent of it); 3,417 = the reachable states of this machine (Sym7 pair-class quotient × (first, last) memory); 18 = the Moore quotient of Lplain. This section in the formal manuscript serves as an explicit anti-confusion clause.
§7 Certificate System and Cross-Certification Matrix
Length
Coverage
CSP Oracle
Relation Machine
Agreement
3
All 128
116 EXISTS / 12 NONE
Same
Word-by-word identical
4
All 512
All EXISTS
All accept
Word-by-word identical
5
All 2,048 (= full even-subgraph space of J5)
All EXISTS (exact sweep)
All accept (lookup)
Word-by-word identical
6
380 adversarial + random
All EXISTS (all 4 caps broken)
All accept (covered by ∀n≥4 theorem)
Consistent
7
210 adversarial + random
All EXISTS (30 caps → all 18 classes broken)
All accept
Consistent
(111)k
k=3,…,10
Dimension-reduced exact solver: all EXISTS
All accept
Consistent
Independence declaration (verified in R1): The CSP oracle (per-graph triangle DFS: MRV + Sym7 root symmetry breaking + restarts) and the relation machine (algebraic pair-class composition) share no generation logic; both source codes are included side by side in the package. Evidence package (v6_evidence/, locked by manifest_v6.json SHA-256): transitions.json, acceptance.json, states_meta.json, pair_classes.json, machine_hash.json, minimal_dfa_18.json (congruence map + quotient table), reject_witnesses.json, j3_exceptions.json, words_3/4.json, census6/7.jsonl, caps6/7.json, closure1/2 summaries. Verifier v6_verify.py: fast mode with seven checks (table completeness / initial states / finite theorem check / reject dissection with witness replay / three-level language exhaustive comparison / quotient congruence recomputation / machine hash); full regeneration mode with head-to-head rebuild. Commands and expected outputs are in the “V6 Algorithms and Verification Document.”
Audit Record R1 (GPT-5.6 Sol, 2026-07-13) Core subset cross-audit passed: 3,417-state table structure, 18-state quotient (independent Moore recomputation matches state by state), reject dissection and J3 certificates, uploaded file hashes all passed; its zero-shared-semantic CSP upgraded n=3..7 to fully exhaustive — 43,648 words agreed with this machine 43,648/43,648 word by word (n=6: all 8,192; n=7: all 32,768; maximum search nodes: 180). Its attack on the legacy verifier succeeded once (witness key rename still passed) — prompting V6.1: manifest gating, strict witness key validation with full coverage, words_5 true-oracle word-by-word comparison, exact length-4 set (468 states, consistent with its independent measurement), canonical state ordering with –full byte-for-byte regeneration, and clean failure. Four manuscript errata were addressed in the same round (2,048/2,047 caliber, k=3,…,10, ⊕ notation, §4 attachment declaration).
Audit Record R2 (GPT-5.6 Sol, 2026-07-13)Heaviest signature obtained: The core relation machine was fully regenerated from scratch via its own c2_core+c2_rel with zero checkpoints — 3,417 states / 13,668 transitions / 3,810 pair-classes, with state-by-state matching of first/last/rel_sha/rel_size/acceptance values, the complete transition table, eight initial states, exact pair-class sets, and canonical hash all MATCH; independent CSP for n=3..7 again 43,648/43,648; R1 fixes verified via four-way coordinated tampering tests, all valid. Its compound attack (eight coordinated auxiliary-field tampers + manifest laundering) succeeded against V6.1 again — prompting V6.2: closure summary numerical-level recomputation, census five-way strict checks (row count / format / parity / uniqueness / cross-verification of key sets with caps), oracle key-set exact equality (rejecting spurious keys), v2 canonical hash incorporating rel_size, pair_classes count and –full exact set comparison, script py_compile + functional self-test, dual manifest (–core load-bearing signature channel, eliminating transmission file loss), manifest fingerprint external anchoring suggestion; c2_core’s stale “surjection lemma” diagnostic renamed to honest wording; hash and file-count calibers unified.
§8 Honest Boundaries, Calibration, and Priority
Proof modality: Computer-assisted (four pillars), not a pure hand proof; a structural theorem explaining “why all danger memories necessarily vanish beyond length ≥4” (hand-written formalization of the 18-state mechanism) is listed as open polishing (§9). Pending signature: The collaborator’s file-by-file audit according to their ten-point checklist (edge-table convention, bit offset, bijection, exhaustiveness, quotient composition, empty-relation preservation, fixed points, witness replay, quotient congruence, independence — item-by-item landing points in the verification document §6). Class-count remark: The main theorem in this paper establishes valid labelings (class count ≤ 8); “5 labels suffice” is an unaudited claim from the collaborator’s fifth session, partially supported by J5 data; the 5-class refinement for general n is listed as an open problem — this paper makes no such claim. Priority: The CDC and strong CDC properties of flower snarks in the literature (Isaacs [6], Häggkvist–McGuinness et al. directions) await MathSciNet/zbMATH verification; three contingency plans (entirely new / conclusion known but proof new / both have close precedents) have been agreed upon, and the outcome will determine the submission positioning. Calibration (quoting the collaborator’s assessment): Content-level strong professional research, postdoctoral-level maturity, competitive for solid specialist journals; not a resolution of the general CDC conjecture, not at the level of top general-interest journals, not of mathematical-history significance — this paper accepts the assessment in full.
§9 Open Problems
First (Pure hand-proof formalization): Replace the 3,417-state exhaustion with a structural argument — candidate skeleton: the all-0 kernel + σ-rhythm (5.10b) + patching lemma, or a “danger prefix” two-step memory theorem. Second (5-class refinement): Achieve the main theorem for general n using ≤5 labels. Third (Periodic module criterion): For a 3-port cubic module B and port permutation π in the family Gn(B,π), find a finite criterion P(B,π) ⟹ ∀n ∀ even H: H ⊆ M0 — the flower graph is the first instance; a second non-isomorphic instance would elevate this method to a general theory for periodic cubic graphs. Fourth (Level IV): The general battlefield ∀G ∀C ∃f: Ω(f,C)=0 — the contraction-reduction calculus (generalization of Theorem 3.1) and the dual obstruction theory of [V5.2] §12 serve as two wings.
§10 Conclusion
An obstruction class learned the language of vanishing in [V5.2]; in this paper, it falls silent once and for all across an entire infinite family. Three thousand four hundred and seventeen states, two machines that know nothing of each other, twelve named exceptions — from now on, every even subgraph of the flower-snark family holds a pass into the zero class. Level III closes here; Level IV stands only one universal quantifier away.
§11 References
[V5.2] LEECHO Global AI Research Lab & Claude Fable 5 & GPT-5.6 Sol. Galois Geometry of Cycle-Double-Cover Proofs V5.2 (Self-Contained Final Edition). 2026-07-12. With release V5.2 certificate package.
[1] OpenAI. A Proof of the Cycle Double Cover Conjecture. 2026-07-10. (Not peer-reviewed; Lean repository cdc-lean accessed and inspected, not independently compiled)
[2] G. Szekeres. Bull. Austral. Math. Soc. 8 (1973), 367–387.
[3] P. D. Seymour. Sums of circuits. Academic Press, 1979.
[4] C.-Q. Zhang. Integer Flows and Cycle Covers of Graphs. Dekker, 1997; Circuit Double Cover of Graphs. CUP, 2012.
[5] J.-C. Bermond, B. Jackson, F. Jaeger. J. Combin. Theory Ser. B 35 (1983), 297–308.
[6] R. Isaacs. Infinite families of nontrivial trivalent graphs which are not Tait colorable. Amer. Math. Monthly 82 (1975), 221–239. (Origin of flower snarks)
[7] D. Blanuša. Problem četiriju boja. Glasnik Mat.-Fiz. Astr. 1 (1946), 31–42.
[8] A. B. Appel, W. Haken. Every planar map is four colorable. 1977. (Precedent for the computer-assisted proof modality)
Appendix (Certificate Pointers) Evidence package evidence/ (17 data files); dual manifest: manifest_v6.json (full package, 32 files) and manifest_core.json (load-bearing core, 17 files, for core signature under transmission-limited channels); verifier v6_verify.py V6.2 (default full check [0]–[9] / –core core signature / –full byte-for-byte regeneration with rel_size and pair-class sets); algorithms and verification document V6_ALGORITHMS_AND_VERIFICATION.md; generation scripts c2_core.py / c2_rel.py / c2_census.py (relation machine) and v7_auto.py / v7_chunk.py / v7_census2.py / v7_caps.py (CSP oracle); finite graph ledger scripts v6_scan.py / v6_session2-4 series. Verification command: python3 v6_verify.py <release_dir> (release V6.1 is a single directory v6_release: paper, document, verifier V6.2, seven generation scripts, audit archive, and evidence/ with all 17 data files, dual manifest with full coverage); expected final line: RESULT: ALL CHECKS PASSED.
