Documentation

LeanPool.Besicovitch.SixPoint.SiblingIncidenceLedger

Geometric sibling-incidence exclusions #

This file connects the exact rational tangent certificates to the endpoint and balanced failure witnesses. The only remaining analytic inputs are the five named lens inequalities.

source
def LeanPool.Besicovitch.swapChildLabel :
SixPointLabel → SixPointLabel

Swap the two child labels while fixing the root.

Equations
Instances For
    source
    def LeanPool.Besicovitch.swapConfigurationChildren (configuration : SixPointConfiguration) :
    SixPointConfiguration

    Simultaneously swap the two children of both colors.

    Equations
    Instances For
      source
      def LeanPool.Besicovitch.transposeConfigurationColors (configuration : SixPointConfiguration) :
      SixPointConfiguration

      Interchange the red and blue colors.

      Equations
      Instances For
        source
        theorem LeanPool.Besicovitch.IsAdmissibleAt.swapChildren {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) :
        (swapConfigurationChildren configuration).IsAdmissibleAt s

        Simultaneous child swap preserves endpoint admissibility.

        source
        theorem LeanPool.Besicovitch.IsAdmissibleAt.transposeColors {configuration : SixPointConfiguration} {s : ℝ} (h : configuration.IsAdmissibleAt s) :
        (transposeConfigurationColors configuration).IsAdmissibleAt s

        Color transposition preserves endpoint admissibility.

        source
        noncomputable def LeanPool.Besicovitch.incidenceCrossDistance (configuration : SixPointConfiguration) (redChild blueChild : Fin 2) :
        ℝ

        The distance between a chosen red child and a chosen blue child.

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

          The root-to-child radius at a chosen color and child.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem LeanPool.Besicovitch.incidenceChildRadius_red_eq_norm (configuration : SixPointConfiguration) (child : Fin 2) :
            incidenceChildRadius configuration SixPointColor.red child = ‖configuration.redDisplacement (incidenceChild child)‖

            A child radius is the norm of its red displacement vector.

            source
            theorem LeanPool.Besicovitch.incidenceChildRadius_blue_eq_norm (configuration : SixPointConfiguration) (child : Fin 2) :
            incidenceChildRadius configuration SixPointColor.blue child = ‖configuration.bluePullback (incidenceChild child)‖

            A child radius is the norm of its pulled-back blue displacement vector.

            source
            theorem LeanPool.Besicovitch.incidenceCrossDistance_eq_norm (configuration : SixPointConfiguration) (redChild blueChild : Fin 2) :
            incidenceCrossDistance configuration redChild blueChild = ‖configuration.rootDisplacement - configuration.redDisplacement (incidenceChild redChild) - configuration.bluePullback (incidenceChild blueChild)‖

            A cross distance is the norm of its endpoint-geometry displacement.

            source
            noncomputable def LeanPool.Besicovitch.balancedIncidencePenalty (code : Fin 4) (firstRadius secondRadius : ℝ) :
            ℝ

            The radial penalty in a reduced balanced incidence slack.

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

              The reduced matching slack retained from the four-child branch.

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

                The selected diagonal matching alternative from the four-child minimax.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem LeanPool.Besicovitch.selectedDiagonalMatchingFails_swapChildren (configuration : SixPointConfiguration) :
                  SelectedDiagonalMatchingFails (swapConfigurationChildren configuration) ↔ SelectedDiagonalMatchingFails configuration

                  The selected diagonal matching is unchanged by simultaneous child swap.

                  source
                  theorem LeanPool.Besicovitch.selectedDiagonalMatchingFails_transposeColors (configuration : SixPointConfiguration) :
                  SelectedDiagonalMatchingFails (transposeConfigurationColors configuration) ↔ SelectedDiagonalMatchingFails configuration

                  The selected diagonal matching is unchanged by color transposition.

                  source
                  theorem LeanPool.Besicovitch.redEndpointFailure_swapChildren (configuration : SixPointConfiguration) (code : Fin 4) :
                  redSiblingTriangleFailure (swapConfigurationChildren configuration) (SiblingTriangleWitness.endpoint (swapEndpointCode code)) ↔ redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)

                  Red endpoint failures respect simultaneous child swap.

                  source
                  theorem LeanPool.Besicovitch.blueEndpointFailure_swapChildren (configuration : SixPointConfiguration) (code : Fin 4) :
                  blueSiblingTriangleFailure (swapConfigurationChildren configuration) (SiblingTriangleWitness.endpoint (swapEndpointCode code)) ↔ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)

                  Blue endpoint failures respect simultaneous child swap.

                  source
                  theorem LeanPool.Besicovitch.redBalancedFailure_swapChildren (configuration : SixPointConfiguration) (code : Fin 4) :
                  redSiblingTriangleFailure (swapConfigurationChildren configuration) (SiblingTriangleWitness.balanced (swapBalancedCode code)) ↔ redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced code)

                  Red balanced failures respect simultaneous child swap.

                  source
                  theorem LeanPool.Besicovitch.blueBalancedFailure_swapChildren (configuration : SixPointConfiguration) (code : Fin 4) :
                  blueSiblingTriangleFailure (swapConfigurationChildren configuration) (SiblingTriangleWitness.balanced (swapBalancedCode code)) ↔ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced code)

                  Blue balanced failures respect simultaneous child swap.

                  source
                  theorem LeanPool.Besicovitch.redEndpointFailure_transposeColors (configuration : SixPointConfiguration) (code : Fin 4) :
                  redSiblingTriangleFailure (transposeConfigurationColors configuration) (SiblingTriangleWitness.endpoint (transposeEndpointCode code)) ↔ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)

                  Red endpoint failures become blue endpoint failures under color transposition.

                  source
                  theorem LeanPool.Besicovitch.blueEndpointFailure_transposeColors (configuration : SixPointConfiguration) (code : Fin 4) :
                  blueSiblingTriangleFailure (transposeConfigurationColors configuration) (SiblingTriangleWitness.endpoint (transposeEndpointCode code)) ↔ redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)

                  Blue endpoint failures become red endpoint failures under color transposition.

                  source
                  theorem LeanPool.Besicovitch.redBalancedFailure_transposeColors (configuration : SixPointConfiguration) (code : Fin 4) :
                  redSiblingTriangleFailure (transposeConfigurationColors configuration) (SiblingTriangleWitness.balanced code) ↔ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced code)

                  Red balanced failures become blue balanced failures under color transposition.

                  source
                  theorem LeanPool.Besicovitch.blueBalancedFailure_transposeColors (configuration : SixPointConfiguration) (code : Fin 4) :
                  blueSiblingTriangleFailure (transposeConfigurationColors configuration) (SiblingTriangleWitness.balanced code) ↔ redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced code)

                  Blue balanced failures become red balanced failures under color transposition.

                  source
                  noncomputable def LeanPool.Besicovitch.redEndpointReducedSlack (configuration : SixPointConfiguration) (code : Fin 4) :
                  ℝ

                  The reduced upper slack for a red endpoint incidence.

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

                    The reduced upper slack for a blue endpoint incidence.

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

                      The reduced upper slack for a red balanced incidence.

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

                        The reduced upper slack for a blue balanced incidence.

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

                          The selected matching alternative makes its reduced slack nonnegative.

                          source
                          theorem LeanPool.Besicovitch.redEndpointReducedSlack_pos {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (code : Fin 4) (hfailure : redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)) :
                          0 < redEndpointReducedSlack configuration code

                          A red endpoint failure makes the corresponding reduced endpoint slack positive.

                          source
                          theorem LeanPool.Besicovitch.blueEndpointReducedSlack_pos {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (code : Fin 4) (hfailure : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint code)) :
                          0 < blueEndpointReducedSlack configuration code

                          A blue endpoint failure makes the corresponding reduced endpoint slack positive.

                          source
                          theorem LeanPool.Besicovitch.redBalancedReducedSlack_pos {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (code : Fin 4) (hfailure : redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced code)) :
                          0 < redBalancedReducedSlack configuration code

                          A red balanced failure makes the corresponding reduced balanced slack positive.

                          source
                          theorem LeanPool.Besicovitch.blueBalancedReducedSlack_pos {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (code : Fin 4) (hfailure : blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced code)) :
                          0 < blueBalancedReducedSlack configuration code

                          A blue balanced failure makes the corresponding reduced balanced slack positive.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_zero_and_blueBalanced_one {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 1))

                          The E0/S1 red-endpoint/blue-balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_zero_and_blueBalanced_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 2))

                          The E0/S2 red-endpoint/blue-balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_zero_and_blueBalanced_three {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 3))

                          The E0/S3 red-endpoint/blue-balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_one_and_blueBalanced_one {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 1))

                          The E1/S1 red-endpoint/blue-balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_one_and_blueBalanced_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 2))

                          The E1/S2 red-endpoint/blue-balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_one_and_blueBalanced_three {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 3))

                          The E1/S3 red-endpoint/blue-balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redBalanced_zero_and_blueBalanced_one {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 1))

                          The S0/S1 balanced/balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redBalanced_zero_and_blueBalanced_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 2))

                          The S0/S2 balanced/balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redBalanced_one_and_blueBalanced_one {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 1))

                          The S1/S1 balanced/balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redBalanced_one_and_blueBalanced_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 2))

                          The S1/S2 balanced/balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redBalanced_two_and_blueBalanced_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 2) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 2))

                          The S2/S2 balanced/balanced representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_zero_and_blueEndpoint_one {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1))

                          The first adjacent endpoint representative is impossible.

                          source
                          theorem LeanPool.Besicovitch.not_redEndpoint_zero_and_blueEndpoint_two {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) :
                          ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 2))

                          The second adjacent endpoint representative is impossible.

                          source
                          def LeanPool.Besicovitch.OffMatchingCoincidentLensBound (configuration : SixPointConfiguration) :
                          Prop

                          The exact scalar lens bound for the off-matching coincident endpoint cell.

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

                            The exact scalar lens bound for the E0/S0 endpoint/balanced cell.

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

                              The exact scalar lens bound for the E1/S0 endpoint/balanced cell.

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

                                The exact scalar lens bound for the S0/S0 balanced/balanced cell.

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

                                  The exact scalar lens bound for the S0/S3 balanced/balanced cell.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    theorem LeanPool.Besicovitch.offMatchingCoincident_excluded_of_lensBound {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hlens : OffMatchingCoincidentLensBound configuration) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1))

                                    The off-matching scalar lens bound excludes its endpoint representative.

                                    source
                                    theorem LeanPool.Besicovitch.endpointBalancedE0S0_excluded_of_lensBound {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hlens : EndpointBalancedE0S0LensBound configuration) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0))

                                    The E0/S0 scalar lens bound excludes its endpoint/balanced representative.

                                    source
                                    theorem LeanPool.Besicovitch.endpointBalancedE1S0_excluded_of_lensBound {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hlens : EndpointBalancedE1S0LensBound configuration) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint 1) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0))

                                    The E1/S0 scalar lens bound excludes its endpoint/balanced representative.

                                    source
                                    theorem LeanPool.Besicovitch.balancedBalancedS0S0_excluded_of_lensBound {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hlens : BalancedBalancedS0S0LensBound configuration) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0))

                                    The S0/S0 scalar lens bound excludes its balanced representative.

                                    source
                                    theorem LeanPool.Besicovitch.balancedBalancedS0S3_excluded_of_lensBound {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hlens : BalancedBalancedS0S3LensBound configuration) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 0) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced 3))

                                    The S0/S3 scalar lens bound excludes its balanced representative.

                                    source
                                    theorem LeanPool.Besicovitch.endpointEndpoint_excluded_outside_lens {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (redCode blueCode : Fin 4) (hnotMatched : endpointEndpointOrbit redCode blueCode ≠ EndpointEndpointOrbit.matchedCoincident) (hnotLens : endpointEndpointOrbit redCode blueCode ≠ EndpointEndpointOrbit.offMatchingCoincident) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint redCode) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint blueCode))

                                    Every endpoint/endpoint cell outside the matched and off-matching lens orbits is excluded.

                                    source
                                    theorem LeanPool.Besicovitch.endpointBalanced_excluded_outside_lenses {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (endpointCode balancedCode : Fin 4) (hnotE0S0 : endpointBalancedOrbit endpointCode balancedCode ≠ EndpointBalancedOrbit.e0s0) (hnotE1S0 : endpointBalancedOrbit endpointCode balancedCode ≠ EndpointBalancedOrbit.e1s0) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint endpointCode) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced balancedCode))

                                    Every endpoint/balanced cell outside the two lens orbits is excluded.

                                    source
                                    theorem LeanPool.Besicovitch.balancedEndpoint_excluded_outside_lenses {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (balancedCode endpointCode : Fin 4) (hnotE0S0 : endpointBalancedOrbit (transposeEndpointCode endpointCode) balancedCode ≠ EndpointBalancedOrbit.e0s0) (hnotE1S0 : endpointBalancedOrbit (transposeEndpointCode endpointCode) balancedCode ≠ EndpointBalancedOrbit.e1s0) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced balancedCode) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.endpoint endpointCode))

                                    The color-reversed endpoint/balanced cells outside the two lens orbits are excluded.

                                    source
                                    theorem LeanPool.Besicovitch.balancedBalanced_excluded_outside_lenses {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (redCode blueCode : Fin 4) (hnotS0S0 : balancedBalancedOrbit redCode blueCode ≠ BalancedBalancedOrbit.s0s0) (hnotS0S3 : balancedBalancedOrbit redCode blueCode ≠ BalancedBalancedOrbit.s0s3) :
                                    ¬(redSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced redCode) ∧ blueSiblingTriangleFailure configuration (SiblingTriangleWitness.balanced blueCode))

                                    Every balanced/balanced cell outside the two lens orbits is excluded.

                                    source
                                    def LeanPool.Besicovitch.SiblingIncidenceOutcome (configuration : SixPointConfiguration) :
                                    Prop

                                    The five possible outcomes after all tangent and direct incidence exclusions.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      theorem LeanPool.Besicovitch.siblingIncidence_route {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hred : ∃ (witness : SiblingTriangleWitness), redSiblingTriangleFailure configuration witness) (hblue : ∃ (witness : SiblingTriangleWitness), blueSiblingTriangleFailure configuration witness) :
                                      SiblingIncidenceOutcome configuration

                                      Simultaneous sibling-triangle witnesses route to a matched endpoint or one lens orbit.

                                      source
                                      theorem LeanPool.Besicovitch.siblingTriangle_score_failure_route {configuration : SixPointConfiguration} (h : configuration.IsAdmissibleAt barS) (hmatching : SelectedDiagonalMatchingFails configuration) (hred : RedSiblingTriangleFails configuration h) (hblue : BlueSiblingTriangleFails configuration h) :
                                      SiblingIncidenceOutcome configuration

                                      If supports 67 and 76 both fail, their witnesses route to the five residual outcomes.