LanglibCanonical executable steps of the complement protocol #
The soundness proof interprets every accepted scanner action. This file supplies the converse local facts used by completeness: from each semantic boundary state, construct the canonical next protocol row and prove that the executable semantic relation accepts it.
theorem
CertifiedRowSystem.Complement.exists_beginRound_step
{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 : ProtocolRow A}
{depth count : ℕ}
(hinput : input ≠ [])
(hinv : RoundStartInvariant D input old depth count)
:
∃ (new : ProtocolRow A), ProtocolStep D old new ∧ ChooseInnerInvariant D input new depth count 0 0 0 ∅
Entering an inductive-counting round is always executable on a nonempty input.
theorem
CertifiedRowSystem.Complement.exists_skipInner_step
{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 : ProtocolRow A}
{depth oldCount newCount outerIndex innerIndex : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : ChooseInnerInvariant D input old depth oldCount newCount outerIndex innerIndex selected)
:
∃ (new : ProtocolRow A),
ProtocolStep D 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)
The canonical skip action advances the inner enumeration by one rank.
theorem
CertifiedRowSystem.Complement.exists_finalSkip_step
{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 : ProtocolRow A}
{depth count innerIndex : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : FinalChooseInvariant D input old depth count innerIndex selected)
:
∃ (new : ProtocolRow A),
ProtocolStep D old new ∧ HasFound false 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)
The canonical final-scan skip preserves the replicated auxiliary bit while advancing the ranked inner row.
theorem
CertifiedRowSystem.Complement.exists_finalFinish_step
{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 : ProtocolRow A}
{depth count : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : FinalFinishInvariant D input old depth count selected)
(hselected : selected = protocolReached D input depth)
:
∃ (new : ProtocolRow A), ProtocolStep D old new ∧ HasPhase ProtocolPhase.accept new
Once the final scan has selected the complete reachable layer, its exact-count check has a canonical accepting successor.
theorem
CertifiedRowSystem.Complement.exists_finishRound_step
{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 : ProtocolRow A}
{depth oldCount newCount : ℕ}
(hinput : input ≠ [])
(hinv : FinishRoundInvariant D input old depth oldCount newCount)
:
∃ (new : ProtocolRow A),
ProtocolStep D old new ∧ (FinalChooseInvariant D input new depth oldCount 0 ∅ ∨ RoundStartInvariant D input new (depth + 1) newCount)
The exact round boundary has an executable successor. Equality selects the plateau branch; strict growth selects the next counting round.
theorem
CertifiedRowSystem.Complement.exists_finishOuter_step
{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 : ProtocolRow A}
{depth oldCount newCount outerIndex : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : FinishOuterInvariant D input old depth oldCount newCount outerIndex selected)
(hselected : selected = protocolReached D input depth)
:
∃ (new : ProtocolRow A),
ProtocolStep D old new ∧ (outerIndex + 1 < Fintype.card A ^ input.length ∧ ChooseInnerInvariant D input new depth oldCount (classifiedPrefix D input depth (outerIndex + 1)).card
(outerIndex + 1) 0 ∅ ∨ outerIndex + 1 = Fintype.card A ^ input.length ∧ FinishRoundInvariant D input new depth oldCount (classifiedPrefix D input depth (outerIndex + 1)).card)
After the canonical inner scan has selected exactly the old reachable layer, the current outer vertex can be committed executably.