GapCVP proof, part 12, continuation 04

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnUpdatedCheckWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnUpdatedCheckComputable : BitTM gaussianPhysicalColumnUpdatedCheckWord

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnUpdatedRhsWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnUpdatedRhsComputable : BitTM gaussianPhysicalColumnUpdatedRhsWord

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnPivotPresent_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row : Fin m) (column active : Fin n) : gaussianPhysicalColumnPivotPresent (gaussianPhysicalColumnCellQuery (↑row) (↑column) (↑active) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = (Core.EffectiveBinaryGaussian.findPivotOption state active).isSome

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnUpdatedCheckWord_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row : Fin m) (column active : Fin n) : gaussianPhysicalColumnUpdatedCheckWord (gaussianPhysicalColumnCellQuery (↑row) (↑column) (↑active) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = [decide ((Core.EffectiveBinaryGaussian.columnStep state active).system.check row column = 1)]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnUpdatedRhsWord_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row : Fin m) (column active : Fin n) : gaussianPhysicalColumnUpdatedRhsWord (gaussianPhysicalColumnCellQuery (↑row) (↑column) (↑active) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = [decide ((Core.EffectiveBinaryGaussian.columnStep state active).system.rhs row = 1)]

def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnActiveUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnActiveUnary = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnActiveUnaryComputable : BitTM gaussianPhysicalColumnActiveUnary

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnActiveUnaryComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnCurrentState : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnCurrentState = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnCurrentStateComputable : BitTM gaussianPhysicalColumnCurrentState

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnCurrentStateComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffixComputable

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotPresent (input : List Bool) : Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotPresent input = (GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotDecisionOutput input).headD false

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotPresentComputable : BitTM fun (input : List Bool) => gaussianPhysicalColumnPivotPresent input :: input

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnNextPivotUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnNextPivotUnaryComputable : BitTM gaussianPhysicalColumnNextPivotUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnActiveUnary_query (column : ℕ) (state : List Bool) : gaussianPhysicalColumnActiveUnary (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery column state) = List.replicate column true

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnCurrentState_query (column : ℕ) (state : List Bool) : gaussianPhysicalColumnCurrentState (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery column state) = state

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotPresent_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (column : Fin n) (hrows : 0 < m) : gaussianPhysicalColumnPivotPresent (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = (Core.EffectiveBinaryGaussian.findPivotOption state column).isSome

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnNextPivotUnary_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (column : Fin n) (hrows : 0 < m) : gaussianPhysicalColumnNextPivotUnary (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = List.replicate (Core.EffectiveBinaryGaussian.columnStep state column).nextPivot true

def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotRecordOuter : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotRecordOuter = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotRecordOuterComputable : BitTM gaussianPhysicalColumnPivotRecordOuter

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotRecordOuter_word (rank width active : ℕ) (state : List Bool) : gaussianPhysicalColumnPivotRecordOuter (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordWord rank width active state) = GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery active state

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalComputedMarkerPreservingComputable {marker : List Bool → List Bool} (computer : BitTM marker) : BitTM fun (input : List Bool) => (marker input).headD false :: input

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotWidthOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotWidthComputable : BitTM gaussianPhysicalColumnPivotWidthOutput

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnUpdatedPivotCatalogueOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnUpdatedPivotCatalogueComputable : BitTM gaussianPhysicalColumnUpdatedPivotCatalogueOutput

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotWidth_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (active : Fin n) (hrows : 0 < m) : GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnPivotWidth✝.output (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery (↑active) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = List.replicate n true

theorem GapCVP.GaussianAdaptivePhysicalColumnStateTM.gaussianPhysicalColumnUpdatedPivotCatalogueOutput_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (active : Fin n) (hrows : 0 < m) : gaussianPhysicalColumnUpdatedPivotCatalogueOutput (GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery (↑active) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedPivotCatalogue (Core.EffectiveBinaryGaussian.columnStep state active)