Enumeration actions of the inductive-counting protocol

These list-level specifications describe the canonical inner-vertex scan, outer-vertex scan, count-round boundary, and final rejecting scan. The synchronous scanners in Construction.lean implement exactly these predicates.

def CertifiedRowSystem.Complement.CopiesPayload {A : Type u_1} [Fintype A] (old new : ProtocolRow A) : Prop

Every track except the replicated phase is copied.

Equations

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

def CertifiedRowSystem.Complement.BeginRoundSpec {A : Type u_1} [Fintype A] (old new : ProtocolRow A) : Prop

Enter the inner scan for the current outer vertex.

Equations

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

def CertifiedRowSystem.Complement.SkipInnerSpec {A : Type u_1} [Fintype A] [Nonempty A] (old new : ProtocolRow A) : Prop

Skip the current inner vertex and advance the canonical enumeration. Overflow means every inner vertex has been considered and enters finishOuter.

Equations

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

def CertifiedRowSystem.Complement.OuterResetSpec {A : Type u_1} [Fintype A] [Nonempty A] (_old new : ProtocolRow A) : Prop

Reset all work tracks used for the next canonical outer scan.

Equations

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

def CertifiedRowSystem.Complement.FinishOuterSpec {A : Type u_1} [Fintype A] [Nonempty A] (old new : ProtocolRow A) : Prop

Finish classifying one outer vertex. Exactness of oldCount is checked by seenCount = oldCount; newCount is incremented exactly when found is true.

Equations

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

def CertifiedRowSystem.Complement.RoundResetSpec {A : Type u_1} [Fintype A] [Nonempty A] (new : ProtocolRow A) : Prop

Common zeroed work tracks at a count-round boundary.

Equations

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

def CertifiedRowSystem.Complement.FinishRoundSpec {A : Type u_1} [Fintype A] [Nonempty A] (old new : ProtocolRow A) : Prop

Finish a complete count round. Equal old and new counts prove a plateau and enter the final all-nonfinal scan. Otherwise the count must strictly increase; it becomes the next exact count while depth is incremented.

Equations

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

def CertifiedRowSystem.Complement.FinalSkipSpec {A : Type u_1} [Fintype A] [Nonempty A] (old new : ProtocolRow A) : Prop

Skip one vertex in the final canonical scan.

Equations

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

def CertifiedRowSystem.Complement.FinalFinishSpec {A : Type u_1} [Fintype A] (old new : ProtocolRow A) : Prop

The final scan accepts only after it has selected exactly the certified number of reachable, nonfinal vertices.

Equations

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