def Hex.GraphIso.Nauty.Sparse.Quota.collect (f : Nat → Nat → Option (CertNode × Nat)) : List Nat → Nat → Option (List CertNode × Nat)

Produce siblings in order, passing only the unused record quota to the next sibling. Failure stops the walk before producing another record.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Quota.collect f [] x✝ = some ([], x✝)

def Hex.GraphIso.Nauty.Sparse.Quota.emit (choose : Nat → Option (Nat × Array Nat)) (witness : Nat → Nat → Array Nat → Bool) (fallback : Nat → Nat → Option (CertNode × Nat)) (o remaining : Nat) : Option (CertNode × Nat)

An automorphism reference costs one record. Failed proposals delegate to the lazy bounded fallback without consuming an additional record.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Quota.collect_budget {f : Nat → Nat → Option (CertNode × Nat)} {os : List Nat} {remaining final : Nat} {cs : List CertNode} (hf : ∀ (o : Nat), o ∈ os → ∀ (q : Nat) (c : CertNode) (rest : Nat), f o q = some (c, rest) → c.stats.records + rest = q) (h : collect f os remaining = some (cs, final)) : (CertNode.statsList cs).records + final = remaining

The sibling traversal charges exactly the records it actually returns.

theorem Hex.GraphIso.Nauty.Sparse.Quota.emit_budget {choose : Nat → Option (Nat × Array Nat)} {witness : Nat → Nat → Array Nat → Bool} {fallback : Nat → Nat → Option (CertNode × Nat)} {o remaining final : Nat} {c : CertNode} (hf : ∀ (q : Nat) (c : CertNode) (rest : Nat), fallback o q = some (c, rest) → c.stats.records + rest = q) (h : emit choose witness fallback o remaining = some (c, final)) : c.stats.records + final = remaining

theorem Hex.GraphIso.Nauty.Sparse.Quota.collect_eq {f : Nat → Nat → Option (CertNode × Nat)} {plain : Nat → CertNode} {os : List Nat} {remaining final : Nat} {cs : List CertNode} (hf : ∀ (o : Nat), o ∈ os → ∀ (q : Nat) (c : CertNode) (rest : Nat), f o q = some (c, rest) → c = plain o) (h : collect f os remaining = some (cs, final)) : cs = List.map plain os

Quota threading retains every successfully produced sibling verbatim.

theorem Hex.GraphIso.Nauty.Sparse.Quota.emit_eq {choose : Nat → Option (Nat × Array Nat)} {witness : Nat → Nat → Array Nat → Bool} {fallback : Nat → Nat → Option (CertNode × Nat)} {plain : Nat → CertNode} {o remaining final : Nat} {c : CertNode} (hf : ∀ (q : Nat) (c : CertNode) (rest : Nat), fallback o q = some (c, rest) → c = plain o) (h : emit choose witness fallback o remaining = some (c, final)) : c = Replay.emit choose witness plain o

A successful bounded emission is exactly the unlimited emission.

theorem Hex.GraphIso.Nauty.Sparse.Quota.collect_complete {f : Nat → Nat → Option (CertNode × Nat)} {plain : Nat → CertNode} (os : List Nat) (remaining : Nat) (hf : ∀ (o : Nat), o ∈ os → ∀ (q : Nat), (plain o).stats.records ≤ q → f o q = some (plain o, q - (plain o).stats.records)) (hq : (CertNode.statsList (List.map plain os)).records ≤ remaining) : collect f os remaining = some (List.map plain os, remaining - (CertNode.statsList (List.map plain os)).records)

A quota covering all sibling records suffices for their sequential production, with exactly their total cost subtracted.

theorem Hex.GraphIso.Nauty.Sparse.Quota.emit_complete {choose : Nat → Option (Nat × Array Nat)} {witness : Nat → Nat → Array Nat → Bool} {fallback : Nat → Nat → Option (CertNode × Nat)} {plain : Nat → CertNode} (o remaining : Nat) (hf : ∀ (q : Nat), (plain o).stats.records ≤ q → fallback o q = some (plain o, q - (plain o).stats.records)) (hq : (Replay.emit choose witness plain o).stats.records ≤ remaining) : emit choose witness fallback o remaining = some (Replay.emit choose witness plain o, remaining - (Replay.emit choose witness plain o).stats.records)

A reference or fallback succeeds when its actual record size fits. Proposals that fail checking consume no record before the fallback.