Ranked fixed-width rows

The complement protocol enumerates width-n source rows as least-significant-first numerals. This file packages that enumeration as the finite vertex type Fin (|A| ^ n) and records the arithmetic facts used by the semantic proof.

@[reducible, inline]

abbrev CertifiedRowSystem.Complement.RankVertex (A : Type u_5) [Fintype A] (n : ℕ) : Type

Ranks of all width-n rows over A.

Equations

• CertifiedRowSystem.Complement.RankVertex A n = Fin (Fintype.card A ^ n)

noncomputable def CertifiedRowSystem.Complement.rankRow {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (v : RankVertex A n) : List A

The row at a given rank in the protocol's canonical enumeration.

Equations

• CertifiedRowSystem.Complement.rankRow n v = (CertifiedRowSystem.Complement.vertexCodec A).nextRow^[↑v] ((CertifiedRowSystem.Complement.vertexCodec A).zeroRow n)

@[simp]

theorem CertifiedRowSystem.Complement.length_rankRow {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (v : RankVertex A n) : (rankRow n v).length = n

noncomputable def CertifiedRowSystem.Complement.rankOfRow {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (row : List A) (hlen : row.length = n) : RankVertex A n

Rank a row whose length is known to be n.

Equations

• CertifiedRowSystem.Complement.rankOfRow n row hlen = ⟨(CertifiedRowSystem.Complement.vertexCodec A).value row, ⋯⟩

@[simp]

theorem CertifiedRowSystem.Complement.rankRow_rankOfRow {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (row : List A) (hlen : row.length = n) : rankRow n (rankOfRow n row hlen) = row

@[simp]

theorem CertifiedRowSystem.Complement.rankOfRow_rankRow {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (v : RankVertex A n) : rankOfRow n (rankRow n v) ⋯ = v

noncomputable def CertifiedRowSystem.Complement.rankRowEquiv {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) : RankVertex A n ≃ { row : List A // row.length = n }

Canonical equivalence between ranks and width-indexed list rows.

Equations

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

def CertifiedRowSystem.Complement.rankEdge {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) (n : ℕ) : RankVertex A n → RankVertex A n → Prop

The rank graph induced by a certified row system at one fixed width.

Equations

• CertifiedRowSystem.Complement.rankEdge D n old new = D.RowStep (CertifiedRowSystem.Complement.rankRow n old) (CertifiedRowSystem.Complement.rankRow n new)

def CertifiedRowSystem.Complement.rankFinal {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) (n : ℕ) : RankVertex A n → Prop

The final predicate transported to ranked rows.

Equations

• CertifiedRowSystem.Complement.rankFinal D n row = D.Final (CertifiedRowSystem.Complement.rankRow n row)

noncomputable def CertifiedRowSystem.Complement.sourceRank {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (source : List A) (hlen : source.length = n) : RankVertex A n

The ranked source vertex corresponding to a concrete source row.

Equations

• CertifiedRowSystem.Complement.sourceRank n source hlen = CertifiedRowSystem.Complement.rankOfRow n source hlen

@[simp]

theorem CertifiedRowSystem.Complement.rankRow_sourceRank {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) (source : List A) (hlen : source.length = n) : rankRow n (sourceRank n source hlen) = source

@[simp]

theorem CertifiedRowSystem.Complement.rankEdge_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) (n : ℕ) (old new : RankVertex A n) : rankEdge D n old new ↔ D.RowStep (rankRow n old) (rankRow n new)

A ranked edge preserves the intended list-level edge exactly.

theorem CertifiedRowSystem.Complement.rankReach_sound {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) (n : ℕ) {old new : RankVertex A n} (h : Relation.ReflTransGen (rankEdge D n) old new) : Relation.ReflTransGen D.RowStep (rankRow n old) (rankRow n new)

Ranked reachability maps to source-row reachability.

theorem CertifiedRowSystem.Complement.rankReach_complete {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) (n : ℕ) {old : RankVertex A n} {row : List A} (h : Relation.ReflTransGen D.RowStep (rankRow n old) row) : ∃ (new : RankVertex A n), rankRow n new = row ∧ Relation.ReflTransGen (rankEdge D n) old new

Every list-level path starting at a ranked row stays at the fixed width and can be transported back to the rank graph.

theorem CertifiedRowSystem.Complement.rankReach_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) (n : ℕ) (old new : RankVertex A n) : Relation.ReflTransGen (rankEdge D n) old new ↔ Relation.ReflTransGen D.RowStep (rankRow n old) (rankRow n new)

Reachability between ranked endpoints is exactly list-level row reachability.

Canonical numeral rows

noncomputable def CertifiedRowSystem.Complement.vertexNumeral {A : Type u_2} [Fintype A] [Nonempty A] (n k : ℕ) : List A

The canonical width-n source-alphabet numeral for the natural number k. Values outside the row capacity wrap around; semantic uses always carry an in-range proof.

Equations

• CertifiedRowSystem.Complement.vertexNumeral n k = (CertifiedRowSystem.Complement.vertexCodec A).nextRow^[k] ((CertifiedRowSystem.Complement.vertexCodec A).zeroRow n)

@[simp]

theorem CertifiedRowSystem.Complement.vertexNumeral_zero {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) : vertexNumeral n 0 = (vertexCodec A).zeroRow n

@[simp]

theorem CertifiedRowSystem.Complement.length_vertexNumeral {A : Type u_2} [Fintype A] [Nonempty A] (n k : ℕ) : (vertexNumeral n k).length = n

theorem CertifiedRowSystem.Complement.value_vertexNumeral {A : Type u_2} [Fintype A] [Nonempty A] {n k : ℕ} (hk : k < Fintype.card A ^ n) : (vertexCodec A).value (vertexNumeral n k) = k

theorem CertifiedRowSystem.Complement.vertexNumeral_injective {A : Type u_2} [Fintype A] [Nonempty A] {n i j : ℕ} (hi : i < Fintype.card A ^ n) (hj : j < Fintype.card A ^ n) : vertexNumeral n i = vertexNumeral n j ↔ i = j

theorem CertifiedRowSystem.Complement.nextRow_vertexNumeral {A : Type u_2} [Fintype A] [Nonempty A] (n k : ℕ) : (vertexCodec A).nextRow (vertexNumeral n k) = vertexNumeral n (k + 1)

theorem CertifiedRowSystem.Complement.increment_vertexNumeral_overflow_iff {A : Type u_2} [Fintype A] [Nonempty A] {n k : ℕ} (hk : k < Fintype.card A ^ n) : ((vertexCodec A).increment (vertexNumeral n k)).2 = true ↔ k + 1 = Fintype.card A ^ n

@[simp]

theorem CertifiedRowSystem.Complement.vertexNumeral_capacity {A : Type u_2} [Fintype A] [Nonempty A] (n : ℕ) : vertexNumeral n (Fintype.card A ^ n) = vertexNumeral n 0

def CertifiedRowSystem.Complement.countNumeral {A : Type u_2} [Fintype A] (n k : ℕ) : List (CountDigit A)

The canonical width-n larger-radix count numeral.

Equations

• CertifiedRowSystem.Complement.countNumeral n k = (CertifiedRowSystem.Complement.countCodec A).nextRow^[k] ((CertifiedRowSystem.Complement.countCodec A).zeroRow n)

@[simp]

theorem CertifiedRowSystem.Complement.countNumeral_zero {A : Type u_2} [Fintype A] (n : ℕ) : countNumeral n 0 = (countCodec A).zeroRow n

@[simp]

theorem CertifiedRowSystem.Complement.countCodec_radix {A : Type u_2} [Fintype A] : (countCodec A).radix = Fintype.card A + 1

@[simp]

theorem CertifiedRowSystem.Complement.length_countNumeral {A : Type u_2} [Fintype A] (n k : ℕ) : (countNumeral n k).length = n

theorem CertifiedRowSystem.Complement.value_countNumeral {A : Type u_2} [Fintype A] {n k : ℕ} (hk : k < (Fintype.card A + 1) ^ n) : (countCodec A).value (countNumeral n k) = k

theorem CertifiedRowSystem.Complement.countNumeral_injective {A : Type u_2} [Fintype A] {n i j : ℕ} (hi : i < (Fintype.card A + 1) ^ n) (hj : j < (Fintype.card A + 1) ^ n) : countNumeral n i = countNumeral n j ↔ i = j

theorem CertifiedRowSystem.Complement.nextRow_countNumeral {A : Type u_2} [Fintype A] (n k : ℕ) : (countCodec A).nextRow (countNumeral n k) = countNumeral n (k + 1)

theorem CertifiedRowSystem.Complement.increment_countNumeral_overflow_iff {A : Type u_2} [Fintype A] {n k : ℕ} (hk : k < (Fintype.card A + 1) ^ n) : ((countCodec A).increment (countNumeral n k)).2 = true ↔ k + 1 = (Fintype.card A + 1) ^ n

theorem CertifiedRowSystem.Complement.rowCapacity_lt_countCapacity {A : Type u_2} [Fintype A] {n : ℕ} (hn : 0 < n) : Fintype.card A ^ n < (Fintype.card A + 1) ^ n

The larger-radix count track can represent every number up to the number of width-n source rows, provided the physical row is nonempty.

theorem CertifiedRowSystem.Complement.countNumeral_injective_of_le_rowCapacity {A : Type u_2} [Fintype A] {n i j : ℕ} (hn : 0 < n) (hi : i ≤ Fintype.card A ^ n) (hj : j ≤ Fintype.card A ^ n) : countNumeral n i = countNumeral n j ↔ i = j

Count numerals are injective throughout the complete range of possible reachable vertex counts.

theorem CertifiedRowSystem.Complement.countNumeral_one {A : Type u_2} [Fintype A] [Nonempty A] {n : ℕ} (hn : 0 < n) : countNumeral n 1 = (countCodec A).oneRow ⋯ n

The first successor of the zero count row is the boot scanner's LSD-first numeral one.

Prefixes of the canonical vertex enumeration

def CertifiedRowSystem.Complement.rankPrefix {A : Type u_2} [Fintype A] (n i : ℕ) : Finset (RankVertex A n)

The first i ranked vertices.

Equations

• CertifiedRowSystem.Complement.rankPrefix n i = {v : CertifiedRowSystem.Complement.RankVertex A n | ↑v < i}

@[simp]

theorem CertifiedRowSystem.Complement.mem_rankPrefix {A : Type u_2} [Fintype A] {n i : ℕ} (v : RankVertex A n) : v ∈ rankPrefix n i ↔ ↑v < i

@[simp]

theorem CertifiedRowSystem.Complement.rankPrefix_zero {A : Type u_2} [Fintype A] (n : ℕ) : rankPrefix n 0 = ∅

theorem CertifiedRowSystem.Complement.rankPrefix_mono {A : Type u_2} [Fintype A] {n i j : ℕ} (hij : i ≤ j) : rankPrefix n i ⊆ rankPrefix n j

@[simp]

theorem CertifiedRowSystem.Complement.rankPrefix_capacity {A : Type u_2} [Fintype A] (n : ℕ) : rankPrefix n (Fintype.card A ^ n) = Finset.univ

theorem CertifiedRowSystem.Complement.rankPrefix_succ {A : Type u_2} [Fintype A] {n i : ℕ} (hi : i < Fintype.card A ^ n) : rankPrefix n (i + 1) = insert ⟨i, hi⟩ (rankPrefix n i)

theorem CertifiedRowSystem.Complement.card_rankPrefix {A : Type u_2} [Fintype A] {n i : ℕ} (hi : i ≤ Fintype.card A ^ n) : (rankPrefix n i).card = i