Semantic invariants of the streaming complement protocol

This module interprets the protocol's canonical row scans in the finite ranked graph of width-preserving source configurations. It is deliberately independent of the later LBA compiler: all arguments concern ProtocolStep and finite graph reachability.

def CertifiedRowSystem.Complement.protocolSource {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (input : List I) : List A

The source row carried by a protocol run.

Equations

• CertifiedRowSystem.Complement.protocolSource D input = List.map D.inputCell input

@[simp]

theorem CertifiedRowSystem.Complement.length_protocolSource {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} (D : CertifiedRowSystem I A Unit Q F) (input : List I) : (protocolSource D input).length = input.length

noncomputable def CertifiedRowSystem.Complement.protocolSourceRank {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : RankVertex A input.length

The source vertex in the ranked width-|input| graph.

Equations

• CertifiedRowSystem.Complement.protocolSourceRank D input = CertifiedRowSystem.Complement.sourceRank input.length (CertifiedRowSystem.Complement.protocolSource D input) ⋯

@[simp]

theorem CertifiedRowSystem.Complement.rankRow_protocolSourceRank {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : rankRow input.length (protocolSourceRank D input) = protocolSource D input

noncomputable def CertifiedRowSystem.Complement.protocolReached {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k : ℕ) : Finset (RankVertex A input.length)

Bounded reachability in the ranked source graph.

Equations

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

@[simp]

theorem CertifiedRowSystem.Complement.protocolReached_zero {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : protocolReached D input 0 = {protocolSourceRank D input}

theorem CertifiedRowSystem.Complement.protocolReached_succ {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k : ℕ) : protocolReached D input (k + 1) = protocolReached D input k ∪ {v : RankVertex A input.length | ∃ u ∈ protocolReached D input k, rankEdge D input.length u v}

theorem CertifiedRowSystem.Complement.protocolReached_mono {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k : ℕ) : protocolReached D input k ⊆ protocolReached D input (k + 1)

theorem CertifiedRowSystem.Complement.mem_protocolReached_iff_of_plateau {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (depth : ℕ) (hplateau : protocolReached D input depth = protocolReached D input (depth + 1)) (v : RankVertex A input.length) : v ∈ protocolReached D input depth ↔ Relation.ReflTransGen (rankEdge D input.length) (protocolSourceRank D input) v

A plateau layer is the complete reflexive-transitive reachable set.

theorem CertifiedRowSystem.Complement.card_protocolReached_le_capacity {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k : ℕ) : (protocolReached D input k).card ≤ Fintype.card A ^ input.length

theorem CertifiedRowSystem.Complement.depth_succ_lt_capacity_of_card_lt {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (depth : ℕ) (hgrowth : (protocolReached D input depth).card < (protocolReached D input (depth + 1)).card) : depth + 1 < Fintype.card A ^ input.length

A strict cardinal increase leaves room for the following depth numeral.

theorem CertifiedRowSystem.Complement.sourceRejects_iff_ranked {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : SourceRejects D input ↔ ¬∃ (row : RankVertex A input.length), Relation.ReflTransGen (rankEdge D input.length) (protocolSourceRank D input) row ∧ rankFinal D input.length row

Source rejection can be stated entirely in the finite ranked graph.

noncomputable def CertifiedRowSystem.Complement.classifiedPrefix {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k outerIndex : ℕ) : Finset (RankVertex A input.length)

Vertices already classified before the current outer enumeration position.

Equations

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

@[simp]

theorem CertifiedRowSystem.Complement.mem_classifiedPrefix {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k outerIndex : ℕ) (v : RankVertex A input.length) : v ∈ classifiedPrefix D input k outerIndex ↔ v ∈ protocolReached D input (k + 1) ∧ ↑v < outerIndex

noncomputable def CertifiedRowSystem.Complement.foundFrom {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (outer : RankVertex A input.length) (selected : Finset (RankVertex A input.length)) : Bool

The Boolean accumulated while scanning old-reachable predecessors of one outer vertex.

Equations

• CertifiedRowSystem.Complement.foundFrom D input outer selected = decide (∃ inner ∈ selected, inner = outer ∨ CertifiedRowSystem.Complement.rankEdge D input.length inner outer)

@[simp]

theorem CertifiedRowSystem.Complement.foundFrom_eq_true_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (outer : RankVertex A input.length) (selected : Finset (RankVertex A input.length)) : foundFrom D input outer selected = true ↔ ∃ inner ∈ selected, inner = outer ∨ rankEdge D input.length inner outer

theorem CertifiedRowSystem.Complement.foundFrom_full_iff {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (k : ℕ) (outer : RankVertex A input.length) : foundFrom D input outer (protocolReached D input k) = true ↔ outer ∈ protocolReached D input (k + 1)

If the selected inner scan is exactly the old reachable layer, its accumulated flag is precisely membership in the next reachable layer.

theorem CertifiedRowSystem.Complement.classifiedPrefix_succ {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (depth outerIndex : ℕ) (houter : outerIndex < Fintype.card A ^ input.length) : classifiedPrefix D input depth (outerIndex + 1) = if ⟨outerIndex, houter⟩ ∈ protocolReached D input (depth + 1) then insert ⟨outerIndex, houter⟩ (classifiedPrefix D input depth outerIndex) else classifiedPrefix D input depth outerIndex

Extending the outer prefix classifies exactly its new rank.

theorem CertifiedRowSystem.Complement.card_classifiedPrefix_succ {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (depth outerIndex : ℕ) (houter : outerIndex < Fintype.card A ^ input.length) : (classifiedPrefix D input depth (outerIndex + 1)).card = if ⟨outerIndex, houter⟩ ∈ protocolReached D input (depth + 1) then (classifiedPrefix D input depth outerIndex).card + 1 else (classifiedPrefix D input depth outerIndex).card

Cardinal form of classifiedPrefix_succ.

Semantic states of a protocol run

theorem CertifiedRowSystem.Complement.hasPhase_unique {A : Type u_2} [Fintype A] {row : ProtocolRow A} {p q : ProtocolPhase} (hne : row ≠ []) (hp : HasPhase p row) (hq : HasPhase q row) : p = q

A nonempty row cannot carry two different replicated phases.

theorem CertifiedRowSystem.Complement.hasFound_unique {A : Type u_2} [Fintype A] {row : ProtocolRow A} {p q : Bool} (hne : row ≠ []) (hp : HasFound p row) (hq : HasFound q row) : p = q

A nonempty row cannot carry two different replicated Boolean flags.

@[simp]

theorem CertifiedRowSystem.Complement.foundTrack_eq_replicate_iff {A : Type u_2} [Fintype A] (row : ProtocolRow A) (found : Bool) : foundTrack row = List.replicate (List.length row) found ↔ HasFound found row

@[simp]

theorem CertifiedRowSystem.Complement.phaseTrack_eq_replicate_iff {A : Type u_2} [Fintype A] (row : ProtocolRow A) (phase : ProtocolPhase) : List.map (fun (cell : ProtocolCell A) => cell.phase) row = List.replicate (List.length row) phase ↔ HasPhase phase row

theorem CertifiedRowSystem.Complement.length_eq_of_sourceTrack_eq {A : Type u_2} [Fintype A] {old new : ProtocolRow A} (h : sourceTrack new = sourceTrack old) : List.length new = List.length old

theorem CertifiedRowSystem.Complement.row_ne_nil_of_length_eq {I : Type u_1} {A : Type u_2} [Fintype A] {row : ProtocolRow A} {input : List I} (hlen : List.length row = input.length) (hinput : input ≠ []) : row ≠ []

theorem CertifiedRowSystem.Complement.hasFound_of_foundTrack_eq {A : Type u_2} [Fintype A] {old new : ProtocolRow A} {found : Bool} (hfound : HasFound found old) (htrack : foundTrack new = foundTrack old) : HasFound found new

structure CertifiedRowSystem.Complement.RoundTracks {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount newCount : ℕ) : Prop

Tracks shared by every state inside one inductive-counting round.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length newCount
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : newCount ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card

structure CertifiedRowSystem.Complement.InnerScanTranscript {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount newCount outerIndex innerIndex : ℕ) (selected : Finset (RankVertex A input.length)) extends CertifiedRowSystem.Complement.RoundTracks D input row depth oldCount newCount : Prop

Transcript of the partial canonical inner scan for one outer vertex. selected contains precisely the old-reachable rows for which a path witness was supplied so far; soundness only needs the subset and cardinal facts recorded here.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length newCount
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : newCount ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card
• outer_lt : outerIndex < Fintype.card A ^ input.length
• inner_le : innerIndex ≤ Fintype.card A ^ input.length
• outer_eq : outerTrack row = vertexNumeral input.length outerIndex
• inner_eq : innerTrack row = vertexNumeral input.length innerIndex
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length innerIndex
• classified_exact : newCount = (classifiedPrefix D input depth outerIndex).card
• found_eq : HasFound (foundFrom D input ⟨outerIndex, ⋯⟩ selected) row

structure CertifiedRowSystem.Complement.RoundStartInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount : ℕ) extends CertifiedRowSystem.Complement.RoundTracks D input row depth oldCount 0 : Prop

A boundary state at the start of a counting round.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length 0
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : 0 ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card
• phase : HasPhase ProtocolPhase.roundStart row
• seen_zero : seenCountTrack row = countNumeral input.length 0
• outer_zero : outerTrack row = vertexNumeral input.length 0
• inner_zero : innerTrack row = vertexNumeral input.length 0
• path_zero : pathTrack row = vertexNumeral input.length 0
• fuel_zero : fuelTrack row = vertexNumeral input.length 0
• found_false : HasFound false row

structure CertifiedRowSystem.Complement.ChooseInnerInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount newCount outerIndex innerIndex : ℕ) (selected : Finset (RankVertex A input.length)) extends CertifiedRowSystem.Complement.InnerScanTranscript D input row depth oldCount newCount outerIndex innerIndex selected : Prop

A state ready either to skip the current inner row or start its path witness.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length newCount
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : newCount ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card
• outer_lt : outerIndex < Fintype.card A ^ input.length
• inner_le : innerIndex ≤ Fintype.card A ^ input.length
• outer_eq : outerTrack row = vertexNumeral input.length outerIndex
• inner_eq : innerTrack row = vertexNumeral input.length innerIndex
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length innerIndex
• classified_exact : newCount = (classifiedPrefix D input depth outerIndex).card
• found_eq : HasFound (foundFrom D input ⟨outerIndex, ⋯⟩ selected) row
• inner_lt : innerIndex < Fintype.card A ^ input.length
• phase : HasPhase ProtocolPhase.chooseInner row
• path_zero : pathTrack row = vertexNumeral input.length 0
• fuel_zero : fuelTrack row = vertexNumeral input.length 0

structure CertifiedRowSystem.Complement.CountingPathInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount newCount outerIndex innerIndex : ℕ) (selected : Finset (RankVertex A input.length)) (pathIndex fuel : ℕ) extends CertifiedRowSystem.Complement.InnerScanTranscript D input row depth oldCount newCount outerIndex innerIndex selected : Prop

State inside a bounded path witness for the current inner row.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length newCount
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : newCount ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card
• outer_lt : outerIndex < Fintype.card A ^ input.length
• inner_le : innerIndex ≤ Fintype.card A ^ input.length
• outer_eq : outerTrack row = vertexNumeral input.length outerIndex
• inner_eq : innerTrack row = vertexNumeral input.length innerIndex
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length innerIndex
• classified_exact : newCount = (classifiedPrefix D input depth outerIndex).card
• found_eq : HasFound (foundFrom D input ⟨outerIndex, ⋯⟩ selected) row
• inner_lt : innerIndex < Fintype.card A ^ input.length
• phase : HasPhase ProtocolPhase.path row
• path_lt : pathIndex < Fintype.card A ^ input.length
• fuel_le : fuel ≤ depth
• path_eq : pathTrack row = vertexNumeral input.length pathIndex
• fuel_eq : fuelTrack row = vertexNumeral input.length fuel
• path_reachable : ⟨pathIndex, ⋯⟩ ∈ protocolReached D input fuel

structure CertifiedRowSystem.Complement.FinishOuterInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount newCount outerIndex : ℕ) (selected : Finset (RankVertex A input.length)) extends CertifiedRowSystem.Complement.InnerScanTranscript D input row depth oldCount newCount outerIndex (Fintype.card A ^ input.length) selected : Prop

The inner enumeration has overflowed and the current outer classification is ready to be committed. A malformed run may arrive here with too few witnesses; the next action's exact-count check then blocks it.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length newCount
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : newCount ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card
• outer_lt : outerIndex < Fintype.card A ^ input.length
• inner_le : Fintype.card A ^ input.length ≤ Fintype.card A ^ input.length
• outer_eq : outerTrack row = vertexNumeral input.length outerIndex
• inner_eq : innerTrack row = vertexNumeral input.length (Fintype.card A ^ input.length)
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length (Fintype.card A ^ input.length)
• classified_exact : newCount = (classifiedPrefix D input depth outerIndex).card
• found_eq : HasFound (foundFrom D input ⟨outerIndex, ⋯⟩ selected) row
• phase : HasPhase ProtocolPhase.finishOuter row
• path_zero : pathTrack row = vertexNumeral input.length 0
• fuel_zero : fuelTrack row = vertexNumeral input.length 0

structure CertifiedRowSystem.Complement.FinishRoundInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth oldCount newCount : ℕ) extends CertifiedRowSystem.Complement.RoundTracks D input row depth oldCount newCount : Prop

Boundary state after every outer vertex has been classified.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• oldCount_eq : oldCountTrack row = countNumeral input.length oldCount
• newCount_eq : newCountTrack row = countNumeral input.length newCount
• depth_lt : depth < Fintype.card A ^ input.length
• oldCount_le : oldCount ≤ Fintype.card A ^ input.length
• newCount_le : newCount ≤ Fintype.card A ^ input.length
• oldCount_exact : oldCount = (protocolReached D input depth).card
• phase : HasPhase ProtocolPhase.finishRound row
• nextCount_exact : newCount = (protocolReached D input (depth + 1)).card
• seen_zero : seenCountTrack row = countNumeral input.length 0
• outer_zero : outerTrack row = vertexNumeral input.length 0
• inner_zero : innerTrack row = vertexNumeral input.length 0
• path_zero : pathTrack row = vertexNumeral input.length 0
• fuel_zero : fuelTrack row = vertexNumeral input.length 0
• found_false : HasFound false row

structure CertifiedRowSystem.Complement.FinalTracks {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth count : ℕ) : Prop

Tracks shared by the final all-nonfinal scan after an exact count plateau.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• count_eq : oldCountTrack row = countNumeral input.length count
• depth_lt : depth < Fintype.card A ^ input.length
• count_le : count ≤ Fintype.card A ^ input.length
• count_exact : count = (protocolReached D input depth).card
• plateau : protocolReached D input depth = protocolReached D input (depth + 1)
• found_false : HasFound false row

structure CertifiedRowSystem.Complement.FinalScanTranscript {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth count innerIndex : ℕ) (selected : Finset (RankVertex A input.length)) extends CertifiedRowSystem.Complement.FinalTracks D input row depth count : Prop

Partial transcript of the final canonical scan.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• count_eq : oldCountTrack row = countNumeral input.length count
• depth_lt : depth < Fintype.card A ^ input.length
• count_le : count ≤ Fintype.card A ^ input.length
• count_exact : count = (protocolReached D input depth).card
• plateau : protocolReached D input depth = protocolReached D input (depth + 1)
• found_false : HasFound false row
• inner_le : innerIndex ≤ Fintype.card A ^ input.length
• inner_eq : innerTrack row = vertexNumeral input.length innerIndex
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length innerIndex
• selected_nonfinal (v : RankVertex A input.length) : v ∈ selected → ¬rankFinal D input.length v

structure CertifiedRowSystem.Complement.FinalChooseInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth count innerIndex : ℕ) (selected : Finset (RankVertex A input.length)) extends CertifiedRowSystem.Complement.FinalScanTranscript D input row depth count innerIndex selected : Prop

State ready to skip or witness the current row in the final scan.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• count_eq : oldCountTrack row = countNumeral input.length count
• depth_lt : depth < Fintype.card A ^ input.length
• count_le : count ≤ Fintype.card A ^ input.length
• count_exact : count = (protocolReached D input depth).card
• plateau : protocolReached D input depth = protocolReached D input (depth + 1)
• found_false : HasFound false row
• inner_le : innerIndex ≤ Fintype.card A ^ input.length
• inner_eq : innerTrack row = vertexNumeral input.length innerIndex
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length innerIndex
• selected_nonfinal (v : RankVertex A input.length) : v ∈ selected → ¬rankFinal D input.length v
• inner_lt : innerIndex < Fintype.card A ^ input.length
• phase : HasPhase ProtocolPhase.finalChoose row
• path_zero : pathTrack row = vertexNumeral input.length 0
• fuel_zero : fuelTrack row = vertexNumeral input.length 0

structure CertifiedRowSystem.Complement.FinalPathInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth count innerIndex : ℕ) (selected : Finset (RankVertex A input.length)) (pathIndex fuel : ℕ) extends CertifiedRowSystem.Complement.FinalScanTranscript D input row depth count innerIndex selected : Prop

State inside a final-scan reachability witness.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• count_eq : oldCountTrack row = countNumeral input.length count
• depth_lt : depth < Fintype.card A ^ input.length
• count_le : count ≤ Fintype.card A ^ input.length
• count_exact : count = (protocolReached D input depth).card
• plateau : protocolReached D input depth = protocolReached D input (depth + 1)
• found_false : HasFound false row
• inner_le : innerIndex ≤ Fintype.card A ^ input.length
• inner_eq : innerTrack row = vertexNumeral input.length innerIndex
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length innerIndex
• selected_nonfinal (v : RankVertex A input.length) : v ∈ selected → ¬rankFinal D input.length v
• inner_lt : innerIndex < Fintype.card A ^ input.length
• phase : HasPhase ProtocolPhase.finalPath row
• path_lt : pathIndex < Fintype.card A ^ input.length
• fuel_le : fuel ≤ depth
• path_eq : pathTrack row = vertexNumeral input.length pathIndex
• fuel_eq : fuelTrack row = vertexNumeral input.length fuel
• path_reachable : ⟨pathIndex, ⋯⟩ ∈ protocolReached D input fuel

structure CertifiedRowSystem.Complement.FinalFinishInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) (row : ProtocolRow A) (depth count : ℕ) (selected : Finset (RankVertex A input.length)) extends CertifiedRowSystem.Complement.FinalScanTranscript D input row depth count (Fintype.card A ^ input.length) selected : Prop

The final enumeration has overflowed and awaits its exact-count check.

• length_eq : List.length row = input.length
• source_eq : sourceTrack row = protocolSource D input
• depth_eq : depthTrack row = vertexNumeral input.length depth
• count_eq : oldCountTrack row = countNumeral input.length count
• depth_lt : depth < Fintype.card A ^ input.length
• count_le : count ≤ Fintype.card A ^ input.length
• count_exact : count = (protocolReached D input depth).card
• plateau : protocolReached D input depth = protocolReached D input (depth + 1)
• found_false : HasFound false row
• inner_le : Fintype.card A ^ input.length ≤ Fintype.card A ^ input.length
• inner_eq : innerTrack row = vertexNumeral input.length (Fintype.card A ^ input.length)
• seen_eq : seenCountTrack row = countNumeral input.length selected.card
• selected_reachable : selected ⊆ protocolReached D input depth
• selected_prefix : selected ⊆ rankPrefix input.length (Fintype.card A ^ input.length)
• selected_nonfinal (v : RankVertex A input.length) : v ∈ selected → ¬rankFinal D input.length v
• phase : HasPhase ProtocolPhase.finalFinish row
• path_zero : pathTrack row = vertexNumeral input.length 0
• fuel_zero : fuelTrack row = vertexNumeral input.length 0

Local preservation lemmas

theorem CertifiedRowSystem.Complement.initialized_roundStartInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] (D : CertifiedRowSystem I A Unit Q F) {input : List I} (hinput : input ≠ []) : RoundStartInvariant D input (initializedProtocolRow (protocolSource D input)) 0 1

The canonical boot target is the initial exact count state (depth = 0, count = 1).

theorem CertifiedRowSystem.Complement.beginRound_preserves {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} {depth count : ℕ} (hinv : RoundStartInvariant D input old depth count) (hstep : BeginRoundSpec old new) : ChooseInnerInvariant D input new depth count 0 0 0 ∅

Entering a round creates the empty inner-scan transcript at outer and inner rank zero.

theorem CertifiedRowSystem.Complement.skipInner_preserves {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} {depth oldCount newCount outerIndex innerIndex : ℕ} {selected : Finset (RankVertex A input.length)} (hinv : ChooseInnerInvariant D input old depth oldCount newCount outerIndex innerIndex selected) (hstep : SkipInnerSpec old new) : innerIndex + 1 < Fintype.card A ^ input.length ∧ ChooseInnerInvariant D input new depth oldCount newCount outerIndex (innerIndex + 1) selected ∨ innerIndex + 1 = Fintype.card A ^ input.length ∧ FinishOuterInvariant D input new depth oldCount newCount outerIndex selected

Skipping the current inner row advances its canonical rank. The last rank moves to finishOuter; every earlier rank stays in chooseInner.

theorem CertifiedRowSystem.Complement.finishOuter_preserves {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} {depth oldCount newCount outerIndex : ℕ} {selected : Finset (RankVertex A input.length)} (hinput : input ≠ []) (hinv : FinishOuterInvariant D input old depth oldCount newCount outerIndex selected) (hstep : FinishOuterSpec old new) : have nextCount := (classifiedPrefix D input depth (outerIndex + 1)).card; outerIndex + 1 < Fintype.card A ^ input.length ∧ ChooseInnerInvariant D input new depth oldCount nextCount (outerIndex + 1) 0 ∅ ∨ outerIndex + 1 = Fintype.card A ^ input.length ∧ FinishRoundInvariant D input new depth oldCount nextCount

Committing an exhaustively checked outer row advances the outer enumeration and the exact next-layer count.

theorem CertifiedRowSystem.Complement.finishRound_preserves {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} {depth oldCount newCount : ℕ} (hinput : input ≠ []) (hinv : FinishRoundInvariant D input old depth oldCount newCount) (hstep : FinishRoundSpec old new) : FinalChooseInvariant D input new depth oldCount 0 ∅ ∨ RoundStartInvariant D input new (depth + 1) newCount

Finishing an exact count round either records a genuine plateau and starts the final scan, or advances to the next exact depth/count pair.

theorem CertifiedRowSystem.Complement.finalSkip_preserves {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} {depth count innerIndex : ℕ} {selected : Finset (RankVertex A input.length)} (hinv : FinalChooseInvariant D input old depth count innerIndex selected) (hstep : FinalSkipSpec old new) : innerIndex + 1 < Fintype.card A ^ input.length ∧ FinalChooseInvariant D input new depth count (innerIndex + 1) selected ∨ innerIndex + 1 = Fintype.card A ^ input.length ∧ FinalFinishInvariant D input new depth count selected

Skipping a row in the final scan advances the same canonical enumeration.

theorem CertifiedRowSystem.Complement.finalFinish_rejects {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {old new : ProtocolRow A} {depth count : ℕ} {selected : Finset (RankVertex A input.length)} (hinput : input ≠ []) (hinv : FinalFinishInvariant D input old depth count selected) (hstep : FinalFinishSpec old new) : SourceRejects D input ∧ HasPhase ProtocolPhase.accept new ∧ List.length new = input.length

The exact final scan proves that every globally reachable ranked row is nonfinal.

inductive CertifiedRowSystem.Complement.ProtocolInvariant {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : ProtocolRow A → Prop

Full semantic invariant covering every control phase of a protocol run.

• input {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} : ProtocolInvariant D input (List.map (inputProtocolCell D.inputCell) input)
• roundStart {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth count : ℕ} : RoundStartInvariant D input row depth count → ProtocolInvariant D input row
• chooseInner {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth oldCount newCount outerIndex innerIndex : ℕ} {selected : Finset (RankVertex A input.length)} : ChooseInnerInvariant D input row depth oldCount newCount outerIndex innerIndex selected → ProtocolInvariant D input row
• countingPath {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth oldCount newCount outerIndex innerIndex : ℕ} {selected : Finset (RankVertex A input.length)} {pathIndex fuel : ℕ} : CountingPathInvariant D input row depth oldCount newCount outerIndex innerIndex selected pathIndex fuel → ProtocolInvariant D input row
• finishOuter {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth oldCount newCount outerIndex : ℕ} {selected : Finset (RankVertex A input.length)} : FinishOuterInvariant D input row depth oldCount newCount outerIndex selected → ProtocolInvariant D input row
• finishRound {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth oldCount newCount : ℕ} : FinishRoundInvariant D input row depth oldCount newCount → ProtocolInvariant D input row
• finalChoose {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth count innerIndex : ℕ} {selected : Finset (RankVertex A input.length)} : FinalChooseInvariant D input row depth count innerIndex selected → ProtocolInvariant D input row
• finalPath {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth count innerIndex : ℕ} {selected : Finset (RankVertex A input.length)} {pathIndex fuel : ℕ} : FinalPathInvariant D input row depth count innerIndex selected pathIndex fuel → ProtocolInvariant D input row
• finalFinish {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} {depth count : ℕ} {selected : Finset (RankVertex A input.length)} : FinalFinishInvariant D input row depth count selected → ProtocolInvariant D input row
• accept {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} : SourceRejects D input → HasPhase ProtocolPhase.accept row → List.length row = input.length → ProtocolInvariant D input row

theorem CertifiedRowSystem.Complement.ProtocolInvariant.length_eq {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} (hinv : ProtocolInvariant D input row) : List.length row = input.length

theorem CertifiedRowSystem.Complement.ProtocolInvariant.rejects_of_accept {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] {D : CertifiedRowSystem I A Unit Q F} {input : List I} {row : ProtocolRow A} (hinv : ProtocolInvariant D input row) (haccept : HasPhase ProtocolPhase.accept row) (hne : row ≠ []) : SourceRejects D input

Compiled versus semantic protocol reachability

theorem CertifiedRowSystem.Complement.compiledProtocolAccepts_iff_protocolAccepts {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : CompiledProtocolAccepts D input ↔ ProtocolAccepts D input

Replacing the integrated finite scanner by its declarative action union preserves all finite protocol runs.

theorem CertifiedRowSystem.Complement.mem_deterministicComplementSystem_iff_protocolAccepts {I : Type u_1} {A : Type u_2} {Q : Type u_3} {F : Type u_4} [Fintype A] [Nonempty A] [DecidableEq A] [Fintype Q] [Fintype F] (D : CertifiedRowSystem I A Unit Q F) (input : List I) : input ∈ (deterministicComplementSystem D).rowReachLanguage ↔ input ≠ [] ∧ ProtocolAccepts D input

Membership in the compiled deterministic-source complement is semantic protocol acceptance, together with the certified-row model's nonempty-input convention.