GapCVP proof, part 12, continuation 03

noncomputable def GapCVP.SourceOrder.sourceTypeCardWordOrder (formula : ThreeCNF) : Fin (Fintype.card (Core.sourceSATTableType (FormulaBridge.srcFormula formula))) ≃ Core.sourceSATTableType (FormulaBridge.srcFormula formula)

GapCVP reduction support.

Equations

• GapCVP.SourceOrder.sourceTypeCardWordOrder formula = (finCongr ⋯).trans (GapCVP.SourceOrder.sourceTypeWordOrder formula)

noncomputable def GapCVP.SourceOrder.sourceCoordinateWordOrder (encodingLength : ℕ) (formula : ThreeCNF) : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) ≃ Core.sourceSATTableCoordinate (FormulaBridge.srcFormula formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula)) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula))

GapCVP reduction support.

Equations

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

def GapCVP.SourceOrder.paperShiftedClauseTagCount (formula : ThreeCNF) (momentBudget : ℕ) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperShiftedClauseWordOrder (formula : ThreeCNF) (momentBudget : ℕ) (index : Fin (FormulaBridge.srcFormula formula).clauses.length) : Fin (paperShiftedClauseTagCount formula momentBudget index) ≃ (_ : ((FormulaBridge.srcFormula formula).clauses.get index).SatisfyingLocalTuple) × ((FormulaBridge.srcFormula formula).clauses.get index).LocalVariable × Fin (momentBudget + 1)

GapCVP reduction support.

Equations

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

def GapCVP.SourceOrder.paperShiftedFamilyTagCount (formula : ThreeCNF) (momentBudget : ℕ) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperShiftedFamilyWordOrder (formula : ThreeCNF) (momentBudget : ℕ) : Fin (paperShiftedFamilyTagCount formula momentBudget) ≃ (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) × (_ : ((FormulaBridge.srcFormula formula).clauses.get clause).SatisfyingLocalTuple) × ((FormulaBridge.srcFormula formula).clauses.get clause).LocalVariable × Fin (momentBudget + 1)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperOrdinaryFamilyWordOrder (formula : ThreeCNF) (momentBudget : ℕ) : Fin ((1 + paperVariableArityLocalTagCount formula) * (momentBudget + 1)) ≃ Core.sourceSATTableType (FormulaBridge.srcFormula formula) × Fin (momentBudget + 1)

GapCVP reduction support.

Equations

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

def GapCVP.SourceOrder.paperExplicitFamilyTagCount (encodingLength : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperExplicitFamilyWordOrder (encodingLength : ℕ) (formula : ThreeCNF) : Fin (paperExplicitFamilyTagCount encodingLength formula) ≃ BinaryExplicitAffineSystem.ExplicitConstraintFamily encodingLength (FormulaBridge.srcFormula formula)

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceOrder.paperExplicitBinaryRowDegree (encodingLength : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperExplicitBinaryFamilyBlockCount (encodingLength : ℕ) (formula : ThreeCNF) (index : Fin (paperExplicitFamilyTagCount encodingLength formula)) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperExplicitBinaryRowWordCount (encodingLength : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.paperVariableArityExplicitBinaryRowWordOrder (encodingLength : ℕ) (formula : ThreeCNF) : Fin (paperExplicitBinaryRowWordCount encodingLength formula) ≃ Core.assembledBinaryRow (BinaryExplicitAffineSystem.explicitFamilyRowCount encodingLength (FormulaBridge.srcFormula formula)) (paperExplicitBinaryRowDegree encodingLength formula)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceOrder.physicalBinarySystem (encodingLength : ℕ) (formula : ThreeCNF) : Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.PhysicalColumnOrder.physicalColumnPermutation (encodingLength : ℕ) (formula : ThreeCNF) : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) ≃ Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalColumnOrder.physicalCoordinateIndex (encodingLength : ℕ) (formula : ThreeCNF) (tableType : Core.sourceSATTableType (FormulaBridge.srcFormula formula)) (point : Core.sourceSATGridPoint (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula))) (value : Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula)) : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalColumnOrder.paperVariableArityPhysicalColumnPermutation_symm_sourceSATColumnIndex (encodingLength : ℕ) (formula : ThreeCNF) (tableType : Core.sourceSATTableType (FormulaBridge.srcFormula formula)) (point : Core.sourceSATGridPoint (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula))) (value : Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula)) : (physicalColumnPermutation encodingLength formula).symm (Core.sourceSATColumnIndex (FormulaBridge.srcFormula formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula)) tableType point value) = physicalCoordinateIndex encodingLength formula tableType point value

@[reducible, inline]

noncomputable abbrev GapCVP.PhysicalColumnOrder.physicalWordBinarySystem (encodingLength : ℕ) (formula : ThreeCNF) : Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalColumnOrder.paperVariableArityPhysicalWordBinarySystem_rowCount (encodingLength : ℕ) (formula : ThreeCNF) : (physicalWordBinarySystem encodingLength formula).rowCount = SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula

theorem GapCVP.PhysicalColumnOrder.paperVariableArityPhysicalWordBinarySystem_check_apply (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) (column : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))) : (physicalWordBinarySystem encodingLength formula).check row column = (SourceOrder.physicalBinarySystem encodingLength formula).check row ((physicalColumnPermutation encodingLength formula) column)

theorem GapCVP.PhysicalWordSoundness.paperVariableArityPhysicalWordBinarySystem_oneHot_of_satisfiable (encodingLength : ℕ) (formula : ThreeCNF) (hsatisfiable : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) : ∃ (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ), (PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula).Solves vector = true ∧ (∀ (index : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))), vector index = 0 ∨ vector index = 1) ∧ Core.integerSquaredNorm vector = FourFamilySoundness.paperVariableArityIntegerRadius encodingLength formula

theorem GapCVP.PhysicalWordSoundness.paperVariableArityPhysicalWordBinarySystem_satisfiable_of_scaled_hamming (encodingLength : ℕ) (formula : ThreeCNF) (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (hsolve : (PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula).Solves vector = true) (hshort : ↑(Core.integerSquaredNorm vector) ≤ 2 * Factor400BinaryCodeDecodingCorollary.binaryCodeGapFactor (PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula).dimension * ↑(FourFamilySoundness.paperVariableArityIntegerRadius encodingLength formula)) : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true

theorem GapCVP.PhysicalWordSoundness.paperVariableArityPhysicalWordBinarySystem_strict_factor400_of_unsatisfiable (encodingLength : ℕ) (formula : ThreeCNF) (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ) (hsolve : (PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula).Solves vector = true) (hunsatisfiable : ¬∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) : (SourceFactor400BinaryConstructionABounds.gapFactor400 (PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula).dimension * ↑(Core.sourceOneHotCompletenessRadius (FormulaBridge.srcFormula formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (FormulaBridge.srcFormula formula)))) ^ 2 < ↑(Core.integerSquaredNorm vector)

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (encodingLength : ℕ) (formula : ThreeCNF) : Core.BinaryAffineSystem

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem encodingLength formula = GapCVP.PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula

@[simp]

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalFormulaSystem_dimension (encodingLength : ℕ) (formula : ThreeCNF) : (physicalFormulaSystem encodingLength formula).dimension = Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem_dimension_pos (encodingLength : ℕ) (formula : ThreeCNF) : 0 < (physicalFormulaSystem encodingLength formula).dimension

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaRadius (encodingLength : ℕ) (formula : ThreeCNF) : ℚ

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaRadius_pos (encodingLength : ℕ) (formula : ThreeCNF) : 0 < physicalFormulaRadius encodingLength formula

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaInstance (encodingLength : ℕ) (formula : ThreeCNF) : GapCVPInstance

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalFormulaSystem_oneHot_of_satisfiable (encodingLength : ℕ) (formula : ThreeCNF) (satisfiable : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) : ∃ (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula)) → ℤ), (physicalFormulaSystem encodingLength formula).Solves vector = true ∧ (∀ (index : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (FormulaBridge.srcFormula formula))), vector index = 0 ∨ vector index = 1) ∧ Core.integerSquaredNorm vector = FourFamilySoundness.paperVariableArityIntegerRadius encodingLength formula

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem_consistent_of_satisfiable (encodingLength : ℕ) (formula : ThreeCNF) (satisfiable : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) : (physicalFormulaSystem encodingLength formula).effectiveReducedConsistent = true

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityOriginal_satisfiable_of_normalized_empty (formula : ThreeCNF) (empty : SourcePreprocessingSemantics.paperSourceNormalizedClauses formula = []) : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalSourceInstance (input : List Bool) : GapCVPInstance

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceMap (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceInstance_of_decode_none (input : List Bool) (decode : BinaryEncoding.decodeThreeCNF input = none) : physicalSourceInstance input = Factor400BinaryCanonicalNo.adaptedCanonicalNoInstance

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceInstance_of_noncanonical (input : List Bool) (formula : ThreeCNF) (decode : BinaryEncoding.decodeThreeCNF input = some formula) (noncanonical : BinaryEncoding.encodeThreeCNF formula ≠ input) : physicalSourceInstance input = Factor400BinaryCanonicalNo.adaptedCanonicalNoInstance

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceInstance_of_normalized_empty (input : List Bool) (formula : ThreeCNF) (decode : BinaryEncoding.decodeThreeCNF input = some formula) (canonical : BinaryEncoding.encodeThreeCNF formula = input) (empty : SourcePreprocessingSemantics.paperSourceNormalizedClauses formula = []) : physicalSourceInstance input = SourceMachineRouting.canonicalYesInstance

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceInstance_of_inconsistent (input : List Bool) (formula : ThreeCNF) (decode : BinaryEncoding.decodeThreeCNF input = some formula) (canonical : BinaryEncoding.encodeThreeCNF formula = input) (nonempty : SourcePreprocessingSemantics.paperSourceNormalizedClauses formula ≠ []) (inconsistent : (physicalFormulaSystem input.length formula).effectiveReducedConsistent = false) : physicalSourceInstance input = Factor400BinaryCanonicalNo.adaptedCanonicalNoInstance

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceInstance_of_consistent (input : List Bool) (formula : ThreeCNF) (decode : BinaryEncoding.decodeThreeCNF input = some formula) (canonical : BinaryEncoding.encodeThreeCNF formula = input) (nonempty : SourcePreprocessingSemantics.paperSourceNormalizedClauses formula ≠ []) (consistent : (physicalFormulaSystem input.length formula).effectiveReducedConsistent = true) : physicalSourceInstance input = physicalFormulaInstance input.length formula

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceReductionOfMachine (machine : BitTM paperVariableArityPhysicalSourceMap) : PromiseReduction OriginalThreeSATNPHardness.paperOriginalThreeSATLanguage gapCVP400Promise

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceReductionOfMachine_map (machine : BitTM paperVariableArityPhysicalSourceMap) (input : List Bool) : (paperVariableArityPhysicalSourceReductionOfMachine machine).map input = paperVariableArityPhysicalSourceMap input

The reduction built from a machine uses the physical source map.

def GapCVP.ClauseOffsetTM.paperVariableArityClauseArityUnary (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ClauseOffsetTM.paperClauseArityUnaryComputable : BitTM paperVariableArityClauseArityUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.ClauseOffsetTM.paperVariableArityClauseArityUnary_valid (clause : ThreeClause) (suffix : List Bool) : paperVariableArityClauseArityUnary (BinaryEncoding.encodeThreeClause clause ++ suffix) = List.replicate (SourcePreprocessingSemantics.paperSourceNormalizedClause clause).length true

def GapCVP.ClauseOffsetTM.paperVariableArityClauseWeightUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ClauseOffsetTM.paperClauseWeightUnaryComputable : BitTM paperVariableArityClauseWeightUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.ClauseOffsetTM.paperVariableArityClauseWeightUnary_valid (clause : ThreeClause) (suffix : List Bool) : paperVariableArityClauseWeightUnary (BinaryEncoding.encodeThreeClause clause ++ suffix) = List.replicate (2 ^ (SourcePreprocessingSemantics.paperSourceNormalizedClause clause).length - 1) true

def GapCVP.ClauseOffsetTM.sourceClauseWeight (clause : ThreeClause) : ℕ

GapCVP reduction support.

Equations

• GapCVP.ClauseOffsetTM.sourceClauseWeight clause = 2 ^ (GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClause clause).length - 1

def GapCVP.ClauseOffsetTM.sourceClauseWeightSum (clauses : List ThreeClause) : ℕ

GapCVP reduction support.

Equations

• GapCVP.ClauseOffsetTM.sourceClauseWeightSum clauses = (List.map GapCVP.ClauseOffsetTM.sourceClauseWeight clauses).sum

def GapCVP.ClauseOffsetTM.sourceClauseOffsetCatalogue : ℕ → List ThreeClause → List Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.ClauseOffsetTM.sourceClauseOffsetCatalogue x✝ [] = []

def GapCVP.ClauseOffsetTM.paperRetainedClauseCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.ClauseOffsetTM.paperRetainedClauseCountUnary = GapCVP.SourcePreprocessingTM.paperSourcePreprocessingFinalField 2

noncomputable def GapCVP.ClauseOffsetTM.paperVariableArityRetainedClauseCountUnaryComputable : BitTM paperRetainedClauseCountUnary

GapCVP reduction support.

Equations

• GapCVP.ClauseOffsetTM.paperVariableArityRetainedClauseCountUnaryComputable = GapCVP.SourcePreprocessingTM.paperPreprocessingFinalFieldComputable 2

@[simp]

theorem GapCVP.ClauseOffsetTM.paperVariableArityRetainedClauseCountUnary_valid (formula : ThreeCNF) : paperRetainedClauseCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) true

def GapCVP.ClauseOffsetTM.paperClauseOffsetOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ClauseOffsetTM.paperVariableArityClauseOffsetOutputComputable : BitTM paperClauseOffsetOutput

GapCVP reduction support.

Equations

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

theorem GapCVP.ClauseOffsetTM.paperVariableArityClauseOffsetOutput_valid (formula : ThreeCNF) : paperClauseOffsetOutput (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.lengthPrefixedWord (sourceClauseOffsetCatalogue 0 (BinarySourceTautologyNormalizationExact.noTautClauses formula)) ++ (BinaryEncoding.lengthPrefixedWord (List.replicate (sourceClauseWeightSum (BinarySourceTautologyNormalizationExact.noTautClauses formula)) true) ++ SourcePreprocessingTM.paperSourcePreprocessingOutput (BinaryEncoding.encodeThreeCNF formula))

theorem GapCVP.BinaryPhysicalWordQueryCatalogueTM.sourcePhysicalWordCanonical_range_mul_flatMap (rows columns : ℕ) : List.range (rows * columns) = List.flatMap (fun (row : ℕ) => List.map (fun (column : ℕ) => row * columns + column) (List.range columns)) (List.range rows)

structure GapCVP.CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape : Type 1

GapCVP reduction support.

• system (encodingLength : ℕ) : ThreeCNF → Core.BinaryAffineSystem

  GapCVP reduction support.

• systemCorrect (encodingLength : ℕ) (formula : ThreeCNF) : self.system encodingLength formula = PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula
• rows : List Bool → List Bool

  GapCVP reduction support.

• columns : List Bool → List Bool

  GapCVP reduction support.

• rowsComputable : BitTM self.rows

  GapCVP reduction support.

• columnsComputable : BitTM self.columns

  GapCVP reduction support.

• rowsCorrect (formula : ThreeCNF) : self.rows (BinaryEncoding.encodeThreeCNF formula) = List.replicate (self.system (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount true
• columnsCorrect (formula : ThreeCNF) : self.columns (BinaryEncoding.encodeThreeCNF formula) = List.replicate (self.system (BinaryEncoding.encodeThreeCNF formula).length formula).dimension true
• columnsPositive (formula : ThreeCNF) : 0 < (self.system (BinaryEncoding.encodeThreeCNF formula).length formula).dimension

structure GapCVP.CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer (shape : PaperVariableArityCanonicalBinaryMatrixShape) : Type 1

GapCVP reduction support.

• check : List Bool → List Bool

  GapCVP reduction support.

• rhs : List Bool → List Bool

  GapCVP reduction support.

• checkComputable : BitTM self.check

  GapCVP reduction support.

• rhsComputable : BitTM self.rhs

  GapCVP reduction support.

• checkCorrect (formula : ThreeCNF) (row : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount) (column : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) : self.check (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]
• rhsCorrect (formula : ThreeCNF) (row : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount) (column : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) : self.rhs (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).rightHandSide row = 1)]

def GapCVP.CanonicalMatrixShape.paperVariableArityCanonicalBinaryMatrixRawCheckWidth (shape : PaperVariableArityCanonicalBinaryMatrixShape) : List Bool → List Bool

Compute the raw check grid width from the matrix row and column dimensions.

Equations

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

noncomputable def GapCVP.CanonicalMatrixShape.paperVariableArityCanonicalBinaryMatrixRawCheckWidthComputable (shape : PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperVariableArityCanonicalBinaryMatrixRawCheckWidth shape)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRankDimension (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : List Bool → List Bool

Read the canonical matrix column dimension from a rank query.

Equations

• GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRankDimension shape = shape.columns ∘ GapCVP.BinaryPhysicalWordQueryCatalogueTM.sourcePhysicalWordCatalogueRankOriginalSource✝

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRankDimensionComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperVariableArityCanonicalBinaryMatrixRankDimension shape)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRankDivisionInput (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (input : List Bool) : List Bool

Combine a catalogue rank, column dimension, and source for row-major division.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRankDivisionInputComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperCanonicalBinaryMatrixRankDivisionInput shape)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRankDivisionOutput (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : List Bool → List Bool

Decode a catalogue rank into its row-major matrix coordinates.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRankDivisionOutputComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperCanonicalBinaryMatrixRankDivisionOutput shape)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckCandidate (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (input : List Bool) : List Bool

Encode one candidate query for a canonical matrix check bit.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckCandidateComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperVariableArityCanonicalBinaryMatrixCheckCandidate shape)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckQueryCatalogue (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : List Bool → List Bool

Enumerate candidate queries for canonical matrix check bits.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckQueryCatalogueComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperVariableArityCanonicalBinaryMatrixCheckQueryCatalogue shape)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsQueryCatalogue (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : List Bool → List Bool

Enumerate candidate queries for canonical matrix right-hand-side bits.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsQueryCatalogueComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperVariableArityCanonicalBinaryMatrixRhsQueryCatalogue shape)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixCheckQueries (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) : List (List Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRhsQueries (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) : List (List Bool)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixCheckFoldPreparation (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckFoldPreparationComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperCanonicalBinaryMatrixCheckFoldPreparation shape)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRhsFoldPreparation (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsFoldPreparationComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperCanonicalBinaryMatrixRhsFoldPreparation shape)

GapCVP reduction support.

Equations

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

theorem GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckFoldPreparation_valid (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) : paperCanonicalBinaryMatrixCheckFoldPreparation shape (BinaryEncoding.encodeThreeCNF formula) = BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedQueryPreparation (paperCanonicalBinaryMatrixCheckQueries shape formula) (BinaryEncoding.encodeThreeCNF formula)

theorem GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsFoldPreparation_valid (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) : paperCanonicalBinaryMatrixRhsFoldPreparation shape (BinaryEncoding.encodeThreeCNF formula) = BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedQueryPreparation (paperCanonicalBinaryMatrixRhsQueries shape formula) (BinaryEncoding.encodeThreeCNF formula)

def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixCheckMarker {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixCheckMarker worker = GapCVP.GaussianRowWorker.binaryGaussianFirstCellWord ∘ worker.check

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckMarkerComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperCanonicalBinaryMatrixCheckMarker worker)

GapCVP reduction support.

Equations

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

def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRhsMarker {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRhsMarker worker = GapCVP.GaussianRowWorker.binaryGaussianFirstCellWord ∘ worker.rhs

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsMarkerComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperCanonicalBinaryMatrixRhsMarker worker)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixCheckFold {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : List Bool → List Bool

Fold the canonical matrix check-bit catalogue with the cell worker.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckFoldComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperCanonicalBinaryMatrixCheckFold worker)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixRhsFold {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : List Bool → List Bool

Fold the canonical matrix right-hand-side catalogue with the cell worker.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsFoldComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperCanonicalBinaryMatrixRhsFold worker)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperCanonicalBinaryMatrixPackedOutput {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixPackedComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperCanonicalBinaryMatrixPackedOutput worker)

GapCVP reduction support.

Equations

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

theorem GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixCheckMarker_valid {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (formula : ThreeCNF) (row : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount) (column : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) : paperCanonicalBinaryMatrixCheckMarker worker (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).check row column = 1)]

theorem GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixRhsMarker_valid {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (formula : ThreeCNF) (row : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount) (column : Fin (shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) : paperCanonicalBinaryMatrixRhsMarker worker (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((shape.system (BinaryEncoding.encodeThreeCNF formula).length formula).rightHandSide row = 1)]

theorem GapCVP.CanonicalSourceCatalogue.paperVariableArityCanonicalBinaryMatrixPackedOutput_valid {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (formula : ThreeCNF) : paperCanonicalBinaryMatrixPackedOutput worker (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.lengthPrefixedWord (BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedCheckBits (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula)) ++ BinaryEncoding.lengthPrefixedWord (BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedRhsBits (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula)) ++ BinaryEncoding.encodeThreeCNF formula

def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery (column : ℕ) (state : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery column state = GapCVP.BinaryEncoding.lengthPrefixedWord (List.replicate column true) ++ state

def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordWord (row width column : ℕ) (state : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordRow : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordRow = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordRowComputable : BitTM gaussianPhysicalPivotRecordRow

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordRowComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordColumn : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordColumnComputable : BitTM gaussianPhysicalPivotRecordColumn

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordState : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordStateComputable : BitTM gaussianPhysicalPivotRecordState

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordNextUnary : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordNextUnaryComputable : BitTM gaussianPhysicalPivotRecordNextUnary

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordRow_word (row width column : ℕ) (state : List Bool) : gaussianPhysicalPivotRecordRow (gaussianPhysicalPivotRecordWord row width column state) = List.replicate row true

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordColumn_word (row width column : ℕ) (state : List Bool) : gaussianPhysicalPivotRecordColumn (gaussianPhysicalPivotRecordWord row width column state) = List.replicate column true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordState_word (row width column : ℕ) (state : List Bool) : gaussianPhysicalPivotRecordState (gaussianPhysicalPivotRecordWord row width column state) = state

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotRecordNextUnary_word {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row width column : ℕ) : gaussianPhysicalPivotRecordNextUnary (gaussianPhysicalPivotRecordWord row width column (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = List.replicate state.nextPivot true

Internal support shared across GapCVP continuation modules.

theorem GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivot_range_flatMap_finRange {α : Type} (count : ℕ) (record : ℕ → List α) : List.flatMap record (List.range count) = List.flatMap (fun (index : Fin count) => record ↑index) (List.finRange count)

noncomputable def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotDecisionOutput : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotDecisionComputable : BitTM gaussianPhysicalPivotDecisionOutput

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotDecisionOutput_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (column : Fin n) (hrows : 0 < m) : gaussianPhysicalPivotDecisionOutput (gaussianPhysicalPivotColumnQuery (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = match Core.EffectiveBinaryGaussian.findPivotOption state column with | none => [false] | some row => true :: List.replicate (↑row) true

Internal support shared across GapCVP continuation modules.

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateSemantics.clearTargets_check_finRange {m n : ℕ} (pivot : Fin m) (active other : Fin n) (state : Core.EffectiveBinaryGaussian.State m n) (row : Fin m) : (Core.EffectiveBinaryGaussian.clearTargets pivot active (List.finRange m) state).system.check row other = if row ≠ pivot ∧ state.system.check row active = 1 then state.system.check row other + state.system.check pivot other else state.system.check row other

Internal support shared across GapCVP continuation modules.

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateSemantics.clearTargets_rhs_finRange {m n : ℕ} (pivot : Fin m) (active : Fin n) (state : Core.EffectiveBinaryGaussian.State m n) (row : Fin m) : (Core.EffectiveBinaryGaussian.clearTargets pivot active (List.finRange m) state).system.rhs row = if row ≠ pivot ∧ state.system.check row active = 1 then state.system.rhs row + state.system.rhs pivot else state.system.rhs row

Internal support shared across GapCVP continuation modules.

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellQuery (row column active : ℕ) (state : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellRow : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellRow = GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellRow

@[reducible, inline]

abbrev GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellColumn : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellColumn = GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellColumn

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellActive : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellActiveComputable : BitTM gaussianPhysicalColumnCellActive

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellPackedState : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellRow_query (row column active : ℕ) (state : List Bool) : gaussianPhysicalColumnCellRow (gaussianPhysicalColumnCellQuery row column active state) = List.replicate row true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellColumn_query (row column active : ℕ) (state : List Bool) : gaussianPhysicalColumnCellColumn (gaussianPhysicalColumnCellQuery row column active state) = List.replicate column true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellActive_query (row column active : ℕ) (state : List Bool) : gaussianPhysicalColumnCellActive (gaussianPhysicalColumnCellQuery row column active state) = List.replicate active true

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCellPackedState_query (row column active : ℕ) (state : List Bool) : gaussianPhysicalColumnCellPackedState (gaussianPhysicalColumnCellQuery row column active state) = state

Internal support shared across GapCVP continuation modules.

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDecisionQuery (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDecisionQuery_query (row column active : ℕ) (state : List Bool) : gaussianPhysicalColumnDecisionQuery (gaussianPhysicalColumnCellQuery row column active state) = GaussianAdaptivePhysicalCandidateCatalogueTM.gaussianPhysicalPivotColumnQuery active state

Internal support shared across GapCVP continuation modules.

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

Internal support shared across GapCVP continuation modules.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnPivotPresentComputable : BitTM gaussianPhysicalColumnPivotPresentWord

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnPivotSelectionComputable : BitTM fun (input : List Bool) => gaussianPhysicalColumnPivotPresent input :: input

Internal support shared across GapCVP continuation modules.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCandidateUnary = List.tail ∘ GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDecisionWord

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnCandidateUnaryComputable : BitTM gaussianPhysicalColumnCandidateUnary

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnNextPivotUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnNextPivotUnaryComputable : BitTM gaussianPhysicalColumnNextPivotUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnNextPivotUnary_query {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row column active : ℕ) : gaussianPhysicalColumnNextPivotUnary (gaussianPhysicalColumnCellQuery row column active (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = List.replicate state.nextPivot true

Internal support shared across GapCVP continuation modules.

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDynamicCheckWord (row column : List Bool → List Bool) : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDynamicCheckComputable {row column : List Bool → List Bool} (hrow : BitTM row) (hcolumn : BitTM column) : BitTM (gaussianPhysicalColumnDynamicCheckWord row column)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDynamicRhsWord (row column : List Bool → List Bool) : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDynamicRhsComputable {row column : List Bool → List Bool} (hrow : BitTM row) (hcolumn : BitTM column) : BitTM (gaussianPhysicalColumnDynamicRhsWord row column)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDynamicCheckWord_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source input : List Bool) (rowWorker columnWorker : List Bool → List Bool) (row : Fin m) (column : Fin n) (hstate : gaussianPhysicalColumnCellPackedState input = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source) (hrow : rowWorker input = List.replicate (↑row) true) (hcolumn : columnWorker input = List.replicate (↑column) true) : gaussianPhysicalColumnDynamicCheckWord rowWorker columnWorker input = [decide (state.system.check row column = 1)]

Internal support shared across GapCVP continuation modules.

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnDynamicRhsWord_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source input : List Bool) (rowWorker columnWorker : List Bool → List Bool) (row : Fin m) (column : Fin n) (hstate : gaussianPhysicalColumnCellPackedState input = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source) (hrow : rowWorker input = List.replicate (↑row) true) (hcolumn : columnWorker input = List.replicate (↑column) true) : gaussianPhysicalColumnDynamicRhsWord rowWorker columnWorker input = [decide (state.system.rhs row = 1)]

Internal support shared across GapCVP continuation modules.

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

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnRowIsPivotWord : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnRowIsPivotComputable : BitTM gaussianPhysicalColumnRowIsPivotWord

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnSwappedBitWord (original pivot candidate : List Bool → List Bool) : List Bool → List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnSwappedBitComputable {original pivot candidate : List Bool → List Bool} (horiginal : BitTM original) (hpivot : BitTM pivot) (hcandidate : BitTM candidate) : BitTM (gaussianPhysicalColumnSwappedBitWord original pivot candidate)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.GaussianAdaptivePhysicalColumnCellUpdateTM.gaussianPhysicalColumnSwappedBitWord_bits (original pivot candidate : List Bool → List Bool) (input : List Bool) (rowIsCandidate rowIsPivot originalBit pivotBit candidateBit : Bool) (hcandidateDecision : gaussianPhysicalColumnRowIsCandidateWord input = [rowIsCandidate]) (hpivotDecision : gaussianPhysicalColumnRowIsPivotWord input = [rowIsPivot]) (horiginal : original input = [originalBit]) (hpivot : pivot input = [pivotBit]) (hcandidate : candidate input = [candidateBit]) : gaussianPhysicalColumnSwappedBitWord original pivot candidate input = [rowIsCandidate && pivotBit || (rowIsPivot && candidateBit || !rowIsCandidate && !rowIsPivot && originalBit)]

Internal support shared across GapCVP continuation modules.