LanglibSemantic preservation for bounded path witnesses #
This module connects the path-action specifications to the ranked finite-graph
invariants used by the inductive-counting proof. It is kept separate from
ProtocolSemantics.lean so the declarative invariant layer does not depend on the
action-by-action preservation proof.
Starting a witness #
theorem
CertifiedRowSystem.Complement.startsPath_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 : StartsPath ProtocolPhase.chooseInner ProtocolPhase.path old new)
:
CountingPathInvariant D input new depth oldCount newCount outerIndex innerIndex selected (↑(protocolSourceRank D input))
0
Starting an ordinary witness copies the round transcript, resets fuel to zero, and places the path at the ranked source vertex.
theorem
CertifiedRowSystem.Complement.finalStartsPath_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 innerIndex : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinv : FinalChooseInvariant D input old depth count innerIndex selected)
(hstep : StartsPath ProtocolPhase.finalChoose ProtocolPhase.finalPath old new)
:
FinalPathInvariant D input new depth count innerIndex selected (↑(protocolSourceRank D input)) 0
The final all-nonfinal scan starts the same bounded witness at the source vertex.
Extending a witness #
theorem
CertifiedRowSystem.Complement.pathStep_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 pathIndex fuel : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinv : CountingPathInvariant D input old depth oldCount newCount outerIndex innerIndex selected pathIndex fuel)
(hstep : IsPathStep D ProtocolPhase.path old new)
:
∃ (pathIndex' : ℕ),
CountingPathInvariant D input new depth oldCount newCount outerIndex innerIndex selected pathIndex' (fuel + 1)
One accepted ordinary path action advances fuel by one and preserves bounded reachability of the path rank.
theorem
CertifiedRowSystem.Complement.finalPathStep_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 innerIndex pathIndex fuel : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinv : FinalPathInvariant D input old depth count innerIndex selected pathIndex fuel)
(hstep : IsPathStep D ProtocolPhase.finalPath old new)
:
∃ (pathIndex' : ℕ), FinalPathInvariant D input new depth count innerIndex selected pathIndex' (fuel + 1)
One accepted final-scan path action has the same ranked reachability effect.
Completing a witness #
theorem
CertifiedRowSystem.Complement.finishWitness_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 pathIndex fuel : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : CountingPathInvariant D input old depth oldCount newCount outerIndex innerIndex selected pathIndex fuel)
(hstep : IsFinishWitness D old new)
:
innerIndex + 1 < Fintype.card A ^ input.length ∧ ChooseInnerInvariant D input new depth oldCount newCount outerIndex (innerIndex + 1)
(insert ⟨innerIndex, ⋯⟩ selected) ∨ innerIndex + 1 = Fintype.card A ^ input.length ∧ FinishOuterInvariant D input new depth oldCount newCount outerIndex (insert ⟨innerIndex, ⋯⟩ selected)
Completing an ordinary witness inserts the current inner rank into the selected transcript and advances the canonical inner enumeration.
theorem
CertifiedRowSystem.Complement.finalWitness_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 innerIndex pathIndex fuel : ℕ}
{selected : Finset (RankVertex A input.length)}
(hinput : input ≠ [])
(hinv : FinalPathInvariant D input old depth count innerIndex selected pathIndex fuel)
(hstep : IsFinalWitness D old new)
:
Completing a final-scan witness additionally records that the inserted reachable rank is nonfinal.