GapCVP proof, part 11, continuation 03

theorem GapCVP.BinarySourceModularDegreeStepSemanticCoefficientLemmas.binarySourceModularFiniteWordBits_drop_head {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) (rank : ℕ) (hrank : rank < degree) : (List.drop rank (BinaryModularReductionTM.finiteWordBits word)).headD false = word ⟨rank, hrank⟩

theorem GapCVP.BinarySourceModularDegreeStepPhysicalCellCorrectness.binarySourceModularFiniteWordBits_drop_head {degree : ℕ} (word : Core.EffectiveBinaryField.Word degree) (rank : ℕ) (hrank : rank < degree) : (List.drop rank (BinaryModularReductionTM.finiteWordBits word)).headD false = word ⟨rank, hrank⟩

noncomputable def GapCVP.BinarySourceFieldMultiplicationTM.binarySourceMultiplyModComputable : BitTM binarySourceMultiplyModWord

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryFieldInverseTM.sourceWordValue_sourceFieldPowerIterate (encodingLength : ℕ) (formula : Core.Formula) (operand : Core.EffectiveBinaryField.Word (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) (steps : ℕ) : BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula (sourceFieldPowerIterate (Core.EffectiveBinaryField.irreducibleWord (Core.sourceFieldExponent (Core.sourceSizeParameter encodingLength formula))) operand steps) = BinaryFieldInverseAlgebra.sourceWordValue encodingLength formula operand ^ (steps + 1)

def GapCVP.GaussianSourceConsistencyBridge.binaryGaussianMalformedReducedState : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianSourceConsistencyBridge.binaryGaussianMalformedReducedState = GapCVP.GaussianPackedPivotColumnTM.binaryGaussianPackedPivotColumnWord [(true, true)] []

def GapCVP.GaussianSourceConsistencyBridge.binaryGaussianSourceConsistencyGuard (system : List Bool → Option Core.BinaryAffineSystem) (input : List Bool) : Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianSourceConsistencyBridge.binaryGaussianSourceConsistencyGuard system input = match system input with | none => false | some actual => actual.effectiveReducedConsistent

def GapCVP.GaussianSourceConsistencyBridge.binaryGaussianExpectedReducedSourceState (system : List Bool → Option Core.BinaryAffineSystem) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

structure GapCVP.GaussianSourceConsistencyBridge.BinaryGaussianExactSourceInitializer (system : List Bool → Option Core.BinaryAffineSystem) : Type 1

GapCVP reduction support.

• output : List Bool → List Bool

  GapCVP reduction support.

• computer : BitTM self.output

  GapCVP reduction support.

• output_eq (input : List Bool) : self.output input = binaryGaussianExpectedReducedSourceState system input

noncomputable def GapCVP.GaussianSourceConsistencyBridge.binaryGaussianExactSourceConsistencyComputable {system : List Bool → Option Core.BinaryAffineSystem} (initializer : BinaryGaussianExactSourceInitializer system) : BitTM fun (input : List Bool) => binaryGaussianSourceConsistencyGuard system input :: input

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedCheckBits (system : Core.BinaryAffineSystem) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedRhsBits (system : Core.BinaryAffineSystem) : List Bool

GapCVP reduction support.

Equations

• GapCVP.BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedRhsBits system = List.map (fun (row : Fin system.rowCount) => decide (system.rightHandSide row = 1)) (List.finRange system.rowCount)

def GapCVP.BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedQueryPreparation (queries : List (List Bool)) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedFlatMap_singleton {α : Type} (values : List α) (bit : α → Bool) : List.flatMap (fun (value : α) => [bit value]) values = List.map bit values

theorem GapCVP.GaussianAdaptivePackedTraceCorrectness.sourcePhysicalWordPackedCheckBits_eq_effective_initial (system : Core.BinaryAffineSystem) : BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedCheckBits system = GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedCheckBits (Core.EffectiveBinaryGaussian.initialState system.effectiveGaussianSystem)

theorem GapCVP.GaussianAdaptivePackedTraceCorrectness.sourcePhysicalWordPackedRhsBits_eq_effective_initial (system : Core.BinaryAffineSystem) : BinaryPhysicalWordPackedMatrixTM.sourcePhysicalWordPackedRhsBits system = GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedRhsBits (Core.EffectiveBinaryGaussian.initialState system.effectiveGaussianSystem)

def GapCVP.GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedPivotCatalogue {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateCheckBits : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateCheckBits = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateCheckBitsComputable : BitTM gaussianPackedStateCheckBits

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateCheckBitsComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateRhsBits : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateRhsBits = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateRhsBitsComputable : BitTM gaussianPackedStateRhsBits

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedInitialOriginalSource : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedInitialOriginalSource = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix

noncomputable def GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedInitialOriginalSourceComputable : BitTM gaussianPackedInitialOriginalSource

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateCheckBits_matrixWord (checks rhs source : List Bool) : gaussianPackedStateCheckBits (BinaryEncoding.lengthPrefixedWord checks ++ BinaryEncoding.lengthPrefixedWord rhs ++ source) = checks

theorem GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedStateRhsBits_matrixWord (checks rhs source : List Bool) : gaussianPackedStateRhsBits (BinaryEncoding.lengthPrefixedWord checks ++ BinaryEncoding.lengthPrefixedWord rhs ++ source) = rhs

theorem GapCVP.GaussianAdaptivePackedTraceCorrectness.gaussianPackedInitialOriginalSource_matrixWord (checks rhs source : List Bool) : gaussianPackedInitialOriginalSource (BinaryEncoding.lengthPrefixedWord checks ++ BinaryEncoding.lengthPrefixedWord rhs ++ source) = source

@[simp]

theorem GapCVP.GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedPivotCatalogue_initial {m n : ℕ} (system : Core.EffectiveBinaryGaussian.System m n) : effectiveGaussianPackedPivotCatalogue (Core.EffectiveBinaryGaussian.initialState system) = GaussianAdaptivePivotStepTM.binaryGaussianPivotBatchStream (List.replicate n [false])

def GapCVP.GaussianPhysicalWordReducedAtomTM.effectiveGaussianStateBasisTag {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (row column : Fin n) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianPackedStateTargetAtomTM.gaussianPackedIndexedStateWord (index : ℕ) (state : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianPackedStateTargetAtomTM.gaussianPackedIndexedStateWord index state = GapCVP.BinaryEncoding.lengthPrefixedWord (List.replicate index true) ++ state

def GapCVP.GaussianPackedStateTargetAtomTM.gaussianPackedIndexedTargetBit : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianPackedStateTargetAtomTM.gaussianPackedIndexedTargetBitComputable : BitTM gaussianPackedIndexedTargetBit

GapCVP reduction support.

Equations

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

def GapCVP.GaussianPackedStateTargetAtomTM.gaussianPackedIndexedTargetAtom : List Bool → List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianPackedStateTargetAtomTM.gaussianPackedIndexedTargetAtom_effective (system : Core.BinaryAffineSystem) (column : Fin system.dimension) (source : List Bool) : gaussianPackedIndexedTargetAtom (gaussianPackedIndexedStateWord (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord system.effectiveGaussianState source)) = BinaryEncoding.encodeAtomic ↑(system.effectiveAffineRepresentative column)

def GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateCheckLengthUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateRowCountUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateRowCountUnaryComputable : BitTM gaussianDenseStateRowCountUnary

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateDimensionDivisionQuery (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateDimensionUnary : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateDimensionUnaryComputable : BitTM gaussianDenseStateDimensionUnary

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalStateCellTM.effectiveGaussianPackedCheckBits_length {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) : (GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedCheckBits state).length = m * n

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalStateCellTM.effectiveGaussianPackedRhsBits_length {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) : (GaussianAdaptiveEliminationCorrectness.effectiveGaussianPackedRhsBits state).length = m

@[simp]

theorem GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateRowCountUnary_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) : gaussianDenseStateRowCountUnary (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source) = List.replicate m true

theorem GapCVP.GaussianAdaptivePhysicalStateCellTM.gaussianDenseStateDimensionUnary_effective {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (hrows : 0 < m) : gaussianDenseStateDimensionUnary (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source) = List.replicate n true

def GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStateCheckCellWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStateCheckCellComputable : BitTM gaussianPackedStateCheckCellWord

GapCVP reduction support.

Equations

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

def GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStateRhsCellWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStateRhsCellComputable : BitTM gaussianPackedStateRhsCellWord

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStateCheckCellWord_query {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row : Fin m) (column : Fin n) (hrows : 0 < m) : gaussianPackedStateCheckCellWord (BinaryExplicitAffineRows.affineCellQuery (↑row) (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = [decide (state.system.check row column = 1)]

theorem GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStateRhsCellWord_query {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (row : Fin m) (column : ℕ) : gaussianPackedStateRhsCellWord (BinaryExplicitAffineRows.affineCellQuery (↑row) column (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = [decide (state.system.rhs row = 1)]

def GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStatePivotCellWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStatePivotCellComputable : BitTM gaussianPackedStatePivotCellWord

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianAdaptivePackedStateLookupTM.gaussianPackedStatePivotCellWord_query {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (source : List Bool) (column : Fin n) : gaussianPackedStatePivotCellWord (BinaryExplicitAffineRows.affineCellQuery (↑column) 0 (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = GaussianAdaptiveEliminationCorrectness.effectiveGaussianStatePivotWord state column

def GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisStateWord (row column : ℕ) (state : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisStateWord row column state = GapCVP.BinaryExplicitAffineRows.affineCellQuery row column state

def GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisTag (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisTagComputable : BitTM gaussianPackedIndexedBasisTag

GapCVP reduction support.

Equations

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

def GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisAtom : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisAtomComputable : BitTM gaussianPackedIndexedBasisAtom

GapCVP reduction support.

Equations

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

theorem GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisTag_state {m n : ℕ} (state : Core.EffectiveBinaryGaussian.State m n) (row column : Fin n) (source : List Bool) : gaussianPackedIndexedBasisTag (gaussianPackedIndexedBasisStateWord (↑row) (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord state source)) = GaussianPhysicalWordReducedAtomTM.effectiveGaussianStateBasisTag state row column

theorem GapCVP.GaussianPackedStateBasisAtomTM.gaussianPackedIndexedBasisAtom_effective (system : Core.BinaryAffineSystem) (row column : Fin system.dimension) (source : List Bool) : gaussianPackedIndexedBasisAtom (gaussianPackedIndexedBasisStateWord (↑row) (↑column) (GaussianAdaptivePackedTraceCorrectness.effectiveGaussianPackedStateWord system.effectiveGaussianState source)) = BinaryEncoding.encodeAtomic (system.effectiveSquareBasisMatrix row column)

noncomputable def GapCVP.Factor400FinitePNormCorollary.finitePNorm (p : ℚ) {n : ℕ} (x : Fin n → ℝ) : ℝ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePNorm p x = (∑ i : Fin n, |x i| ^ ↑p) ^ (↑p)⁻¹

theorem GapCVP.Factor400FinitePNormCorollary.finitePNorm_nonneg (p : ℚ) {n : ℕ} (x : Fin n → ℝ) : 0 ≤ finitePNorm p x

theorem GapCVP.Factor400FinitePNormCorollary.finitePNorm_rpow (p : ℚ) (hp : 0 < p) {n : ℕ} (x : Fin n → ℝ) : finitePNorm p x ^ ↑p = ∑ i : Fin n, |x i| ^ ↑p

def GapCVP.Factor400FinitePNormCorollary.finitePLatticeDiscrepancy (I : GapCVPInstance) (z : Fin I.dimension → ℤ) : Fin I.dimension → ℝ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePLatticeDiscrepancy I z i = ↑(I.target i) - ∑ j : Fin I.dimension, ↑(I.basis i j) * ↑(z j)

noncomputable def GapCVP.Factor400FinitePNormCorollary.finitePLatticeDistance (p : ℚ) (I : GapCVPInstance) (z : Fin I.dimension → ℤ) : ℝ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePLatticeDistance p I z = GapCVP.Factor400FinitePNormCorollary.finitePNorm p (GapCVP.Factor400FinitePNormCorollary.finitePLatticeDiscrepancy I z)

noncomputable def GapCVP.Factor400FinitePNormCorollary.finitePGapFactor (p : ℚ) (I : GapCVPInstance) : ℝ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePGapFactor p I = ↑I.dimension ^ (200 * ↑p)⁻¹

def GapCVP.Factor400FinitePNormCorollary.finitePRadiusScale (p : ℚ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePRadiusScale p = ⌈4 * p⌉₊

theorem GapCVP.Factor400FinitePNormCorollary.finitePRadiusScale_pos (p : ℚ) (hp : 1 ≤ p) : 0 < finitePRadiusScale p

def GapCVP.Factor400FinitePNormCorollary.finitePRadiusNumerator (p : ℚ) (R : ℕ) : ℕ

GapCVP reduction support.

Equations

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

def GapCVP.Factor400FinitePNormCorollary.finitePRadius (p : ℚ) (R : ℕ) : ℚ

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePRadius p R = ↑(GapCVP.Factor400FinitePNormCorollary.finitePRadiusNumerator p R) / ↑(GapCVP.Factor400FinitePNormCorollary.finitePRadiusScale p)

def GapCVP.Factor400FinitePNormCorollary.finitePSignedBinarySupport {n : ℕ} (z : Fin n → ℤ) : Finset (Fin n)

GapCVP reduction support.

Equations

• GapCVP.Factor400FinitePNormCorollary.finitePSignedBinarySupport z = {i : Fin n | ↑(z i) ≠ 0}

theorem GapCVP.Factor400FinitePNormCorollary.finitePSignedBinarySupport_card_le_power_sum (p : ℚ) (hp : 1 ≤ p) {n : ℕ} (z : Fin n → ℤ) : ↑(finitePSignedBinarySupport z).card ≤ ∑ i : Fin n, |↑(z i)| ^ ↑p

noncomputable def GapCVP.Factor400FinitePNormCorollary.finitePGapCVPPromise (p : ℚ) (hp : 1 ≤ p) : PromiseProblem

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400FinitePRadiusArithmetic.finitePExponent_num_pos (p : ℚ) (hp : 1 ≤ p) : 0 < p.num.natAbs

theorem GapCVP.Factor400FinitePRadiusArithmetic.finitePExponent_cast (p : ℚ) (hp : 1 ≤ p) : ↑p = ↑p.num.natAbs / ↑p.den

theorem GapCVP.Factor400FinitePRadiusArithmetic.four_mul_le_finitePRadiusScale (p : ℚ) : 4 * ↑p ≤ ↑(Factor400FinitePNormCorollary.finitePRadiusScale p)

theorem GapCVP.Factor400FinitePRadiusArithmetic.finitePCeilingRoot_le_nthRoot_add_one (a value : ℕ) : GapCVP.Factor400FinitePNormCorollary.finitePCeilingRoot✝ a value ≤ a.nthRoot value + 1

theorem GapCVP.Factor400FinitePRadiusArithmetic.finitePRadiusNumerator_spec (p : ℚ) (hp : 1 ≤ p) (R : ℕ) : Factor400FinitePNormCorollary.finitePRadiusScale p ^ p.num.natAbs * R ^ p.den ≤ Factor400FinitePNormCorollary.finitePRadiusNumerator p R ^ p.num.natAbs

theorem GapCVP.Factor400FinitePRadiusArithmetic.finitePRadius_pos (p : ℚ) (hp : 1 ≤ p) (R : ℕ) (hR : 0 < R) : 0 < Factor400FinitePNormCorollary.finitePRadius p R

theorem GapCVP.Factor400FinitePRadiusArithmetic.finitePRadius_cast (p : ℚ) (R : ℕ) : ↑(Factor400FinitePNormCorollary.finitePRadius p R) = ↑(Factor400FinitePNormCorollary.finitePRadiusNumerator p R) / ↑(Factor400FinitePNormCorollary.finitePRadiusScale p)

def GapCVP.Factor400BinaryCodeDecodingCorollary.binaryWordLift {n : ℕ} (word : Fin n → ZMod 2) : Fin n → ℤ

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryCodeDecodingCorollary.binaryWordLift word index = ↑(word index).val

@[simp]

theorem GapCVP.Factor400BinaryCodeDecodingCorollary.binaryResidue_binaryWordLift {n : ℕ} (word : Fin n → ZMod 2) : Core.binaryResidue (binaryWordLift word) = word

noncomputable def GapCVP.Factor400BinaryCodeDecodingCorollary.sourceBinaryDecodingRadius (encodingLength : ℕ) (formula : Core.Formula) : ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400BinaryCodeDecodingCorollary.sourceBinaryDecodingRadius_pos (encodingLength : ℕ) (formula : Core.Formula) : 0 < sourceBinaryDecodingRadius encodingLength formula

noncomputable def GapCVP.Factor400BinaryCodeDecodingCorollary.binaryCodeGapFactor (blockLength : ℕ) : ℝ

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryCodeDecodingCorollary.binaryCodeGapFactor blockLength = ↑blockLength ^ (1 / 200)

theorem GapCVP.Factor400BinaryCodeDecodingCorollary.sourceBinaryDecoding_scaledNorm_support (encodingLength : ℕ) (formula : Core.Formula) (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) → ℤ) (hshort : ↑(Core.integerSquaredNorm vector) ≤ 2 * binaryCodeGapFactor (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength formula) * ↑(sourceBinaryDecodingRadius encodingLength formula)) : 10 * Core.integerSquaredNorm vector ≤ Fintype.card (Factor400BinaryConstructiveSourcePlaces.sourceFormulaField encodingLength formula) * Core.sourceSizeParameter encodingLength formula ^ 4

def GapCVP.Factor400FinitePRadiusSourceTM.finitePNthRootUnaryOutput (a : ℕ) (target : 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.Factor400FinitePRadiusSourceTM.finitePNthRootUnaryComputable (a : ℕ) {target : List Bool → List Bool} (computer : BitTM target) : BitTM (finitePNthRootUnaryOutput a target)

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400FinitePRadiusSourceTM.finitePNthRootUnaryOutput_valid (a : ℕ) (ha : 0 < a) (target : List Bool → List Bool) (input : List Bool) (value : ℕ) (hvalue : target input = List.replicate value true) : finitePNthRootUnaryOutput a target input = List.replicate (GapCVP.Factor400FinitePNormCorollary.finitePCeilingRoot✝ a value) true

def GapCVP.Factor400FinitePRadiusRationalAtomTM.sourceReducedRationalAtomicOutput (scale : ℕ) (numerator : 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.Factor400FinitePRadiusRationalAtomTM.sourceReducedRationalAtomicComputable (scale : ℕ) {numerator : List Bool → List Bool} (computer : BitTM numerator) : BitTM (sourceReducedRationalAtomicOutput scale numerator)

GapCVP reduction support.

Equations

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

theorem GapCVP.Factor400FinitePRadiusRationalAtomTM.sourceReducedRationalAtomicOutput_valid (scale : ℕ) (numerator : List Bool → List Bool) (input : List Bool) (value : ℕ) (hscale : 0 < scale) (hvalue : numerator input = List.replicate value true) : sourceReducedRationalAtomicOutput scale numerator input = BinaryEncoding.encodeAtomic (↑value / ↑scale)

def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankReducedState (reduced : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankReducedState reduced = reduced ∘ GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSource

noncomputable def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankReducedStateComputable {reduced : List Bool → List Bool} (computer : BitTM reduced) : BitTM (compactPhysicalGaussianRankReducedState reduced)

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankTargetStateQuery (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.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankTargetStateQueryComputable {reduced : List Bool → List Bool} (computer : BitTM reduced) : BitTM (compactPhysicalGaussianRankTargetStateQuery reduced)

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankTargetAtom (reduced : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankTargetAtomComputable {reduced : List Bool → List Bool} (computer : BitTM reduced) : BitTM (compactPhysicalGaussianRankTargetAtom reduced)

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankRadiusAtom (radius : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankRadiusAtom radius = radius ∘ GapCVP.BinaryGaussianStructuralAtomTM.structuralRankOriginalSource

noncomputable def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianRankRadiusAtomComputable {radius : List Bool → List Bool} (computer : BitTM radius) : BitTM (compactPhysicalGaussianRankRadiusAtom radius)

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianStructuralAtomComputerPack (output : List Bool → List Bool) (computer : BitTM output) : BinaryStructuralRecordTM.ConstructiveStructuralAtomComputer

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianStructuralAtomComputerPack output computer = { output := output, computer := computer }

@[simp]

theorem GapCVP.Factor400BinaryCompactPhysicalGaussianOutputSerializerTM.compactPhysicalGaussianStructuralAtomComputerPack_output (output : List Bool → List Bool) (computer : BitTM output) (input : List Bool) : (compactPhysicalGaussianStructuralAtomComputerPack output computer).output input = output input

noncomputable def GapCVP.OriginalThreeSATNPHardness.paperOriginalThreeSATLanguage (bits : List Bool) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.OriginalThreeSATNPHardness.paperOriginalThreeSATLanguage_iff (bits : List Bool) : paperOriginalThreeSATLanguage bits = true ↔ ∃ (formula : ThreeCNF), BinaryEncoding.encodeThreeCNF formula = bits ∧ ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true

theorem GapCVP.OriginalThreeSATNPHardness.paperOriginalThreeSATIsNPHard : NPHard paperOriginalThreeSATLanguage = true

def GapCVP.BinarySourceTautologyNormalizationExact.sourceClauseIsTautology (clause : ThreeClause) : Bool

GapCVP reduction support.

Equations

• GapCVP.BinarySourceTautologyNormalizationExact.sourceClauseIsTautology clause = decide (∃ (left : Fin 3) (right : Fin 3), (clause left).1 = (clause right).1 ∧ (clause left).2 ≠ (clause right).2)

theorem GapCVP.BinarySourceTautologyNormalizationExact.sourceClauseIsTautology_iff (clause : ThreeClause) : sourceClauseIsTautology clause = true ↔ ∃ (left : Fin 3) (right : Fin 3), (clause left).1 = (clause right).1 ∧ (clause left).2 ≠ (clause right).2

def GapCVP.BinarySourceTautologyNormalizationExact.noTautClauses (formula : ThreeCNF) : ThreeCNF

GapCVP reduction support.

Equations

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

theorem GapCVP.BinarySourceTautologyNormalizationExact.mem_sourceClausesWithoutTautologies (formula : ThreeCNF) (clause : ThreeClause) : clause ∈ noTautClauses formula ↔ clause ∈ formula ∧ sourceClauseIsTautology clause = false

def GapCVP.SourcePreprocessingSemantics.paperSourceClauseLiterals (clause : ThreeClause) : List Literal

GapCVP reduction support.

Equations

• GapCVP.SourcePreprocessingSemantics.paperSourceClauseLiterals clause = [clause 0, clause 1, clause 2]

def GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClause (clause : ThreeClause) : List Literal

GapCVP reduction support.

Equations

• GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClause clause = (GapCVP.SourcePreprocessingSemantics.paperSourceClauseLiterals clause).eraseDups

def GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClauses (formula : ThreeCNF) : List (List Literal)

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClauseRecord (clause : ThreeClause) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClauseStream (formula : ThreeCNF) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedVariables (formula : ThreeCNF) : List ℕ

GapCVP reduction support.

Equations

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

def GapCVP.SourcePreprocessingSemantics.paperNormalizedOccurringVariables (formula : ThreeCNF) : List ℕ

GapCVP reduction support.

Equations

• GapCVP.SourcePreprocessingSemantics.paperNormalizedOccurringVariables formula = (GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedVariables formula).eraseDups

theorem GapCVP.SourcePreprocessingSemantics.paperNormalizedClause_length_le_three (clause : ThreeClause) : (paperSourceNormalizedClause clause).length ≤ 3

theorem GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClause_ne_nil (clause : ThreeClause) : paperSourceNormalizedClause clause ≠ []

theorem GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClause_nodup (clause : ThreeClause) : (paperSourceNormalizedClause clause).Nodup

theorem GapCVP.SourcePreprocessingSemantics.mem_paperSourceNormalizedClause_iff (clause : ThreeClause) (literal : Literal) : literal ∈ paperSourceNormalizedClause clause ↔ ∃ (index : Fin 3), clause index = literal

theorem GapCVP.SourcePreprocessingSemantics.mem_paperSourceNormalizedClauses_iff (formula : ThreeCNF) (normalized : List Literal) : normalized ∈ paperSourceNormalizedClauses formula ↔ ∃ clause ∈ BinarySourceTautologyNormalizationExact.noTautClauses formula, paperSourceNormalizedClause clause = normalized

theorem GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedClauses_satisfied_iff (formula : ThreeCNF) (assignment : ℕ → Bool) : (∀ clause ∈ paperSourceNormalizedClauses formula, ∃ literal ∈ clause, literalSatisfied assignment literal = true) ↔ ∀ clause ∈ formula, clauseSatisfied assignment clause = true

theorem GapCVP.SourcePreprocessingSemantics.mem_paperSourceNormalizedOccurringVariables_iff (formula : ThreeCNF) (name : ℕ) : name ∈ paperNormalizedOccurringVariables formula ↔ ∃ clause ∈ BinarySourceTautologyNormalizationExact.noTautClauses formula, ∃ (index : Fin 3), (clause index).1 = name

theorem GapCVP.SourcePreprocessingSemantics.paperSourceNormalizedOccurringVariables_nodup (formula : ThreeCNF) : (paperNormalizedOccurringVariables formula).Nodup

def GapCVP.FormulaBridge.paperVariableArityVariableCount (formula : ThreeCNF) : ℕ

GapCVP reduction support.

Equations

• GapCVP.FormulaBridge.paperVariableArityVariableCount formula = (GapCVP.SourcePreprocessingSemantics.paperNormalizedOccurringVariables formula).length

def GapCVP.FormulaBridge.paperVariableArityVariableRank (formula : ThreeCNF) (name : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.FormulaBridge.paperVariableArityVariableRank formula name = List.idxOf name (GapCVP.SourcePreprocessingSemantics.paperNormalizedOccurringVariables formula)

theorem GapCVP.FormulaBridge.paperVariableArityVariableRank_lt (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) (literal : Literal) (hliteral : literal ∈ clause) : paperVariableArityVariableRank formula literal.1 < paperVariableArityVariableCount formula

def GapCVP.FormulaBridge.paperVariableAritySourceLiteral (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) (literal : Literal) (hliteral : literal ∈ clause) : Core.Literal (paperVariableArityVariableCount formula)

GapCVP reduction support.

Equations

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

theorem GapCVP.FormulaBridge.paper_retainedClause_length_le_three (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) : clause.length ≤ 3

def GapCVP.FormulaBridge.paperVariableAritySourceClause (formula : ThreeCNF) (clause : List Literal) (hclause : clause ∈ SourcePreprocessingSemantics.paperSourceNormalizedClauses formula) : Core.Clause (paperVariableArityVariableCount formula)

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.FormulaBridge.srcFormula (formula : ThreeCNF) : Core.Formula

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.FormulaBridge.paperVariableAritySourceFormula_variableCount (formula : ThreeCNF) : (srcFormula formula).variableCount = paperVariableArityVariableCount formula

theorem GapCVP.FormulaBridge.paperVariableAritySourceFormula_clauses_length (formula : ThreeCNF) : (srcFormula formula).clauses.length = List.length (BinarySourceTautologyNormalizationExact.noTautClauses formula)

theorem GapCVP.FormulaBridge.sourceFormula_satisfiable_iff (formula : ThreeCNF) : (srcFormula formula).Satisfiable = true ↔ ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true

@[reducible, inline]

noncomputable abbrev GapCVP.FormulaBridge.paperExplicitBinarySystem (encodingLength : ℕ) (formula : ThreeCNF) : Core.BinaryAffineSystem

GapCVP reduction support.

Equations

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

theorem GapCVP.FormulaBridge.paperVariableArityExplicitBinarySystem_signedSolution_of_satisfiable (encodingLength : ℕ) (formula : ThreeCNF) (hsatisfiable : ∃ (assignment : ℕ → Bool), ∀ clause ∈ formula, clauseSatisfied assignment clause = true) : ∃ (vector : Fin (Factor400BinaryConstructiveSourcePlaces.sourceFormulaDimension encodingLength (srcFormula formula)) → ℤ), (paperExplicitBinarySystem encodingLength formula).Solves vector = true ∧ ↑(Core.integerSquaredNorm vector) ≤ ↑(Core.sourceOneHotCompletenessRadius (srcFormula formula) (Factor400BinaryConstructiveSourcePlaces.sourceFormulaGrid encodingLength (srcFormula formula))) ^ 2

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.binaryField_zero_or_one (value : ZMod 2) : value = 0 ∨ value = 1

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.integerSquaredNorm_binaryWordLift {n : ℕ} (word : Fin n → ZMod 2) : Core.integerSquaredNorm (Factor400BinaryCodeDecodingCorollary.binaryWordLift word) = hammingNorm word

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.sourceOneHotSignedTable_zero_or_one {K : Type u_1} [Field K] [Fintype K] [DecidableEq K] (formula : Core.Formula) (points : Finset K) (assignment : Fin formula.variableCount → Bool) (hsatisfies : formula.Satisfied assignment = true) (interpolant : Polynomial K) (index : Fin (Core.sourceSATTableDimension formula K points)) : Core.sourceOneHotSignedTable formula points assignment hsatisfies interpolant index = 0 ∨ Core.sourceOneHotSignedTable formula points assignment hsatisfies interpolant index = 1

structure GapCVP.Factor400BinaryDecodingPromiseReduction.BinaryNearestCodewordInstance : Type

GapCVP reduction support.

• blockLength : ℕ

  GapCVP reduction support.

• generatorRank : ℕ

  GapCVP reduction support.

• generator : Fin self.blockLength → Fin self.generatorRank → ZMod 2

  GapCVP reduction support.

• target : Fin self.blockLength → ZMod 2

  GapCVP reduction support.

• radius : ℕ

  GapCVP reduction support.

structure GapCVP.Factor400BinaryDecodingPromiseReduction.BinarySyndromeDecodingInstance : Type

GapCVP reduction support.

• checkCount : ℕ

  GapCVP reduction support.

• blockLength : ℕ

  GapCVP reduction support.

• parityCheck : Fin self.checkCount → Fin self.blockLength → ZMod 2

  GapCVP reduction support.

• syndrome : Fin self.checkCount → ZMod 2

  GapCVP reduction support.

• radius : ℕ

  GapCVP reduction support.

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.binaryIntegerLift_zero : ↑(ZMod.val 0) = 0

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.binaryIntegerLift_one : ↑(ZMod.val 1) = 1

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.binaryIntegerLift_two : ↑(ZMod.val 2) = 0

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.binaryIntegerLift_intCast_of_zero_or_one {value : ℤ} (hvalue : value = 0 ∨ value = 1) : ↑(↑value).val = value

def GapCVP.Factor400BinaryDecodingPromiseReduction.encodeBinaryNearestCodewordInstance (record : BinaryNearestCodewordInstance) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryDecodingPromiseReduction.encodeBinarySyndromeDecodingInstance (record : BinarySyndromeDecodingInstance) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryDecodingPromiseReduction.decodeBinaryNearestCodewordInstance (bits : List Bool) : Option BinaryNearestCodewordInstance

GapCVP reduction support.

Equations

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

def GapCVP.Factor400BinaryDecodingPromiseReduction.decodeBinarySyndromeDecodingInstance (bits : List Bool) : Option BinarySyndromeDecodingInstance

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.decodeBinaryNearestCodewordInstance_encode (record : BinaryNearestCodewordInstance) : decodeBinaryNearestCodewordInstance (encodeBinaryNearestCodewordInstance record) = some record

@[simp]

theorem GapCVP.Factor400BinaryDecodingPromiseReduction.decodeBinarySyndromeDecodingInstance_encode (record : BinarySyndromeDecodingInstance) : decodeBinarySyndromeDecodingInstance (encodeBinarySyndromeDecodingInstance record) = some record

def GapCVP.Factor400BinaryDecodingPromiseReduction.binaryNearestCodeword (record : BinaryNearestCodewordInstance) (coefficients : Fin record.generatorRank → ZMod 2) : Fin record.blockLength → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryDecodingPromiseReduction.binaryNearestCodeword record coefficients index = ∑ column : Fin record.generatorRank, record.generator index column * coefficients column

def GapCVP.Factor400BinaryDecodingPromiseReduction.binaryNearestTarget (record : BinaryNearestCodewordInstance) : Fin record.blockLength → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryDecodingPromiseReduction.binaryNearestTarget record = record.target

def GapCVP.Factor400BinaryDecodingPromiseReduction.binarySyndromeProduct (record : BinarySyndromeDecodingInstance) (word : Fin record.blockLength → ZMod 2) : Fin record.checkCount → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryDecodingPromiseReduction.binarySyndromeProduct record word row = ∑ column : Fin record.blockLength, record.parityCheck row column * word column

def GapCVP.Factor400BinaryDecodingPromiseReduction.binarySyndromeTarget (record : BinarySyndromeDecodingInstance) : Fin record.checkCount → ZMod 2

GapCVP reduction support.

Equations

• GapCVP.Factor400BinaryDecodingPromiseReduction.binarySyndromeTarget record = record.syndrome