Documentation

LeanPool.Besicovitch.SixPoint.WeightedFailure

The three active six-point failure slacks #

The surviving path through the packing failure tree produces three scalar inequalities. This file names those natural slacks and identifies their positive weighted sum with the coordinate-free weighted pair score.

source
noncomputable def LeanPool.Besicovitch.firstActiveFailureSlack (configuration : SixPointConfiguration) :
ℝ

The weakened diagonal-matching slack q1.

Equations
Instances For
    source
    noncomputable def LeanPool.Besicovitch.secondActiveFailureSlack (configuration : SixPointConfiguration) :
    ℝ

    The coincident sibling-endpoint slack q2.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def LeanPool.Besicovitch.thirdActiveFailureSlack (configuration : SixPointConfiguration) :
      ℝ

      The balanced root--edge slack q3.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem LeanPool.Besicovitch.firstActiveFailureSlack_nonneg {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
        0 ≤ firstActiveFailureSlack configuration

        The selected diagonal matching makes q1 nonnegative.

        source
        theorem LeanPool.Besicovitch.secondActiveFailureSlack_pos {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hred : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) (hblue : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0)) :
        0 < secondActiveFailureSlack configuration

        Coincident endpoint failures at B11 make q2 strictly positive.

        source
        theorem LeanPool.Besicovitch.thirdActiveFailureSlack_pos {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hred : 2 * redRootEdgeTarget configuration < dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) + redRootBlueTriangleReach configuration SixPointLabel.left + redChildBlueTriangleReach configuration SixPointLabel.right SixPointLabel.left) (hblue : 2 * blueRootEdgeTarget configuration < dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) + blueRootRedTriangleReach configuration SixPointLabel.left + blueChildRedTriangleReach configuration SixPointLabel.right SixPointLabel.left) :
        0 < thirdActiveFailureSlack configuration

        The two surviving (1,1) root--edge terms make q3 strictly positive.

        source
        theorem LeanPool.Besicovitch.weightedPairScore_configuration_eq_activeFailureCombination (configuration : SixPointConfiguration) (lambda mu : ℝ) :
        weightedPairScore configuration.rootDisplacement barC lambda mu (configuration.redDisplacement SixPointLabel.left) (configuration.redDisplacement SixPointLabel.right) (configuration.bluePullback SixPointLabel.left) (configuration.bluePullback SixPointLabel.right) = firstActiveFailureSlack configuration + lambda * secondActiveFailureSlack configuration + mu * thirdActiveFailureSlack configuration

        The weighted score of the displacement pairs is exactly q1 + lambda*q2 + mu*q3.

        source
        theorem LeanPool.Besicovitch.activeFailureCombination_nonneg {configuration : SixPointConfiguration} {lambda mu : ℝ} (hlambda : 0 ≤ lambda) (hmu : 0 ≤ mu) (hq₁ : 0 ≤ firstActiveFailureSlack configuration) (hq₂ : 0 ≤ secondActiveFailureSlack configuration) (hq₃ : 0 ≤ thirdActiveFailureSlack configuration) :
        0 ≤ firstActiveFailureSlack configuration + lambda * secondActiveFailureSlack configuration + mu * thirdActiveFailureSlack configuration

        Nonnegative active slacks make their exact weighted combination nonnegative.

        source
        theorem LeanPool.Besicovitch.activeFailureCombination_pos {configuration : SixPointConfiguration} {lambda mu : ℝ} (hlambda : 0 < lambda) (hmu : 0 < mu) (hq₁ : 0 ≤ firstActiveFailureSlack configuration) (hq₂ : 0 < secondActiveFailureSlack configuration) (hq₃ : 0 < thirdActiveFailureSlack configuration) :
        0 < firstActiveFailureSlack configuration + lambda * secondActiveFailureSlack configuration + mu * thirdActiveFailureSlack configuration

        Strict second and third failure slacks make their weighted combination positive.