Converse constructors for path-action specifications

PathActions.lean projects accepted componentwise scans to track equalities. The lemmas here prove the converse direction needed to build canonical accepting runs: the same track equations imply every cell-local check.

@[simp]

theorem CertifiedRowSystem.Complement.scanBits_start_replicate_of_pos (bit : Bool) {n : ℕ} (hn : 0 < n) : scanBits UniformScan.start (List.replicate n bit) = UniformScan.value bit

@[simp]

theorem CertifiedRowSystem.Complement.scanPhases_start_replicate_of_pos (phase : ProtocolPhase) {n : ℕ} (hn : 0 < n) : scanPhases UniformScan.start (List.replicate n phase) = UniformScan.value phase

theorem CertifiedRowSystem.Complement.startsPath_iff_tracks {A : Type u_2} [Fintype A] [Nonempty A] [DecidableEq A] (oldPhase newPhase : ProtocolPhase) (old new : ProtocolRow A) : StartsPath oldPhase newPhase old new ↔ List.length old = List.length new ∧ HasPhase oldPhase old ∧ HasPhase newPhase new ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ innerTrack new = innerTrack old ∧ pathTrack new = sourceTrack old ∧ fuelTrack new = (vertexCodec A).zeroRow (List.length new) ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old ∧ seenCountTrack new = seenCountTrack old ∧ foundTrack new = foundTrack old

Track equalities characterize the componentwise path-start action exactly.

theorem CertifiedRowSystem.Complement.isPathStep_of_tracks {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) (phase : ProtocolPhase) (old new : ProtocolRow A) (htracks : List.length old = List.length new ∧ HasPhase phase old ∧ HasPhase phase new ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ innerTrack new = innerTrack old ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old ∧ seenCountTrack new = seenCountTrack old ∧ foundTrack new = foundTrack old) (hfuel : (vertexCodec A).evalSucc RowNumeral.CarryState.carry (fuelTrack old) (fuelTrack new) = some RowNumeral.CarryState.done) (hbound : (vertexCodec A).compareRows (fuelTrack old) (depthTrack old) = some Ordering.lt) (hpath : pathTrack new = pathTrack old ∨ D.RowStep (pathTrack old) (pathTrack new)) : IsPathStep D phase old new

Persistent-track equations plus the three global numeral/path checks construct an accepted path-step action.

theorem CertifiedRowSystem.Complement.isFinishWitness_of_tracks {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) (old new : ProtocolRow A) (edgeState : Q) (innerState : RowNumeral.CarryState) (oldFound newFound : Bool) (newPhase : ProtocolPhase) (holdNe : old ≠ []) (htracks : List.length old = List.length new ∧ HasPhase ProtocolPhase.path old ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ pathTrack new = (vertexCodec A).zeroRow (List.length new) ∧ fuelTrack new = (vertexCodec A).zeroRow (List.length new) ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old) (hedge : D.evalStep D.stepStart (innerTrack old) (outerTrack old) (List.replicate (List.length old) ()) = some edgeState) (hpath : pathTrack old = innerTrack old) (hfuel : fuelTrack old = depthTrack old) (hseen : (countCodec A).evalSucc RowNumeral.CarryState.carry (seenCountTrack old) (seenCountTrack new) = some RowNumeral.CarryState.done) (hinner : (vertexCodec A).evalSucc RowNumeral.CarryState.carry (innerTrack old) (innerTrack new) = some innerState) (hphase : innerState = RowNumeral.CarryState.done ∧ newPhase = ProtocolPhase.chooseInner ∨ innerState = RowNumeral.CarryState.carry ∧ newPhase = ProtocolPhase.finishOuter) (holdFound : HasFound oldFound old) (hnewFound : HasFound newFound new) (hnewPhase : HasPhase newPhase new) (hfound : newFound = (oldFound || decide (innerTrack old = outerTrack old) || D.stepDone edgeState)) : IsFinishWitness D old new

Construct the exact ordinary witness-completion specification from its track, successor, uniformity, and source-verifier facts.

theorem CertifiedRowSystem.Complement.isFinalWitness_of_tracks {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) (old new : ProtocolRow A) (finalState : F) (innerState : RowNumeral.CarryState) (newPhase : ProtocolPhase) (holdNe : old ≠ []) (htracks : List.length old = List.length new ∧ HasPhase ProtocolPhase.finalPath old ∧ sourceTrack new = sourceTrack old ∧ depthTrack new = depthTrack old ∧ outerTrack new = outerTrack old ∧ pathTrack new = (vertexCodec A).zeroRow (List.length new) ∧ fuelTrack new = (vertexCodec A).zeroRow (List.length new) ∧ oldCountTrack new = oldCountTrack old ∧ newCountTrack new = newCountTrack old ∧ foundTrack new = foundTrack old) (hfinal : D.evalFinal D.finalStart (innerTrack old) = finalState) (hpath : pathTrack old = innerTrack old) (hfuel : fuelTrack old = depthTrack old) (hseen : (countCodec A).evalSucc RowNumeral.CarryState.carry (seenCountTrack old) (seenCountTrack new) = some RowNumeral.CarryState.done) (hinner : (vertexCodec A).evalSucc RowNumeral.CarryState.carry (innerTrack old) (innerTrack new) = some innerState) (hphase : innerState = RowNumeral.CarryState.done ∧ newPhase = ProtocolPhase.finalChoose ∨ innerState = RowNumeral.CarryState.carry ∧ newPhase = ProtocolPhase.finalFinish) (hnewPhase : HasPhase newPhase new) (hfinalDone : D.finalDone finalState = false) : IsFinalWitness D old new

Construct the exact final-scan witness-completion specification.