GapCVP proof, part 13

def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationBudgetWord (packed : List Bool) : List Bool

Encode the column iteration budget as a unary word.

Equations

• GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationBudgetWord packed = List.replicate (64 * (packed.length + 1) ^ 2) true

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationBudgetWordComputable : BitTM gaussianPhysicalColumnIterationBudgetWord

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationActiveUnary : List Bool → List Bool

Extract the active column index in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationActiveUnaryComputable : BitTM gaussianPhysicalColumnIterationActiveUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationCandidate (input : List Bool) : List Bool

Extract the candidate pivot column from the iteration state.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationCandidateComputable : BitTM gaussianPhysicalColumnIterationCandidate

GapCVP reduction support.

def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationBudgetLengthUnary : List Bool → List Bool

Encode the archived column budget length in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationBudgetLengthUnaryComputable : BitTM gaussianPhysicalColumnIterationBudgetLengthUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationCandidateLengthUnary : List Bool → List Bool

Encode the candidate column length in unary form.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationCandidateLengthUnaryComputable : BitTM gaussianPhysicalColumnIterationCandidateLengthUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationOverflowMarker : List Bool → List Bool

Mark whether the column iteration exceeds its budget.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationOverflowMarkerComputable : BitTM gaussianPhysicalColumnIterationOverflowMarker

GapCVP reduction support.

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationAcceptMarker : List Bool → List Bool

Mark whether the current pivot candidate is accepted.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationAcceptMarkerComputable : BitTM gaussianPhysicalColumnIterationAcceptMarker

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationAccepted (input : List Bool) : Bool

Select the accepted column iteration state.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationAcceptedComputable : BitTM fun (input : List Bool) => gaussianPhysicalColumnIterationAccepted input :: input

GapCVP reduction support.

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationAcceptedOutput (input : List Bool) : List Bool

Produce the output of an accepted column iteration.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationAcceptedOutputComputable : BitTM gaussianPhysicalColumnIterationAcceptedOutput

GapCVP reduction support.

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationStep : List Bool → List Bool

Advance the physical Gaussian column iteration by one candidate.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationStepComputable : BitTM gaussianPhysicalColumnIterationStep

GapCVP reduction support.

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationFoldComputable : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput gaussianPhysicalColumnIterationStep)

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationSeed (packed : List Bool) : List Bool

Initialize the physical Gaussian column iteration state.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationSeedComputable : BitTM gaussianPhysicalColumnIterationSeed

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationPreparation (packed : List Bool) : List Bool

Prepare the packed state for physical column iteration.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationPreparationComputable : BitTM gaussianPhysicalColumnIterationPreparation

GapCVP reduction support.

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationOutput : List Bool → List Bool

Compute the final physical column iteration output.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalColumnIterationComputable : BitTM gaussianPhysicalColumnIterationOutput

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalSourceEliminationOutput : List Bool → List Bool

Compute the physical Gaussian source elimination output.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianAdaptivePhysicalColumnIterationBoundTM.gaussianPhysicalSourceEliminationComputable : BitTM gaussianPhysicalSourceEliminationOutput

GapCVP reduction support.

Equations

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

structure GapCVP.GaussianSourceInitializer.PaperVariableArityPhysicalPackedMatrixSourceComputer : Type 1

A computer for a packed matrix derived from a variable-arity source.

• output : List Bool → List Bool

  The serialized matrix produced from an encoded source formula.

• computer : BitTM self.output

  A polynomial-time machine computing the serialized matrix.

• output_valid (formula : ThreeCNF) : self.output (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

noncomputable def GapCVP.GaussianSourceReducedConsistency.gaussianPaperVariableAritySourceReducedConsistencyQueryOutput (matrix : GaussianSourceInitializer.PaperVariableArityPhysicalPackedMatrixSourceComputer) : List Bool → List Bool

Form the reduced-consistency query from a variable-arity source matrix.

Equations

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

noncomputable def GapCVP.GaussianSourceReducedConsistency.gaussianPaperVariableAritySourceReducedConsistencyQueryComputable (matrix : GaussianSourceInitializer.PaperVariableArityPhysicalPackedMatrixSourceComputer) : BitTM (gaussianPaperVariableAritySourceReducedConsistencyQueryOutput matrix)

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianSourceInitializerInstantiation.paperVariableArityCanonicalPhysicalPackedMatrixSourceComputer {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : GaussianSourceInitializer.PaperVariableArityPhysicalPackedMatrixSourceComputer

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianSourceInitializerInstantiation.gaussianPaperVariableArityCanonicalSourceReducedStateComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (gaussianPaperVariableArityCanonicalSourceReducedStateOutput worker)

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianSourceInitializerInstantiation.gaussianPaperVariableArityCanonicalSourceReducedStateOutput_effective {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (formula : ThreeCNF) : gaussianPaperVariableArityCanonicalSourceReducedStateOutput worker (BinaryEncoding.encodeThreeCNF formula) = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveGaussianState (BinaryEncoding.encodeThreeCNF formula)

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

Form the canonical source's reduced-consistency query.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianSourceInitializerInstantiation.gaussianPaperVariableArityCanonicalSourceReducedConsistencyQueryComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (gaussianPaperVariableArityCanonicalSourceReducedConsistencyQueryOutput worker)

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianSourceInitializerInstantiation.gaussianPaperVariableArityCanonicalSourceReducedConsistencyQueryOutput_valid {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (formula : ThreeCNF) : gaussianPaperVariableArityCanonicalSourceReducedConsistencyQueryOutput worker (BinaryEncoding.encodeThreeCNF formula) = GaussianReducedConsistencyTM.effectiveGaussianReducedConsistencyQuery (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula) (BinaryEncoding.encodeThreeCNF formula)

noncomputable def GapCVP.GaussianOutputSerializerTM.paperGaussianSourceDimensionWidth (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

• GapCVP.GaussianOutputSerializerTM.paperGaussianSourceDimensionWidth shape = { output := shape.columns, computer := shape.columnsComputable }

theorem GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianSourceDimensionWidth_valid (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) : (paperGaussianSourceDimensionWidth shape).output (BinaryEncoding.encodeThreeCNF formula) = List.replicate (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension true

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

GapCVP reduction support.

Equations

• GapCVP.GaussianOutputSerializerTM.paperGaussianRankDimensionUnary shape = shape.columns ∘ GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSource

theorem GapCVP.GaussianOutputSerializerTM.paperGaussianRankDimensionUnary_query (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) (rank : ℕ) : paperGaussianRankDimensionUnary shape (BinaryStructuralRecordTM.constructiveStructuralRankQuery (paperGaussianSourceDimensionWidth shape) (BinaryEncoding.encodeThreeCNF formula) rank) = List.replicate (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension true

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

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianRankDimensionAtomicComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperGaussianRankDimensionAtomicOutput shape)

GapCVP reduction support.

Equations

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

def GapCVP.GaussianOutputSerializerTM.paperGaussianRankTargetBound (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianOutputSerializerTM.paperGaussianRankTargetBound shape input = true :: true :: GapCVP.GaussianOutputSerializerTM.paperGaussianRankDimensionUnary shape input

noncomputable def GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianRankTargetBoundComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) : BitTM (paperGaussianRankTargetBound shape)

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianRankTargetBound_query (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) (rank : ℕ) : paperGaussianRankTargetBound shape (BinaryStructuralRecordTM.constructiveStructuralRankQuery (paperGaussianSourceDimensionWidth shape) (BinaryEncoding.encodeThreeCNF formula) rank) = List.replicate (2 + (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) true

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

GapCVP reduction support.

Equations

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

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

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianBasisRowUnary_query (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) (rank : ℕ) : paperGaussianBasisRowUnary shape (BinaryStructuralRecordTM.constructiveStructuralRankQuery (paperGaussianSourceDimensionWidth shape) (BinaryEncoding.encodeThreeCNF formula) rank) = List.replicate ((rank - (2 + (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension)) / (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) true

theorem GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianBasisColumnUnary_query (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (formula : ThreeCNF) (rank : ℕ) : paperGaussianBasisColumnUnary shape (BinaryStructuralRecordTM.constructiveStructuralRankQuery (paperGaussianSourceDimensionWidth shape) (BinaryEncoding.encodeThreeCNF formula) rank) = List.replicate ((rank - (2 + (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension)) % (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension) true

def GapCVP.GaussianOutputSerializerTM.paperGaussianRankBasisStateQuery (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (reduced : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianRankBasisStateQueryComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {reduced : List Bool → List Bool} (computer : BitTM reduced) : BitTM (paperGaussianRankBasisStateQuery shape reduced)

GapCVP reduction support.

Equations

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

def GapCVP.GaussianOutputSerializerTM.paperGaussianStructuralAtomOutput (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) (radius reduced : List Bool → List Bool) : List Bool → List Bool

Compute the structural atom used by the paper's Gaussian reduction.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianStructuralAtomComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {radius reduced : List Bool → List Bool} (radiusComputer : BitTM radius) (reducedComputer : BitTM reduced) : BitTM (paperGaussianStructuralAtomOutput shape radius reduced)

GapCVP reduction support.

@[irreducible]

noncomputable def GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianStructuralAtomComputer (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {radius reduced : List Bool → List Bool} (radiusComputer : BitTM radius) (reducedComputer : BitTM reduced) : BinaryStructuralRecordTM.ConstructiveStructuralAtomComputer

GapCVP reduction support.

noncomputable def GapCVP.GaussianOutputSerializerTM.paperGaussianStructuralSourceWord (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {radius reduced : List Bool → List Bool} (radiusComputer : BitTM radius) (reducedComputer : BitTM reduced) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianStructuralSourceWordComputable (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {radius reduced : List Bool → List Bool} (radiusComputer : BitTM radius) (reducedComputer : BitTM reduced) : BitTM (paperGaussianStructuralSourceWord shape radiusComputer reducedComputer)

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianOutputSerializerTM.paperGaussianRankReducedState_query (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {reduced : List Bool → List Bool} (formula : ThreeCNF) (rank : ℕ) (actual : reduced (BinaryEncoding.encodeThreeCNF formula) = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveGaussianState (BinaryEncoding.encodeThreeCNF formula)) : Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankReducedState reduced (BinaryStructuralRecordTM.constructiveStructuralRankQuery (paperGaussianSourceDimensionWidth shape) (BinaryEncoding.encodeThreeCNF formula) rank) = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveGaussianState (BinaryEncoding.encodeThreeCNF formula)

theorem GapCVP.GaussianOutputSerializerTM.paperVariableArityGaussianStructuralSourceWord_eq_encodeGapCVPInstance (shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape) {radius reduced : List Bool → List Bool} (radiusComputer : BitTM radius) (reducedComputer : BitTM reduced) (formula : ThreeCNF) (radiusValue : ℚ) (radiusPositive : 0 < radiusValue) (actualRadius : radius (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.encodeAtomic radiusValue) (actualReduced : reduced (BinaryEncoding.encodeThreeCNF formula) = GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveGaussianState (BinaryEncoding.encodeThreeCNF formula)) : paperGaussianStructuralSourceWord shape radiusComputer reducedComputer (BinaryEncoding.encodeThreeCNF formula) = BinaryEncoding.encodeGapCVPInstance (Factor400BinaryInstanceBridge.effectiveGapCVPInstance (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula) ⋯ radiusValue radiusPositive)

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaSize (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFormulaSize formula = GapCVP.Core.sourceSizeParameter (GapCVP.BinaryEncoding.encodeThreeCNF formula).length (GapCVP.FormulaBridge.srcFormula formula)

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physDegree (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physDegree formula = GapCVP.Core.sourceFieldExponent (GapCVP.PhysicalFamilyRowTM.physicalFormulaSize formula)

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physFieldCard (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physFieldCard formula = 2 ^ GapCVP.PhysicalFamilyRowTM.physDegree formula

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaVariableCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFormulaVariableCount formula = GapCVP.FormulaBridge.paperVariableArityVariableCount formula

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physGridCard (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physGridCard formula = GapCVP.PhysicalFamilyRowTM.physFieldCard formula - GapCVP.PhysicalFamilyRowTM.physicalFormulaVariableCount formula

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaMomentCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFormulaMomentCount formula = GapCVP.PhysicalFamilyRowTM.physicalFormulaSize formula ^ 30 + 1

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaTupleCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFormulaTupleCount formula = GapCVP.ClauseOffsetTM.sourceClauseWeightSum (GapCVP.BinarySourceTautologyNormalizationExact.noTautClauses formula)

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaGlobalBoundary (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula = GapCVP.PhysicalFamilyRowTM.physGridCard formula * GapCVP.PhysicalFamilyRowTM.physDegree formula

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaRefinementBoundary (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalFamilyRowTM.physicalFamilyVariableCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyVariableCountUnaryComputable : BitTM physicalFamilyVariableCountUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyVariableCountUnary_valid (formula : ThreeCNF) : physicalFamilyVariableCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (physicalFormulaVariableCount formula) true

noncomputable def GapCVP.PhysicalFamilyRowTM.physicalFamilyPowerTwoHundredUnary : List Bool → List Bool

Encode the physical family size raised to the 200th power in unary form.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyPowerTwoHundredUnaryComputable : BitTM physicalFamilyPowerTwoHundredUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.physicalFamilyFieldCardinalityUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFamilyFieldCardinalityUnary = GapCVP.BinaryDimensionTM.nextPowerUnaryOutput GapCVP.PhysicalFamilyRowTM.physicalFamilyPowerTwoHundredUnary

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldCardinalityUnaryComputable : BitTM physicalFamilyFieldCardinalityUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldCardinalityUnary_valid (formula : ThreeCNF) : physicalFamilyFieldCardinalityUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (physFieldCard formula) true

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldCardinalityBinary : List Bool → List Bool

Encode the physical family field cardinality in binary form.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldCardinalityBinaryComputable : BitTM paperVariableArityPhysicalFamilyFieldCardinalityBinary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldBitLengthUnary : List Bool → List Bool

Encode the field bit length of a physical family in unary form.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldBitLengthUnaryComputable : BitTM paperVariableArityPhysicalFamilyFieldBitLengthUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.physicalFamilyFieldDegreeUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFamilyFieldDegreeUnary = List.tail ∘ GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldBitLengthUnary

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldDegreeUnaryComputable : BitTM physicalFamilyFieldDegreeUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyFieldDegreeUnary_valid (formula : ThreeCNF) : physicalFamilyFieldDegreeUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (physDegree formula) true

noncomputable def GapCVP.PhysicalFamilyRowTM.physicalFamilyGridCardinalityUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyGridCardinalityUnaryComputable : BitTM physicalFamilyGridCardinalityUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyGridCardinalityUnary_valid (formula : ThreeCNF) : physicalFamilyGridCardinalityUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (physGridCard formula) true

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyMomentBudgetUnary : List Bool → List Bool

Encode the physical family's moment budget in unary form.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyMomentBudgetUnaryComputable : BitTM paperVariableArityPhysicalFamilyMomentBudgetUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyRowTM.physicalFamilyMomentCountUnary (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFamilyMomentCountUnary input = true :: GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyMomentBudgetUnary input

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyMomentCountUnaryComputable : BitTM physicalFamilyMomentCountUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyMomentCountUnary_valid (formula : ThreeCNF) : physicalFamilyMomentCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (physicalFormulaMomentCount formula) true

def GapCVP.PhysicalFamilyRowTM.physicalFamilyTupleCountUnary : List Bool → List Bool

Encode the number of physical family tuples in unary form.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFamilyTupleCountUnary = GapCVP.SourcePreprocessingTM.paperSourcePreprocessingField 1 ∘ GapCVP.ClauseOffsetTM.paperClauseOffsetOutput

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyTupleCountUnaryComputable : BitTM physicalFamilyTupleCountUnary

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalFamilyRowTM.physicalFamilyTypeCountUnary (input : List Bool) : List Bool

Encode the number of physical family types in unary form.

Equations

• GapCVP.PhysicalFamilyRowTM.physicalFamilyTypeCountUnary input = true :: GapCVP.PhysicalFamilyRowTM.physicalFamilyTupleCountUnary input

noncomputable def GapCVP.PhysicalFamilyRowTM.paperVariableArityPhysicalFamilyTypeCountUnaryComputable : BitTM physicalFamilyTypeCountUnary

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.physicalOneHotClauseCountUnary (input : List Bool) : List Bool

Encode the number of one-hot clauses in unary form.

Equations

• GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.physicalOneHotClauseCountUnary input = true :: GapCVP.PhysicalFamilyRowTM.physicalFamilyClauseCountUnary✝ input

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.paperVariableArityPhysicalOneHotClauseCountUnaryComputable : BitTM physicalOneHotClauseCountUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.physicalOneHotWeightUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.paperVariableArityPhysicalOneHotWeightUnaryComputable : BitTM physicalOneHotWeightUnary

GapCVP reduction support.

@[simp]

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.paperVariableArityPhysicalOneHotWeightUnary_valid (formula : ThreeCNF) : physicalOneHotWeightUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate ((List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula) + 1) * (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid (BinaryEncoding.encodeThreeCNF formula).length (FormulaBridge.srcFormula formula)).card) true

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.paperVariableArityPhysicalRadiusAtomicOutput : List Bool → List Bool

Compute the atomic physical radius output of the variable-arity source.

Equations

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

@[irreducible]

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRadiusMachine.paperVariableArityPhysicalRadiusAtomicComputable : BitTM paperVariableArityPhysicalRadiusAtomicOutput

GapCVP reduction support.

def GapCVP.PhysicalNormalizedBranchTM.physicalNormalizedNonemptyMarker (input : List Bool) : Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalNormalizedBranchTM.physicalNormalizedNonemptyMarker input = (GapCVP.PhysicalFamilyRowTM.physicalFamilyClauseCountUnary✝ input).headD false

def GapCVP.PhysicalNormalizedBranchTM.physicalNormalizedNonemptyDecisionWord : List Bool → List Bool

Encode the normalized nonempty-case decision bit.

Equations

• GapCVP.PhysicalNormalizedBranchTM.physicalNormalizedNonemptyDecisionWord = GapCVP.GaussianRowWorker.binaryGaussianFirstCellWord ∘ GapCVP.PhysicalFamilyRowTM.physicalFamilyClauseCountUnary✝

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalNormalizedNonemptyDecisionComputable : BitTM physicalNormalizedNonemptyDecisionWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalNormalizedNonemptyMarker_valid (formula : ThreeCNF) : physicalNormalizedNonemptyMarker (BinaryEncoding.encodeThreeCNF formula) = decide (SourcePreprocessingSemantics.paperSourceNormalizedClauses formula ≠ [])

def GapCVP.PhysicalNormalizedBranchTM.physicalNormalizedEmptyDecisionWord : List Bool → List Bool

Encode the normalized empty-case decision bit.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalNormalizedEmptyDecisionComputable : BitTM physicalNormalizedEmptyDecisionWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedBranchTM.physicalCanonicalDecisionWord : List Bool → List Bool

Encode the canonical physical decision bit.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalCanonicalDecisionComputable : BitTM physicalCanonicalDecisionWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedBranchTM.physicalCanonicalNormalizedNonemptyGuard (input : List Bool) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedBranchTM.physicalCanonicalNormalizedNonemptyDecisionWord : List Bool → List Bool

Encode the canonical normalized nonempty-case decision bit.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalCanonicalNormalizedNonemptyDecisionComputable : BitTM physicalCanonicalNormalizedNonemptyDecisionWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedBranchTM.physicalCanonicalNormalizedNonemptySelectionOutput : List Bool → List Bool

Select the canonical normalized nonempty-case output.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalCanonicalNormalizedNonemptyPreservedComputable : BitTM (SourceOriginalSourcePreservingTM.originalSourcePreservingOutput physicalCanonicalNormalizedNonemptyDecisionWord)

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedBranchTM.paperVariableArityPhysicalCanonicalNormalizedNonemptySelectionComputable : BitTM physicalCanonicalNormalizedNonemptySelectionOutput

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedCanonicalGuardTM.physicalNormalizedEmptyMarker (input : List Bool) : Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalNormalizedCanonicalGuardTM.physicalNormalizedEmptyMarker input = !GapCVP.PhysicalNormalizedBranchTM.physicalNormalizedNonemptyMarker input

def GapCVP.PhysicalNormalizedCanonicalGuardTM.physicalCanonicalNormalizedEmptyGuard (input : List Bool) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedCanonicalGuardTM.physicalCanonicalNormalizedEmptyDecisionWord : List Bool → List Bool

Encode the canonical normalized empty-case decision bit.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedCanonicalGuardTM.paperVariableArityPhysicalCanonicalNormalizedEmptyDecisionComputable : BitTM physicalCanonicalNormalizedEmptyDecisionWord

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalNormalizedCanonicalGuardTM.physicalCanonicalNormalizedEmptySelectionOutput : List Bool → List Bool

Select the canonical normalized empty-case output.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedCanonicalGuardTM.paperVariableArityPhysicalCanonicalNormalizedEmptyPreservedComputable : BitTM (SourceOriginalSourcePreservingTM.originalSourcePreservingOutput physicalCanonicalNormalizedEmptyDecisionWord)

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedCanonicalGuardTM.paperVariableArityPhysicalCanonicalNormalizedEmptySelectionComputable : BitTM physicalCanonicalNormalizedEmptySelectionOutput

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedCanonicalGuardTM.paperVariableArityPhysicalCanonicalNormalizedEmptyGuardComputable : BitTM fun (input : List Bool) => physicalCanonicalNormalizedEmptyGuard input :: input

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.PhysicalNormalizedCanonicalGuardTM.paperVariableArityPhysicalCanonicalNormalizedNonemptyGuardComputable : BitTM fun (input : List Bool) => PhysicalNormalizedBranchTM.physicalCanonicalNormalizedNonemptyGuard input :: input

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianExactSourceInitializer.paperCanonicalSourceBinarySystem (input : List Bool) : Option Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

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

Compute the exact reduced state of a variable-arity source.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianExactSourceInitializer.gaussianPaperVariableArityExactSourceReducedStateComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (gaussianPaperVariableArityExactSourceReducedStateOutput worker)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianExactSourceInitializer.gaussianPaperVariableArityAllInputExactConsistencyOutput (input : List Bool) : List Bool

Compute exact Gaussian consistency on every source input.

Equations

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

@[irreducible]

noncomputable def GapCVP.GaussianExactSourceInitializer.gaussianPaperVariableArityAllInputExactConsistencyComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (worker : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM gaussianPaperVariableArityAllInputExactConsistencyOutput

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ExactPhysicalSourceTM.paperExactPhysicalStructuralOutput {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : List Bool → List Bool

Compute the exact physical structural output.

Equations

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

@[irreducible]

noncomputable def GapCVP.ExactPhysicalSourceTM.paperVariableArityExactPhysicalStructuralOutputComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperExactPhysicalStructuralOutput cell)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ExactPhysicalSourceTM.paperExactPhysicalRoutedOutput {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) (input : List Bool) : List Bool

Route the exact physical output through its selected branch.

Equations

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

@[irreducible]

noncomputable def GapCVP.ExactPhysicalSourceTM.paperVariableArityExactPhysicalRoutedOutputComputable {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM (paperExactPhysicalRoutedOutput cell)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.ExactPhysicalSourceTM.paperVariableArityExactPhysicalConsistencyGuard_encode (formula : ThreeCNF) : GaussianSourceConsistencyBridge.binaryGaussianSourceConsistencyGuard GaussianExactSourceInitializer.paperCanonicalSourceBinarySystem (BinaryEncoding.encodeThreeCNF formula) = (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveReducedConsistent

theorem GapCVP.ExactPhysicalSourceTM.physicalRoutedOutput_eq_sourceMap (structuralOutput sourceMap : List Bool → List Bool) (noWord : List Bool) (decodeNone : ∀ (input : List Bool), BinaryEncoding.decodeThreeCNF input = none → noWord = sourceMap input) (noncanonical : ∀ (input : List Bool) (formula : ThreeCNF), BinaryEncoding.decodeThreeCNF input = some formula → BinaryEncoding.encodeThreeCNF formula ≠ input → noWord = sourceMap input) (normalizedEmpty : ∀ (formula : ThreeCNF), SourcePreprocessingSemantics.paperSourceNormalizedClauses formula = [] → SourceMachineRouting.canonicalYesWord = sourceMap (BinaryEncoding.encodeThreeCNF formula)) (inconsistent : ∀ (formula : ThreeCNF), SourcePreprocessingSemantics.paperSourceNormalizedClauses formula ≠ [] → (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveReducedConsistent = false → noWord = sourceMap (BinaryEncoding.encodeThreeCNF formula)) (consistent : ∀ (formula : ThreeCNF), SourcePreprocessingSemantics.paperSourceNormalizedClauses formula ≠ [] → (Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.physicalFormulaSystem (BinaryEncoding.encodeThreeCNF formula).length formula).effectiveReducedConsistent = true → structuralOutput (BinaryEncoding.encodeThreeCNF formula) = sourceMap (BinaryEncoding.encodeThreeCNF formula)) (input : List Bool) : (if PhysicalNormalizedCanonicalGuardTM.physicalCanonicalNormalizedEmptyGuard input = true then SourceMachineRouting.canonicalYesWord else if PhysicalNormalizedBranchTM.physicalCanonicalNormalizedNonemptyGuard input = true then if GaussianSourceConsistencyBridge.binaryGaussianSourceConsistencyGuard GaussianExactSourceInitializer.paperCanonicalSourceBinarySystem input = true then structuralOutput input else noWord else noWord) = sourceMap input

Identifies the shared physical routing tree from its five semantic branches.

@[irreducible]

noncomputable def GapCVP.ExactPhysicalSourceTM.paperVariableArityPhysicalSourceMapMachineOfCell {shape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape} (cell : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixCellComputer shape) : BitTM Factor400BinaryConstructivePaperVariableArityPhysicalSourceMap.paperVariableArityPhysicalSourceMap

GapCVP reduction support.

Equations

• GapCVP.ExactPhysicalSourceTM.paperVariableArityPhysicalSourceMapMachineOfCell cell = ⋯.mp (GapCVP.ExactPhysicalSourceTM.paperVariableArityExactPhysicalRoutedOutputComputable cell)

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalRefinementBoundaryUnary : List Bool → List Bool

Encode the physical refinement boundary in unary form.

Equations

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

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalRefinementBoundaryUnaryComputable : BitTM physicalRefinementBoundaryUnary

GapCVP reduction support.

Equations

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

def GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift (worker : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift worker = worker ∘ GapCVP.BinaryExplicitAffineRows.sourceExplicitAffineCellOriginalSource

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLiftComputable {worker : List Bool → List Bool} (computer : BitTM worker) : BitTM (physicalCellSourceLift worker)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellSourceLift_query (worker : List Bool → List Bool) (row column : ℕ) (formula : ThreeCNF) : physicalCellSourceLift worker (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = worker (BinaryEncoding.encodeThreeCNF formula)

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalCellGlobalBoundaryUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.physicalCellGlobalBoundaryUnary = GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift GapCVP.PhysicalFamilyMarkerTM.physicalGlobalBoundaryUnary✝

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellGlobalBoundaryUnaryComputable : BitTM physicalCellGlobalBoundaryUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellGlobalBoundaryUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalCellGlobalBoundaryUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula) true

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalCellRefinementBoundaryUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.physicalCellRefinementBoundaryUnary = GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift GapCVP.PhysicalFamilyMarkerTM.physicalRefinementBoundaryUnary

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellRefinementBoundaryUnaryComputable : BitTM physicalCellRefinementBoundaryUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellRefinementBoundaryUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalCellRefinementBoundaryUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula) true

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalCellOrdinaryBoundaryUnary : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.physicalCellOrdinaryBoundaryUnary = GapCVP.PhysicalFamilyMarkerTM.physicalCellSourceLift GapCVP.PhysicalFamilyMarkerTM.physicalOrdinaryBoundaryUnary✝

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellOrdinaryBoundaryUnaryComputable : BitTM physicalCellOrdinaryBoundaryUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalCellOrdinaryBoundaryUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalCellOrdinaryBoundaryUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula) true

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalRowBeforeGlobal : List Bool → List Bool

Tests whether a physical row precedes the global-family boundary.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.PhysicalFamilyMarkerTM.physicalGlobalRowMarker : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.physicalGlobalRowMarker = GapCVP.PhysicalFamilyMarkerTM.physicalRowBeforeGlobal

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalGlobalRowMarkerComputable : BitTM physicalGlobalRowMarker

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalGlobalRowMarkerComputable = GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalRowBeforeGlobalComputable✝

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalGlobalRowMarker_query (row column : ℕ) (formula : ThreeCNF) : physicalGlobalRowMarker (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide (row < PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula)]

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalRefinementRowMarker : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalRefinementRowMarkerComputable : BitTM physicalRefinementRowMarker

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalRefinementRowMarker_query (row column : ℕ) (formula : ThreeCNF) : physicalRefinementRowMarker (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaGlobalBoundary formula ≤ row ∧ row < PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula)]

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalOrdinaryRowMarker : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalOrdinaryRowMarkerComputable : BitTM physicalOrdinaryRowMarker

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalOrdinaryRowMarker_query (row column : ℕ) (formula : ThreeCNF) : physicalOrdinaryRowMarker (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaRefinementBoundary formula ≤ row ∧ row < PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula)]

noncomputable def GapCVP.PhysicalFamilyMarkerTM.physicalShiftedRowMarker : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.PhysicalFamilyMarkerTM.physicalShiftedRowMarker = GapCVP.SourceFourFamilyBooleanPredicateTM.sourceFourFamilyBooleanNotOutput GapCVP.PhysicalFamilyMarkerTM.physicalRowBeforeOrdinary✝

noncomputable def GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalShiftedRowMarkerComputable : BitTM physicalShiftedRowMarker

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalFamilyMarkerTM.paperVariableArityPhysicalShiftedRowMarker_query (row column : ℕ) (formula : ThreeCNF) : physicalShiftedRowMarker (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide (PhysicalFamilyRowTM.physicalFormulaOrdinaryBoundary formula ≤ row)]

def GapCVP.ShiftedTupleTM.paperShiftedSourceClauseWeight (clause : ThreeClause) : ℕ

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleTM.paperShiftedSourceClauseWeightSum (clauses : List ThreeClause) : ℕ

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleTM.paperShiftedSourceClauseWeightSum clauses = (List.map GapCVP.ShiftedTupleTM.paperShiftedSourceClauseWeight clauses).sum

def GapCVP.ShiftedTupleTM.paperShiftedClauseWeightUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleTM.paperVariableArityShiftedClauseWeightUnaryComputable : BitTM paperShiftedClauseWeightUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.ShiftedTupleTM.paperVariableArityShiftedClauseWeightUnary_valid (clause : ThreeClause) (suffix : List Bool) : paperShiftedClauseWeightUnary (BinaryEncoding.encodeThreeClause clause ++ suffix) = List.replicate (paperShiftedSourceClauseWeight clause) true

@[reducible, inline]

abbrev GapCVP.ShiftedTupleTM.paperVariableArityShiftedRetainedSourceWord : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleTM.paperVariableArityShiftedRetainedSourceWord = GapCVP.SourcePreprocessingTM.paperPreprocessingFilteredFormulaWord

noncomputable def GapCVP.ShiftedTupleTM.paperVariableArityShiftedRetainedSourceWordComputable : BitTM paperVariableArityShiftedRetainedSourceWord

GapCVP reduction support.

noncomputable def GapCVP.ShiftedTupleTM.paperShiftedRetainedClauseWidth : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.ShiftedTupleTM.paperVariableArityShiftedRetainedClauseWidth_output (input : List Bool) : paperShiftedRetainedClauseWidth.output input = ClauseOffsetTM.paperRetainedClauseCountUnary input

def GapCVP.ShiftedTupleTM.paperShiftedIndexedClauseQuery (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.ShiftedTupleTM.paperVariableArityShiftedIndexedClauseQueryComputable : BitTM paperShiftedIndexedClauseQuery

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.ShiftedTupleTM.paperVariableArityShiftedIndexedClauseQuery_valid (formula : ThreeCNF) (rank : ℕ) : paperShiftedIndexedClauseQuery (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ SourceMixedRadixMaskSelectedFlatPreparationTM.sourceQaryMaskDynamicGridBaseSource paperShiftedRetainedClauseWidth (BinaryEncoding.encodeThreeCNF formula)) = SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseQuery rank (BinarySourceTautologyNormalizationExact.noTautClauses formula)

def GapCVP.ShiftedTupleTM.paperVariableArityShiftedIndexedClauseWeightUnary : List Bool → List Bool

Encode a shifted indexed clause weight in unary form.

Equations

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

noncomputable def GapCVP.ShiftedTupleTM.paperVariableArityShiftedIndexedClauseWeightUnaryComputable : BitTM paperVariableArityShiftedIndexedClauseWeightUnary

GapCVP reduction support.

Equations

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

def GapCVP.ShiftedTupleTM.paperShiftedIndexedSourceClauseWeight (clauses : List ThreeClause) (rank : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.ShiftedTupleTM.paperShiftedIndexedSourceClauseWeight clauses rank = match clauses[rank]? with | some clause => GapCVP.ShiftedTupleTM.paperShiftedSourceClauseWeight clause | none => 0

theorem GapCVP.ShiftedTupleTM.paperVariableArityShiftedSourceClauseWeight_flatMap (clauses : List ThreeClause) : List.flatMap (fun (rank : ℕ) => List.replicate (paperShiftedIndexedSourceClauseWeight clauses rank) true) (List.range clauses.length) = List.replicate (paperShiftedSourceClauseWeightSum clauses) true

theorem GapCVP.CanonicalOffsetIdentity.sourceListWeightSum {α : Type u_1} (clauses : List α) (weight : α → ℕ) : (List.map weight clauses).sum = ∑ index : Fin clauses.length, weight (clauses.get index)

@[reducible, inline]

abbrev GapCVP.CanonicalOffsetIdentity.paperRetainedOriginalClauseIndexOrder (formula : ThreeCNF) : Fin (List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)) ≃ Fin (FormulaBridge.srcFormula formula).clauses.length

GapCVP reduction support.

Equations

• GapCVP.CanonicalOffsetIdentity.paperRetainedOriginalClauseIndexOrder formula = finCongr ⋯

theorem GapCVP.CanonicalOffsetIdentity.paperFormulaClauseWidth_retainedOriginal (formula : ThreeCNF) (index : Fin (List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula))) : SourceOrder.paperFormulaClauseWidth formula ((paperRetainedOriginalClauseIndexOrder formula) index) = (SourcePreprocessingSemantics.paperSourceNormalizedClause (List.get (BinarySourceTautologyNormalizationExact.noTautClauses formula) index)).length

theorem GapCVP.CanonicalOffsetIdentity.sourceClauseWeightSum_eq_localTagCount (formula : ThreeCNF) : ClauseOffsetTM.sourceClauseWeightSum (BinarySourceTautologyNormalizationExact.noTautClauses formula) = SourceOrder.paperVariableArityLocalTagCount formula

theorem GapCVP.CanonicalOffsetIdentity.paperVariableArityShiftedFamilyTagCount_eq_sourceWeight (formula : ThreeCNF) (momentBudget : ℕ) : SourceOrder.paperShiftedFamilyTagCount formula momentBudget = ShiftedTupleTM.paperShiftedSourceClauseWeightSum (BinarySourceTautologyNormalizationExact.noTautClauses formula) * (momentBudget + 1)

@[reducible, inline]

abbrev GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.physicalFormulaShiftedTupleCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalFormulaShiftedWidth (formula : ThreeCNF) : ℕ

Number of shifted-family rows in the physical formula system.

Equations

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

@[reducible, inline]

abbrev GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalFormulaRowCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.physicalShiftedTupleCountUnary : List Bool → List Bool

Encode the shifted physical tuple count in unary form.

Equations

• GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.physicalShiftedTupleCountUnary = GapCVP.ShiftedTupleTM.paperVariableArityShiftedTagCountUnary✝

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalShiftedTupleCountUnaryComputable : BitTM physicalShiftedTupleCountUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.physicalRowCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalRowCountUnaryComputable : BitTM physicalRowCountUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.physicalColumnCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalColumnCountUnaryComputable : BitTM physicalColumnCountUnary

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalColumnCountUnary_valid (formula : ThreeCNF) : physicalColumnCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension true

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityExplicitBinaryRowWordCount_eq_fourFamily (formula : ThreeCNF) : SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula = paperVariableArityPhysicalFormulaRowCount formula

theorem GapCVP.Factor400BinaryConstructivePaperVariableArityPhysicalRowCountMachine.paperVariableArityPhysicalRowCountUnary_valid (formula : ThreeCNF) : physicalRowCountUnary (BinaryEncoding.encodeThreeCNF formula) = List.replicate (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount true

noncomputable def GapCVP.CanonicalPhysicalMatrixShape.paperCanonicalPhysicalMatrixShape : CanonicalMatrixShape.PaperVariableArityCanonicalBinaryMatrixShape

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CanonicalPhysicalMatrixShape.paperVariableArityCanonicalPhysicalMatrixShape_rows_valid (formula : ThreeCNF) : paperCanonicalPhysicalMatrixShape.rows (BinaryEncoding.encodeThreeCNF formula) = List.replicate (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).rowCount true

@[simp]

theorem GapCVP.CanonicalPhysicalMatrixShape.paperVariableArityCanonicalPhysicalMatrixShape_columns_valid (formula : ThreeCNF) : paperCanonicalPhysicalMatrixShape.columns (BinaryEncoding.encodeThreeCNF formula) = List.replicate (PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).dimension true

@[reducible, inline]

abbrev GapCVP.CanonicalPhysicalMatrixShape.PaperVariableArityCanonicalPhysicalBinaryMatrixCellComputer : Type 1

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitIndex : List Bool → List Bool

Read the coefficient bit index from a compact physical field query.

Equations

• GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitIndex = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitIndexComputable : BitTM compactPhysicalFieldCoefficientBitIndex

GapCVP reduction support.

Equations

• GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitIndexComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitSource : List Bool → List Bool

Read the source word from a compact coefficient bit query.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitSourceComputable : BitTM compactPhysicalFieldCoefficientBitSource

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitWord : List Bool → List Bool

Compute the selected bit of a compact physical field coefficient.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitComputable : BitTM compactPhysicalFieldCoefficientBitWord

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitPreparedQuery (basisRank coefficient source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) : List Bool

Prepare the query for a compact coefficient bit computation.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientBitPreparedQueryComputable (basisRank coefficient source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldCoefficientBitPreparedQuery basisRank coefficient source)

GapCVP reduction support.

Equations

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

def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientPreparedBit (basisRank coefficient source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientPreparedBitComputable (basisRank coefficient source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldCoefficientPreparedBit basisRank coefficient source)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientPreparedBit_bounded_valid {degree : ℕ} (basisRank coefficient source : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (input : List Bool) (formula : ThreeCNF) (word : Core.EffectiveBinaryField.Word degree) (position : ℕ) (hposition : position < degree) (hrank : basisRank.output input = List.replicate position true) (hcoefficient : coefficient.output input = BinaryModularReductionTM.finiteWordBits word) (hsource : source.output input = BinaryEncoding.encodeThreeCNF formula) : compactPhysicalFieldCoefficientPreparedBit basisRank coefficient source input = [word ⟨position, hposition⟩]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientCellBit (basisRank coefficient : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientCellBitComputable (basisRank coefficient : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) : BitTM (compactPhysicalFieldCoefficientCellBit basisRank coefficient)

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryCompactPhysicalFieldCoefficientBitTM.compactPhysicalFieldCoefficientCellBit_valid {degree : ℕ} (basisRank coefficient : BinaryPhysicalLagrangeCoefficientTM.SourcePhysicalLagrangeWordComputer) (row column : ℕ) (formula : ThreeCNF) (word : Core.EffectiveBinaryField.Word degree) (position : ℕ) (hposition : position < degree) (hrank : basisRank.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate position true) (hcoefficient : coefficient.output (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = BinaryModularReductionTM.finiteWordBits word) : compactPhysicalFieldCoefficientCellBit basisRank coefficient (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [word ⟨position, hposition⟩]

theorem GapCVP.BinaryCompactPhysicalFieldBasisCoordinates.sourceFormulaFieldBasis_sourceWordValue_coordinate (encodingLength : ℕ) (formula : Core.Formula) (word : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) (index : Fin (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) : (Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis encodingLength formula).equivFun (BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula word) index = Core.EffectiveBinaryField.bitValue (word index)

@[reducible, inline]

abbrev GapCVP.MatrixEntrySemantics.PaperVariableArityPhysicalWordField (encodingLength : ℕ) (formula : ThreeCNF) : Type

GapCVP reduction support.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (encodingLength : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.MatrixEntrySemantics.PaperVariableArityPhysicalWordGrid (encodingLength : ℕ) (formula : ThreeCNF) : Finset (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula))

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.MatrixEntrySemantics.physicalWordCoordinateDelta (encodingLength : ℕ) (formula : ThreeCNF) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) (tableType : Core.sourceSATTableType (FormulaBridge.srcFormula formula)) (point : Core.sourceSATGridPoint (PaperVariableArityPhysicalWordGrid encodingLength formula)) (value : PaperVariableArityPhysicalWordField encodingLength formula) : PaperVariableArityPhysicalWordField encodingLength formula

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.MatrixEntrySemantics.physicalWordFamilyFieldCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (family : BinaryExplicitAffineSystem.ExplicitConstraintFamily encodingLength (FormulaBridge.srcFormula formula)) (row : Fin (BinaryExplicitAffineSystem.explicitFamilyRowCount encodingLength (FormulaBridge.srcFormula formula) family)) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) : PaperVariableArityPhysicalWordField encodingLength formula

GapCVP reduction support.

Equations

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

theorem GapCVP.MatrixEntrySemantics.paperVariableArityPhysicalWordGlobalFieldCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) : physicalWordFamilyFieldCoefficient encodingLength formula (Sum.inl ()) row column = ∑ value : PaperVariableArityPhysicalWordField encodingLength formula, physicalWordCoordinateDelta encodingLength formula column (Sum.inl ()) ((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) row) value

theorem GapCVP.MatrixEntrySemantics.paperVariableArityPhysicalWordRefinementFieldCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) (row : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula) × PaperVariableArityPhysicalWordField encodingLength formula))) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) : physicalWordFamilyFieldCoefficient encodingLength formula (Sum.inr (Sum.inl clause)) row column = have position := (BinarySourceRowOrder.sourceFormulaExplicitRefinementOrder encodingLength (FormulaBridge.srcFormula formula)) row; physicalWordCoordinateDelta encodingLength formula column (Sum.inl ()) position.1 position.2 - ∑ tuple : ((FormulaBridge.srcFormula formula).clauses.get clause).SatisfyingLocalTuple, physicalWordCoordinateDelta encodingLength formula column (Sum.inr ⟨clause, tuple⟩) position.1 position.2

theorem GapCVP.MatrixEntrySemantics.paperVariableArityPhysicalWordOrdinaryFieldCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (tableType : Core.sourceSATTableType (FormulaBridge.srcFormula formula)) (moment : Fin (BinaryExplicitAffineSystem.explicitMomentBudget encodingLength (FormulaBridge.srcFormula formula) + 1)) (row : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) : physicalWordFamilyFieldCoefficient encodingLength formula (Sum.inr (Sum.inr (Sum.inl (tableType, moment)))) row column = ∑ position : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula))), BinaryReedSolomonParity.constructiveParityMatrix (fun (index : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) => ↑((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) index)) ⋯ row position * ∑ value : PaperVariableArityPhysicalWordField encodingLength formula, physicalWordCoordinateDelta encodingLength formula column tableType ((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) position) value * value ^ ↑moment

theorem GapCVP.MatrixEntrySemantics.paperVariableArityPhysicalWordShiftedFieldCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) (tuple : ((FormulaBridge.srcFormula formula).clauses.get clause).SatisfyingLocalTuple) (localVariable : ((FormulaBridge.srcFormula formula).clauses.get clause).LocalVariable) (moment : Fin (BinaryExplicitAffineSystem.explicitMomentBudget encodingLength (FormulaBridge.srcFormula formula) + 1)) (row : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) : physicalWordFamilyFieldCoefficient encodingLength formula (Sum.inr (Sum.inr (Sum.inr ⟨clause, ⟨tuple, (localVariable, moment)⟩⟩))) row column = ∑ position : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula))), BinaryReedSolomonParity.constructiveParityMatrix (fun (index : Fin (Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)))) => ↑((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) index)) ⋯ row position * ∑ value : PaperVariableArityPhysicalWordField encodingLength formula, physicalWordCoordinateDelta encodingLength formula column (Sum.inr ⟨clause, tuple⟩) ((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) position) value * ((value - Core.sourceSATFieldBit (↑tuple localVariable)) / (↑((BinaryExplicitAffineSystem.sourceFormulaExplicitGridOrder encodingLength (FormulaBridge.srcFormula formula)) position) - Factor400BinaryConstructiveSourcePlaces.sourceFormulaVariablePlace encodingLength (FormulaBridge.srcFormula formula) ↑localVariable)) ^ ↑moment

@[reducible, inline]

noncomputable abbrev GapCVP.MatrixEntrySemantics.physicalWordDecodedRow (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : Core.assembledBinaryRow (BinaryExplicitAffineSystem.explicitFamilyRowCount encodingLength (FormulaBridge.srcFormula formula)) (SourceOrder.paperExplicitBinaryRowDegree encodingLength formula)

GapCVP reduction support.

Equations

• GapCVP.MatrixEntrySemantics.physicalWordDecodedRow encodingLength formula row = (GapCVP.SourceOrder.paperVariableArityExplicitBinaryRowWordOrder encodingLength formula) row

theorem GapCVP.MatrixEntrySemantics.physicalWordBinaryCheckCoefficient (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) (column : Fin (PaperVariableArityPhysicalWordDimension encodingLength formula)) : (PhysicalColumnOrder.physicalWordBinarySystem encodingLength formula).check row column = (Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis encodingLength (FormulaBridge.srcFormula formula)).equivFun (physicalWordFamilyFieldCoefficient encodingLength formula (physicalWordDecodedRow encodingLength formula row).fst (physicalWordDecodedRow encodingLength formula row).snd.1 column) (physicalWordDecodedRow encodingLength formula row).snd.2

@[simp]

theorem GapCVP.MatrixEntrySemantics.paperVariableArityPhysicalFieldBasis_one_coordinate (encodingLength : ℕ) (formula : ThreeCNF) (coordinate : Fin (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength (FormulaBridge.srcFormula formula)))) : (Factor400BinaryConstructiveSourcePlaces.sourceFormulaFieldBasis encodingLength (FormulaBridge.srcFormula formula)).equivFun 1 coordinate = Core.EffectiveBinaryField.bitValue (decide (↑coordinate = 0))

noncomputable def GapCVP.PhysicalRowOrderProjection.physicalRowDependentFamilyIndex (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : Fin (SourceOrder.paperExplicitFamilyTagCount encodingLength formula)

GapCVP reduction support.

Equations

• GapCVP.PhysicalRowOrderProjection.physicalRowDependentFamilyIndex encodingLength formula row = (finSigmaFinEquiv.symm row).fst

noncomputable def GapCVP.PhysicalRowOrderProjection.physicalRowDependentBlockRank (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : Fin (SourceOrder.paperExplicitBinaryFamilyBlockCount encodingLength formula (physicalRowDependentFamilyIndex encodingLength formula row))

GapCVP reduction support.

Equations

• GapCVP.PhysicalRowOrderProjection.physicalRowDependentBlockRank encodingLength formula row = (finSigmaFinEquiv.symm row).snd

theorem GapCVP.PhysicalRowOrderProjection.physicalRowDependentRank_eq_prefix (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : ↑row = ∑ index : Fin ↑(physicalRowDependentFamilyIndex encodingLength formula row), SourceOrder.paperExplicitBinaryFamilyBlockCount encodingLength formula (Fin.castLE ⋯ index) + ↑(physicalRowDependentBlockRank encodingLength formula row)

theorem GapCVP.PhysicalRowOrderProjection.physicalRowOrder_family (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : (MatrixEntrySemantics.physicalWordDecodedRow encodingLength formula row).fst = (SourceOrder.paperExplicitFamilyWordOrder encodingLength formula) (physicalRowDependentFamilyIndex encodingLength formula row)

theorem GapCVP.PhysicalRowOrderProjection.physicalRowOrder_fieldRow (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : ↑(MatrixEntrySemantics.physicalWordDecodedRow encodingLength formula row).snd.1 = ↑(physicalRowDependentBlockRank encodingLength formula row) / SourceOrder.paperExplicitBinaryRowDegree encodingLength formula

theorem GapCVP.PhysicalRowOrderProjection.physicalRowOrder_basis_val (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : ↑(MatrixEntrySemantics.physicalWordDecodedRow encodingLength formula row).snd.2 = ↑row % SourceOrder.paperExplicitBinaryRowDegree encodingLength formula

theorem GapCVP.PhysicalRowOrderProjection.physicalFamilyTagCount_pos (encodingLength : ℕ) (formula : ThreeCNF) : 0 < SourceOrder.paperExplicitFamilyTagCount encodingLength formula

theorem GapCVP.PhysicalRowOrderProjection.physicalFamilyWordOrder_zero (encodingLength : ℕ) (formula : ThreeCNF) : (SourceOrder.paperExplicitFamilyWordOrder encodingLength formula) ⟨0, ⋯⟩ = Sum.inl ()

theorem GapCVP.PhysicalRowOrderProjection.physicalFirstFamilyBlockCount (encodingLength : ℕ) (formula : ThreeCNF) : SourceOrder.paperExplicitBinaryFamilyBlockCount encodingLength formula ⟨0, ⋯⟩ = Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)) * SourceOrder.paperExplicitBinaryRowDegree encodingLength formula

@[reducible, inline]

noncomputable abbrev GapCVP.PhysicalRowOrderProjection.physicalSourceGlobalBoundary (encodingLength : ℕ) (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalRowOrderProjection.paperVariableArityPhysicalRowOrder_global_iff (encodingLength : ℕ) (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount encodingLength formula)) : (MatrixEntrySemantics.physicalWordDecodedRow encodingLength formula row).fst = Sum.inl () ↔ ↑row < physicalSourceGlobalBoundary encodingLength formula

theorem GapCVP.PhysicalRowOrderProjection.physicalSourceGridCardinality_eq (encodingLength : ℕ) (formula : ThreeCNF) : Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)) = 2 ^ Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength (FormulaBridge.srcFormula formula)) - FormulaBridge.paperVariableArityVariableCount formula

def GapCVP.PhysicalRowOrderProjection.physicalSigmaPrefix {familyCount : ℕ} (blockCount : Fin familyCount → ℕ) (family : Fin familyCount) : ℕ

GapCVP reduction support.

Equations

• GapCVP.PhysicalRowOrderProjection.physicalSigmaPrefix blockCount family = ∑ index : Fin ↑family, blockCount (Fin.castLE ⋯ index)

theorem GapCVP.PhysicalRowOrderProjection.paperVariableArityPhysicalSigmaFamilyIndex_eq_iff {familyCount : ℕ} (blockCount : Fin familyCount → ℕ) (row : Fin (∑ index : Fin familyCount, blockCount index)) (family : Fin familyCount) : (finSigmaFinEquiv.symm row).fst = family ↔ physicalSigmaPrefix blockCount family ≤ ↑row ∧ ↑row < physicalSigmaPrefix blockCount family + blockCount family

noncomputable def GapCVP.PhysicalRowOrderProjection.physicalRefinementFamilyIndex (encodingLength : ℕ) (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) : Fin (SourceOrder.paperExplicitFamilyTagCount encodingLength formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalRowOrderProjection.paperVariableArityPhysicalRefinementFamilyIndex_val (encodingLength : ℕ) (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) : ↑(physicalRefinementFamilyIndex encodingLength formula clause) = 1 + ↑clause

theorem GapCVP.PhysicalRowOrderProjection.paperVariableArityPhysicalRefinementFamilyBlockCount (encodingLength : ℕ) (formula : ThreeCNF) (clause : Fin (FormulaBridge.srcFormula formula).clauses.length) : SourceOrder.paperExplicitBinaryFamilyBlockCount encodingLength formula (physicalRefinementFamilyIndex encodingLength formula clause) = Fintype.card (BinaryExplicitAffineSystem.ExplicitGridPoint encodingLength (FormulaBridge.srcFormula formula)) * Fintype.card (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength (FormulaBridge.srcFormula formula)) * SourceOrder.paperExplicitBinaryRowDegree encodingLength formula

noncomputable def GapCVP.PhysicalRightHandSideTM.physicalRightHandSideCellDegreeUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSideCellDegreeUnaryComputable : BitTM physicalRightHandSideCellDegreeUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSideCellDegreeUnary_query (row column : ℕ) (formula : ThreeCNF) : physicalRightHandSideCellDegreeUnary (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = List.replicate (PhysicalFamilyRowTM.physDegree formula) true

noncomputable def GapCVP.PhysicalRightHandSideTM.physicalRightHandSideBasisRankUnary : List Bool → List Bool

Encode the right-hand-side basis rank in unary form.

Equations

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

noncomputable def GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSideBasisRankUnaryComputable : BitTM physicalRightHandSideBasisRankUnary

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRightHandSideTM.physicalRightHandSideBasisZeroBit : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSideBasisZeroBitComputable : BitTM physicalRightHandSideBasisZeroBit

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSideBasisZeroBit_query (row column : ℕ) (formula : ThreeCNF) : physicalRightHandSideBasisZeroBit (BinaryExplicitAffineRows.affineCellQuery row column (BinaryEncoding.encodeThreeCNF formula)) = [decide (row % PhysicalFamilyRowTM.physDegree formula = 0)]

noncomputable def GapCVP.PhysicalRightHandSideTM.physicalRightHandSideBit : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSideBitComputable : BitTM physicalRightHandSideBit

GapCVP reduction support.

Equations

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

theorem GapCVP.PhysicalRightHandSideTM.paperVariableArityPhysicalRightHandSide_valid (formula : ThreeCNF) (row : Fin (SourceOrder.paperExplicitBinaryRowWordCount (BinaryEncoding.encodeThreeCNF formula).length formula)) (column : Fin (MatrixEntrySemantics.PaperVariableArityPhysicalWordDimension (BinaryEncoding.encodeThreeCNF formula).length formula)) : physicalRightHandSideBit (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (BinaryEncoding.encodeThreeCNF formula)) = [decide ((PhysicalColumnOrder.physicalWordBinarySystem (BinaryEncoding.encodeThreeCNF formula).length formula).rightHandSide row = 1)]

theorem GapCVP.BinaryAllWordRankOrder.allWords_eq_finRange_indexedWord (degree : ℕ) : Core.EffectiveBinaryField.allWords degree = List.map (BinaryFieldBasis.indexedWord degree) (List.finRange (2 ^ degree))

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalCompositionComputer {f g : List Bool → List Bool} (first : BitTM f) (second : BitTM g) : BitTM (g ∘ f)

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalCompositionComputer first second = GapCVP.TMComposition.computableInPolyTime first second

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalAppendComputer {first second : List Bool → List Bool} (firstComputer : BitTM first) (secondComputer : BitTM second) : BitTM fun (input : List Bool) => first input ++ second input

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalDynamicCatalogueComputer (width : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth) {record : List Bool → List Bool} (computer : BitTM record) : BitTM (SourceMixedRadixMaskSelectedFlatPreparationTM.maskDynamicGridRecordCatalogueOutput width computer)

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalDynamicWidth {output : List Bool → List Bool} (computer : BitTM output) : SourceMixedRadixMaskSelectedFlatPreparationTM.SourceQaryMaskDynamicGridWidth

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalDynamicWidth computer = { output := output, computer := computer }

@[simp]

theorem GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalDynamicWidth_output {output : List Bool → List Bool} (computer : BitTM output) (input : List Bool) : (factor400BinaryIrreduciblePhysicalDynamicWidth computer).output input = output input

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFalseComputer : BitTM fun (x : List Bool) => [false]

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFalseComputer = GapCVP.SourceCanonicalFixedWordTuringTM.sourceFixedWordComputable [false]

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalTrueComputer : BitTM fun (x : List Bool) => [true]

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalTrueComputer = GapCVP.SourceCanonicalFixedWordTuringTM.sourceFixedWordComputable [true]

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalNaturalWriterComputer : BitTM fun (input : List Bool) => Computability.encodeNat input.length

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalNaturalWriterComputer = GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordNaturalWriterComputer

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalDropHeadComputer : BitTM List.tail

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalDropHeadComputer = GapCVP.BinaryPhysicalWordRuntimeDegreeTM.factor400BinaryPhysicalWordDropHeadComputer

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFieldContentsComputer : BitTM SourceFormulaStructuralDecoder.firstFieldContents

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFieldContentsComputer = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFieldSuffixComputer : BitTM SourceFormulaStructuralDecoder.firstFieldSuffix

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFieldSuffixComputer = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffixComputable

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalPrefixWriterComputer : BitTM BinaryEncoding.lengthPrefixedWord

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalPrefixWriterComputer = GapCVP.CLStructuralPrefixWriter.structuralPrefixWriterComputable

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreduciblePhysicalComputedPrefixOutput (word : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreduciblePhysicalComputedPrefixOutput word = GapCVP.BinaryEncoding.lengthPrefixedWord ∘ word

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalComputedPrefixComputer {word : List Bool → List Bool} (computer : BitTM word) : BitTM (binaryIrreduciblePhysicalComputedPrefixOutput word)

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalSquareComputer : BitTM fun (input : List Bool) => List.replicate (Polynomial.eval input.length (Polynomial.X ^ 2)) true

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalSquareComputer = GapCVP.CNFBoundedRecordFoldTM.polynomialValueUnaryComputable (Polynomial.X ^ 2)

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalConvolutionComputer : BitTM BinarySourceConvolutionTM.binarySourceRawConvolutionWord

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalConvolutionComputer = GapCVP.BinarySourceConvolutionTM.factor400BinarySourceRawConvolutionComputable

def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankUnary (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankUnary input = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents input

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankUnaryComputable : BitTM factor400BinaryIrreducibleRankUnary

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankUnaryComputable = GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreduciblePhysicalFieldContentsComputer

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleRankOriginal : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleRankOriginal = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankOriginalComputable : BitTM binaryIrreducibleRankOriginal

GapCVP reduction support.

Equations

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

theorem GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankOriginal_valid (rank auxiliary source : List Bool) : binaryIrreducibleRankOriginal (BinaryEncoding.lengthPrefixedWord rank ++ BinaryEncoding.lengthPrefixedWord auxiliary ++ source) = source

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleRankBinary : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankBinaryComputable : BitTM binaryIrreducibleRankBinary

GapCVP reduction support.

Equations

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

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleCoefficientOuterSource : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleCoefficientOuterSource = GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleRankOriginal

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleCoefficientOuterSourceComputable : BitTM binaryIrreducibleCoefficientOuterSource

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleCoefficientOuterSourceComputable = GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleRankOriginalComputable

def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleCoefficientRankBinary : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleCoefficientRankBinaryComputable : BitTM factor400BinaryIrreducibleCoefficientRankBinary

GapCVP reduction support.

Equations

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

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIrreducibleCoefficientBitWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleCoefficientBitComputable : BitTM binaryIrreducibleCoefficientBitWord

GapCVP reduction support.

Equations

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

theorem GapCVP.BinarySelectedIrreducibleWordTM.factor400Irreducible_encodeNat_drop_head (value index : ℕ) : (List.drop index (Computability.encodeNat value)).headD false = value.testBit index

theorem GapCVP.BinarySelectedIrreducibleWordTM.factor400BinaryIrreducibleFiniteWordBits_indexedWord (degree : ℕ) (rank : Fin (2 ^ degree)) : BinaryModularReductionTM.finiteWordBits (BinaryFieldBasis.indexedWord degree rank) = List.map (fun (bitRank : ℕ) => (↑rank).testBit bitRank) (List.range degree)

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIndexedNoProperFactorsBit (degree rank : ℕ) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinarySelectedIrreducibleWordTM.binarySourceIrreducibleFactorPairCandidateSource : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.binarySourceIrreducibleFactorPairCandidateSource = GapCVP.BinarySourceConvolutionTM.factor400BinarySourceSkipFields 2

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinarySourceIrreducibleFactorPairCandidateSourceComputable : BitTM binarySourceIrreducibleFactorPairCandidateSource

GapCVP reduction support.

Equations

• GapCVP.BinarySelectedIrreducibleWordTM.factor400BinarySourceIrreducibleFactorPairCandidateSourceComputable = GapCVP.BinarySourceConvolutionTM.binarySourceSkipFieldsComputable 2

def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinarySourceIrreducibleFactorPairOriginalSource : List Bool → List Bool

GapCVP reduction support.

Equations

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

@[irreducible]

noncomputable def GapCVP.BinarySelectedIrreducibleWordTM.factor400BinarySourceIrreducibleFactorPairOriginalSourceComputable : BitTM factor400BinarySourceIrreducibleFactorPairOriginalSource

GapCVP reduction support.

Equations

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

def GapCVP.BinarySelectedIrreducibleWordTM.binaryIndexedIrreducibleCandidateMarkers (degree : ℕ) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinarySelectedIrreducibleFactorCorrectness.binaryIndexedProperFactorPairBit (degree : ℕ) (lower : Core.EffectiveBinaryField.Word degree) (rank : ℕ) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinarySelectedIrreducibleFactorCorrectness.factor400BinaryIndexedProperFactorPairMarkers_find_none_iff (degree : ℕ) (lower : Core.EffectiveBinaryField.Word degree) : List.findIdx? id (List.map (binaryIndexedProperFactorPairBit degree lower) (List.range ((2 ^ degree) ^ 2))) = none ↔ ∀ (first second : Core.EffectiveBinaryField.Word degree), Core.EffectiveBinaryField.multiplyWords first second ≠ Core.EffectiveBinaryField.monicWord lower