@[implemented_by _private.HexGraphIso.Sparse.TacticSupport.0.Hex.GraphIso.Sparse.Tactic.evalNatUnsafe]

opaque Hex.GraphIso.Sparse.Tactic.evalNat (e : Lean.Expr) : Lean.MetaM Nat

def Hex.GraphIso.Sparse.Tactic.evalColored (n k : Nat) (e : Lean.Expr) : Lean.MetaM (Colored n k)

Evaluate a closed native sparse graph without constructing dense rows. All evaluated data are untrusted until the emitted kernel proof checks them.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.findWitness {n k : Nat} (maxNodes : Nat) (G H : Colored n k) : Option (Option (Perm n) × Nat)

Propose a transporter using two native searches sharing one node quota. The outer none reports exhaustion; it supplies no isomorphism verdict. The returned count is the actual combined number of admitted native visits.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.findCandidates {n k : Nat} (maxNodes maxRecords : Nat) (G H : Colored n k) : Except String (Nauty.Sparse.CertCandidate n × Nauty.Sparse.CertCandidate n)

Propose two compact certificates with a shared search quota and a record cap on each certificate. Exhaustion names the failed phase; only subsequent kernel replay can turn the candidates into a negative proof.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.tie (lhs rhs : Lean.Expr) : Lean.MetaM Lean.Expr

Prove equality with a literal through the kernel, without an elaborator evaluation of the equality's decidable instance.

Equations

• Hex.GraphIso.Sparse.Tactic.tie lhs rhs = do let __do_lift ← Lean.Meta.mkAppM `Eq #[lhs, rhs] Hex.GraphIso.Tactic.kernelDecideProof __do_lift

def Hex.GraphIso.Sparse.Tactic.proveIsIso {n k : Nat} (GE HE : Lean.Expr) (G H : Colored n k) (p : Perm n) : Lean.MetaM (Lean.Expr × Lean.Expr)

Replay an explicit forward transporter on identified sparse row, colour and permutation literals. The decisive theorem checks edges through sorted neighbour images and never materializes a dense adjacency matrix.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.proveWitness {n k : Nat} (GE HE : Lean.Expr) (G H : Colored n k) (p : Perm n) : Lean.MetaM Lean.Expr

Wrap the checked explicit transporter as native sparse isomorphism.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.graphExpr {n : Nat} (G : SparseGraph n) : Lean.MetaM Lean.Expr

Reify a sparse graph as checked undirected edge literals. The default empty graph only makes parsing total; kernel replay still checks the key.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.keyExpr {n : Nat} (B : Nauty.Sparse.Key n) : Lean.MetaM Lean.Expr

Equations

• Hex.GraphIso.Sparse.Tactic.keyExpr B = do let __do_lift ← Hex.GraphIso.Sparse.Tactic.graphExpr B.graph Lean.Meta.mkAppM `Hex.GraphIso.Nauty.Sparse.Key.mk #[Lean.toExpr B.codes, __do_lift]

partial def Hex.GraphIso.Sparse.Tactic.certExpr : Nauty.Sparse.CertNode → Lean.MetaM Lean.Expr

Preserve all sparse certificate records and their literal payloads.

def Hex.GraphIso.Sparse.Tactic.proveKey {n k : Nat} (GE : Lean.Expr) (G : Colored n k) (c : Nauty.Sparse.CertCandidate n) : Lean.MetaM (Lean.Expr × Lean.Expr)

Reify and replay an untrusted compact key certificate. A failed check supplies no canonical-key proof.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Sparse.Tactic.proveDifferent {n k : Nat} (GE HE : Lean.Expr) (G H : Colored n k) (a b : Nauty.Sparse.CertCandidate n) : Lean.MetaM Lean.Expr

Two accepted different canonical keys give a native sparse negative proof. All graph and certificate data in the proof term undergo kernel replay.

Equations

• One or more equations did not get rendered due to their size.