Local Gram certificates for the weighted six-point score

The weighted pair score at the small rational weights 1/12 and 13/14 is a positive combination of six norms minus two radial penalties. Replacing each norm by a quadratic tangent, each radial penalty by a secant on a radius box, and adding two nonnegative separation multipliers turns the score into a quadratic form in the five configuration vectors. A rank-three rational factor, completed by elementary two-vector squares, dominates that form, so the score is bounded by an explicit rational number depending only on the certificate.

@[reducible, inline]

abbrev LeanPool.Besicovitch.Five : Type

Indices of the five vectors in a six-point Gram certificate.

Equations

• LeanPool.Besicovitch.Five = Fin 5

@[reducible, inline]

abbrev LeanPool.Besicovitch.Three : Type

Indices of the three rows in the rational Gram factor.

Equations

• LeanPool.Besicovitch.Three = Fin 3

noncomputable def LeanPool.Besicovitch.gramLambda : ℝ

The small rational weight on the coincident-endpoint slack.

Equations

• LeanPool.Besicovitch.gramLambda = 1 / 12

noncomputable def LeanPool.Besicovitch.gramMu : ℝ

The small rational weight on the balanced root--edge slack.

Equations

• LeanPool.Besicovitch.gramMu = 13 / 14

theorem LeanPool.Besicovitch.gramLambda_pos : 0 < gramLambda

theorem LeanPool.Besicovitch.gramMu_pos : 0 < gramMu

noncomputable def LeanPool.Besicovitch.gramFirstPenalty : ℝ

Half the first-child radial penalty at the small rational weights.

Equations

• LeanPool.Besicovitch.gramFirstPenalty = LeanPool.Besicovitch.weightedFirstPenalty LeanPool.Besicovitch.barC LeanPool.Besicovitch.gramLambda LeanPool.Besicovitch.gramMu / 2

noncomputable def LeanPool.Besicovitch.gramSecondPenalty : ℝ

Half the second-child radial penalty at the small rational weights.

Equations

• LeanPool.Besicovitch.gramSecondPenalty = LeanPool.Besicovitch.weightedSecondPenalty LeanPool.Besicovitch.barC LeanPool.Besicovitch.gramLambda LeanPool.Besicovitch.gramMu / 2

theorem LeanPool.Besicovitch.gramFirstPenalty_pos : 0 < gramFirstPenalty

theorem LeanPool.Besicovitch.gramSecondPenalty_pos : 0 < gramSecondPenalty

structure LeanPool.Besicovitch.GramCertificate : Type

A local certificate on one rectangle of second-child radii.

• pLower : ℚ

  Lower bound for the second red radius.

• pUpper : ℚ

  Upper bound for the second red radius.

• wLower : ℚ

  Lower bound for the second blue radius.

• wUpper : ℚ

  Upper bound for the second blue radius.

• alpha₀ : ℚ

  Tangent parameter for e - p₁ - w₁.

• alpha₁ : ℚ

  Tangent parameter for e - p₂ - w₂.

• alpha₂ : ℚ

  Tangent parameter for e - p₁.

• alpha₃ : ℚ

  Tangent parameter for e - w₁.

• alpha₄ : ℚ

  Tangent parameter for e - p₁ - w₂.

• alpha₅ : ℚ

  Tangent parameter for e - w₁ - p₂.

• etaP : ℚ

  Multiplier for the red separation constraint.

• etaW : ℚ

  Multiplier for the blue separation constraint.

• factor : Fin 3 → Fin 5 → ℚ

  The rank-three rational Gram factor.

def LeanPool.Besicovitch.tenThousandthFactor (entries : Fin 3 → Fin 5 → ℤ) : Fin 3 → Fin 5 → ℚ

Scale a table of integers by 10⁻⁴.

Equations

• LeanPool.Besicovitch.tenThousandthFactor entries i j = ↑(entries i j) / 10000

def LeanPool.Besicovitch.factorRow (certificate : GramCertificate) (k : Three) : Five → ℝ

One rational Gram-factor row, cast to real coordinates.

Equations

• LeanPool.Besicovitch.factorRow certificate k i = ↑(certificate.factor k i)

def LeanPool.Besicovitch.factorGram (certificate : GramCertificate) : Matrix Five Five ℝ

The positive semidefinite Gram matrix represented by the three factor rows.

Equations

• LeanPool.Besicovitch.factorGram certificate = ∑ k : LeanPool.Besicovitch.Three, Matrix.vecMulVec (LeanPool.Besicovitch.factorRow certificate k) (LeanPool.Besicovitch.factorRow certificate k)

def LeanPool.Besicovitch.targetOffDiagonal (certificate : GramCertificate) : Matrix Five Five ℝ

The negated off-diagonal coefficients of the quadratic form.

Equations

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

def LeanPool.Besicovitch.residual (certificate : GramCertificate) (i j : Five) : ℝ

The discrepancy between the target quadratic form and its rational Gram factor.

Equations

• LeanPool.Besicovitch.residual certificate i j = LeanPool.Besicovitch.targetOffDiagonal certificate i j - LeanPool.Besicovitch.factorGram certificate i j

def LeanPool.Besicovitch.diagonal₀ (certificate : GramCertificate) : ℝ

Diagonal entry 0 after adding the rank-one residual corrections.

Equations

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

def LeanPool.Besicovitch.diagonal₁ (certificate : GramCertificate) : ℝ

Diagonal entry 1 after adding the rank-one residual corrections.

Equations

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

def LeanPool.Besicovitch.diagonal₂ (certificate : GramCertificate) : ℝ

Diagonal entry 2 after adding the rank-one residual corrections.

Equations

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

def LeanPool.Besicovitch.diagonal₃ (certificate : GramCertificate) : ℝ

Diagonal entry 3 after adding the rank-one residual corrections.

Equations

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

def LeanPool.Besicovitch.diagonal₄ (certificate : GramCertificate) : ℝ

Diagonal entry 4 after adding the rank-one residual corrections.

Equations

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

noncomputable def LeanPool.Besicovitch.redFirstLower (certificate : GramCertificate) : ℝ

The lower bound the separation forces on the first red radius.

Equations

• LeanPool.Besicovitch.redFirstLower certificate = LeanPool.Besicovitch.barC - ↑certificate.pUpper

noncomputable def LeanPool.Besicovitch.blueFirstLower (certificate : GramCertificate) : ℝ

The lower bound the separation forces on the first blue radius.

Equations

• LeanPool.Besicovitch.blueFirstLower certificate = LeanPool.Besicovitch.barC - ↑certificate.wUpper

def LeanPool.Besicovitch.balance₀ (certificate : GramCertificate) : ℝ

The balance of the root vector.

Equations

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

noncomputable def LeanPool.Besicovitch.balance₁ (certificate : GramCertificate) : ℝ

The balance of the first red vector.

Equations

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

noncomputable def LeanPool.Besicovitch.balance₂ (certificate : GramCertificate) : ℝ

The balance of the second red vector.

Equations

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

noncomputable def LeanPool.Besicovitch.balance₃ (certificate : GramCertificate) : ℝ

The balance of the first blue vector.

Equations

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

noncomputable def LeanPool.Besicovitch.balance₄ (certificate : GramCertificate) : ℝ

The balance of the second blue vector.

Equations

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

noncomputable def LeanPool.Besicovitch.dualRadialBound (certificate : GramCertificate) : ℝ

The radius-box maximum of the diagonal form after the Gram corrections.

Equations

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

noncomputable def LeanPool.Besicovitch.GramCertificate.upperBound (certificate : GramCertificate) : ℝ

The exact rational upper bound the certificate proves for the weighted score.

Equations

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

def LeanPool.Besicovitch.GramCertificate.Valid (certificate : GramCertificate) : Prop

The arithmetic conditions making a certificate usable.

Equations

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

theorem LeanPool.Besicovitch.weightedPairScore_le_of_gramCertificate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (certificate : GramCertificate) (hvalid : certificate.Valid) (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) (hpLower : ↑certificate.pLower ≤ ‖p₂‖) (hpUpper : ‖p₂‖ ≤ ↑certificate.pUpper) (hwLower : ↑certificate.wLower ≤ ‖w₂‖) (hwUpper : ‖w₂‖ ≤ ↑certificate.wUpper) : weightedPairScore e barC gramLambda gramMu p₁ p₂ w₁ w₂ ≤ -(1 / 2000)

A valid certificate bounds the weighted pair score on its radius rectangle.