GapCVP proof, part 01, continuation 02

@[reducible, inline]

abbrev GapCVP.CLCompleteVerifierSimulation.PairedInputBlock (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.PairedInputBlock tm = (Fin (GapCVP.CLLocalWindows.blockSize tm) → GapCVP.CLCompleteVerifierSimulation.PairedInputTag)

@[reducible, inline]

abbrev GapCVP.CLCompleteVerifierSimulation.PhaseMaskBlock (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.PhaseMaskBlock tm = (Fin (GapCVP.CLLocalWindows.blockSize tm) → Bool)

def GapCVP.CLCompleteVerifierSimulation.pairedInputBlockAt (tm : Turing.FinTM2) (width : ℕ) (x certificate : List Bool) (position : Fin (width + 1)) : PairedInputBlock tm

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.phaseRangeBlockAt (tm : Turing.FinTM2) (width : ℕ) (position : Fin (width + 1)) : PhaseMaskBlock tm

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.phaseRangeBlockAt tm width position offset = decide (↑position * GapCVP.CLLocalWindows.blockSize tm + ↑offset < width + 1)

def GapCVP.CLCompleteVerifierSimulation.phaseBudgetBlockAt (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (position : Fin (CLCellRowBounds.rowWidth bound machine x + 1)) : PhaseMaskBlock machine.tm

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.initialPairedAtom {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (stack : machine.tm.K) (tag : PairedInputTag) : CLBoundedStates.CellAtom machine.tm

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CLCompleteVerifierSimulation.initialPairedAtom machine stack GapCVP.CLCompleteVerifierSimulation.PairedInputTag.marker = none
• GapCVP.CLCompleteVerifierSimulation.initialPairedAtom machine stack GapCVP.CLCompleteVerifierSimulation.PairedInputTag.blank = none

noncomputable def GapCVP.CLCompleteVerifierSimulation.initializedPhaseBlock {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (old : CLLocalWindows.BlockCell machine.tm) (payload : PairedInputBlock machine.tm) (range : PhaseMaskBlock machine.tm) : CLLocalWindows.BlockCell machine.tm

GapCVP reduction support.

Equations

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

structure GapCVP.CLCompleteVerifierSimulation.CompletePhaseCell (tm : Turing.FinTM2) : Type

GapCVP reduction support.

• mode : CLBoundedStates.PhaseTag

  GapCVP reduction support.

• script : CLTableauSimulationCert.ScriptBlockCell tm

  GapCVP reduction support.

• payload : PairedInputBlock tm

  GapCVP reduction support.

• payloadHead : PairedInputBlock tm

  GapCVP reduction support.

• range : PhaseMaskBlock tm

  GapCVP reduction support.

• rangeHead : PhaseMaskBlock tm

  GapCVP reduction support.

• budget : PhaseMaskBlock tm

  GapCVP reduction support.

• guessBit : Bool

  GapCVP reduction support.

@[instance_reducible]

noncomputable instance GapCVP.CLCompleteVerifierSimulation.instFintypeCompletePhaseCell (tm : Turing.FinTM2) : Fintype (CompletePhaseCell tm)

Equations

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

@[reducible, inline]

abbrev GapCVP.CLCompleteVerifierSimulation.CompletePhaseWindow (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.completeMachineBlock (tm : Turing.FinTM2) (cell : CompletePhaseCell tm) : CLLocalWindows.BlockCell tm

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.completeMachineBlock tm cell = cell.script.1.1

def GapCVP.CLCompleteVerifierSimulation.completeMachineHead (tm : Turing.FinTM2) (cell : CompletePhaseCell tm) : CLLocalWindows.BlockCell tm

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.completeMachineHead tm cell = cell.script.1.2

def GapCVP.CLCompleteVerifierSimulation.completeIsFirstBlock (tm : Turing.FinTM2) (cell : CompletePhaseCell tm) : Bool

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.completeIsFirstBlock tm cell = cell.script.2.2

def GapCVP.CLCompleteVerifierSimulation.lastPhaseOffset (tm : Turing.FinTM2) : Fin (CLLocalWindows.blockSize tm)

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.lastPhaseOffset tm = ⟨GapCVP.CLLocalWindows.blockSize tm - 1, ⋯⟩

def GapCVP.CLCompleteVerifierSimulation.phaseLeftOffset {α : Type} (tm : Turing.FinTM2) (first : Bool) (left center : Fin (CLLocalWindows.blockSize tm) → α) (offset : Fin (CLLocalWindows.blockSize tm)) : α

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.phaseRightOffset {α : Type} (tm : Turing.FinTM2) (center right : Fin (CLLocalWindows.blockSize tm) → α) (offset : Fin (CLLocalWindows.blockSize tm)) : α

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.phaseRightOffset tm center right offset = if hnext : ↑offset + 1 < GapCVP.CLLocalWindows.blockSize tm then center ⟨↑offset + 1, hnext⟩ else right ⟨0, ⋯⟩

def GapCVP.CLCompleteVerifierSimulation.completeWitnessWindow (tm : Turing.FinTM2) (window : CompletePhaseWindow tm) (offset : Fin (CLLocalWindows.blockSize tm)) : CLExactLocalRules.GuessPhaseWindow

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.completePayloadWindow (tm : Turing.FinTM2) (window : CompletePhaseWindow tm) (offset : Fin (CLLocalWindows.blockSize tm)) : PairedInputTag × PairedInputTag × PairedInputTag × PairedInputTag

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.PairedInputGuessAllowed (bit : Bool) (window : PairedInputTag × PairedInputTag × PairedInputTag × PairedInputTag) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.BroadcastWitnessGuessAllowed (bit : Bool) (window : CLExactLocalRules.GuessPhaseWindow) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.CompletePhaseCoherent (tm : Turing.FinTM2) (window : CompletePhaseWindow tm) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.completeScriptWindow (tm : Turing.FinTM2) (window : CompletePhaseWindow tm) : CLTableauSimulationCert.ScriptBlockWindow tm

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.completeScriptWindow tm window = (window.1.script, window.2.1.script, window.2.2.1.script, window.2.2.2.script)

noncomputable def GapCVP.CLCompleteVerifierSimulation.CompleteStaticTracksPreserved (tm : Turing.FinTM2) (window : CompletePhaseWindow tm) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.canonicalGuessingScriptRow {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (width : ℕ) (certificate : List Bool) (hint : CLExactVerifierTransition.FiniteVerifierHint machine.tm) : CLTableauSimulationCert.ScriptBlockRow machine.tm width

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.initialPhaseCell (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (x : List Bool) (position : Fin (CLCellRowBounds.rowWidth bound machine x + 1)) : CompletePhaseCell machine.tm

GapCVP reduction support.

Equations

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

def GapCVP.CLCompleteVerifierSimulation.acceptingPhaseCell (tm : Turing.FinTM2) : CompletePhaseCell tm

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.AcceptingPhaseBlock {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (cell : CompletePhaseCell machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.CompleteInitializationAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.CompleteVerificationAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.CompleteAcceptanceAllowed {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (window : CompletePhaseWindow machine.tm) : Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CLCompleteVerifierSimulation.completePhaseSymbolCount (tm : Turing.FinTM2) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.completePhaseSymbolCount tm = Fintype.card (GapCVP.CLCompleteVerifierSimulation.CompletePhaseCell tm) - 1

noncomputable def GapCVP.CLCompleteVerifierSimulation.completePhaseSymbolEquiv (tm : Turing.FinTM2) : CompletePhaseCell tm ≃ CL.Symbol (completePhaseSymbolCount tm)

GapCVP reduction support.

Equations

• GapCVP.CLCompleteVerifierSimulation.completePhaseSymbolEquiv tm = (Fintype.equivFin (GapCVP.CLCompleteVerifierSimulation.CompletePhaseCell tm)).trans (Equiv.cast ⋯)