def Hex.GraphIso.Nauty.Sparse.Replay.sibling (check : Nat → CertNode → Option Bool) (witness : Nat → Nat → Array Nat → Bool) (seen : Array Bool) (c : CertNode) : Option Bool

Check one sibling or copy a previously checked attainment flag after validating the reference's strict order and automorphism witness.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Replay.sibling check witness seen c = check seen.size c

def Hex.GraphIso.Nauty.Sparse.Replay.scan (check : Nat → CertNode → Option Bool) (witness : Nat → Nat → Array Nat → Bool) : Array Bool → List CertNode → Option (Array Bool)

Process sibling records in order. Only successful checks enter the flag array; forward, cyclic, and out-of-range references are rejected.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Sparse.Replay.scan check witness x✝ [] = some x✝

theorem Hex.GraphIso.Nauty.Sparse.Replay.sibling_valid {P : Nat → Bool → Prop} {check : Nat → CertNode → Option Bool} {witness : Nat → Nat → Array Nat → Bool} {seen : Array Bool} {c : CertNode} {a : Bool} (hcheck : ∀ (o : Nat) (c : CertNode) (b : Bool), check o c = some b → P o b) (hcopy : ∀ (o earlier : Nat) (raw : Array Nat) (b : Bool), earlier < o → P earlier b → witness o earlier raw = true → P o b) (hs : ∀ (o : Nat), o < seen.size → P o seen[o]!) (h : sibling check witness seen c = some a) : P seen.size a

theorem Hex.GraphIso.Nauty.Sparse.Replay.scan_valid {P : Nat → Bool → Prop} {check : Nat → CertNode → Option Bool} {witness : Nat → Nat → Array Nat → Bool} {seen flags : Array Bool} {cs : List CertNode} (hcheck : ∀ (o : Nat) (c : CertNode) (b : Bool), check o c = some b → P o b) (hcopy : ∀ (o earlier : Nat) (raw : Array Nat) (b : Bool), earlier < o → P earlier b → witness o earlier raw = true → P o b) (hs : ∀ (o : Nat), o < seen.size → P o seen[o]!) (h : scan check witness seen cs = some flags) : flags.size = seen.size + cs.length ∧ ∀ (o : Nat), o < flags.size → P o flags[o]!

Every stored flag has a checked justification, and exactly one flag is stored per accepted record. This includes chains of earlier references.

theorem Hex.GraphIso.Nauty.Sparse.Replay.scan_exists {check : Nat → CertNode → Option Bool} {witness : Nat → Nat → Array Nat → Bool} {seen : Array Bool} {cs : List CertNode} (hsteps : ∀ (i : Nat) (hi : i < cs.length) (s : Array Bool), s.size = seen.size + i → ∃ (a : Bool), sibling check witness s cs[i] = some a) : ∃ (flags : Array Bool), scan check witness seen cs = some flags

A scan succeeds when each record can be checked at its actual offset. No assumptions about the values of earlier attainment flags are needed.