OAI/Combinatorics/HoneycombChords/Interlacing.lean

GitHub source file

122 declarations, 0 contain sorry, 0 declared as axioms

Moment pencils and positive root interlacing

Formalized from Critical honeycomb chords with prescribed boundary endpoints (OpenAI, September 26, 2026).

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil line 15
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_prefix line 18
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_transpose line 20
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_pairing line 26
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_kernel_last_ne line 44
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_monic_left_kernel line 73
  7. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_sturm line 95

    Source documentation

    Exact signed-border identity with positive factors at every real root. This proves the Sturm sign needed for the second oblique comparison.

    theorem flagPencil_sturm {n : ℕ} (F G : ℕ → ℝ → ℝ) (w : ℝ → ℝ) (r : ℝ)
    (hz : (flagPencil (n+1) F G w r).det=0)
    (hF : PositiveFlag F (n+2)) (hG : PositiveFlag G (n+2))
    (hFc : ∀ i : Fin (n+2),Continuous (F i)) (hGc : ∀ i : Fin (n+2),Continuous (G i))
    (hw : ∀ p,0 < p → 0 < w p)
    (hi : ∀ i j : Fin (n+2),IntegrableOn (fun p=>(p^2-r)*F i (p^2)*G j (p^2)*w p) (Set.Ioi 0)) :
    0 < r ∧ ∃ L R : ℝ,0 < L ∧ 0 < R ∧
      (flagPencil (n+2) F G w r).det= -(flagPencil n F G w r).det*L*R := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveFlag

  8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generalizedCharpoly line 157
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generalizedCharpoly_monic line 159
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generalizedCharpoly_natDegree line 161
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generalizedCharpoly_eval line 163
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.generalizedCharpoly_eval_zero_iff line 173
  13. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagGram line 188
  14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic line 190
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_affine line 192
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_integrable line 205
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagGram_det_pos line 217
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_zero_det_pos line 221
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic_eval line 240
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic_eval_zero_iff line 247
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic_zero_sign line 253
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monic_eq_root_product line 276
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.product_cut_sign line 283
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interlacing_product_sign line 304
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strictMono_lastCases_real line 321
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuous_root_between line 330
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.root_between_each line 337
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.alternating_sign_opposite line 347
  29. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_sturm_intervals line 359

    Source documentation

    A polynomial with the Sturm signs at a positive ordered node vector has a root in each intervening interval, including the first and last.

    theorem polynomial_sturm_intervals {n : ℕ} (p : ℝ[X]) (r : Fin n → ℝ)
    (hr : StrictMono r) (hr0 : ∀ i,0<r i)
    (hrootSigns : ∀ j,0 < (-1:ℝ)^(n-j.val)*p.eval (r j))
    (hzero : 0 < (-1:ℝ)^(n+1)*p.eval 0)
    (htop : Tendsto (fun x=>p.eval x) atTop atTop) :
    ∃ s : Fin (n+1) → ℝ,StrictMono s ∧ (∀ i,0<s i) ∧ (∀ i,p.eval (s i)=0) ∧
      (∀ i,s i.castSucc<r i ∧ r i<s i.succ) := by
…
  30. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveInterlacing line 410

    Source documentation

    Strict positive interlacing, with the exact characteristic factorization.

    def PositiveInterlacing (p q : ℝ[X]) (n : ℕ) : Prop :=
…
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monic_polynomial_tendsto line 415
  32. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_sturm_chain line 422

    Source documentation

    The sign relation for a one-dimensional oblique extension implies real, simple, positive, interlacing roots for every finite prefix.

    theorem polynomial_sturm_chain {N : ℕ} (p : ℕ → ℝ[X])
    (hm : ∀ k,k ≤ N → (p k).Monic) (hd : ∀ k,k ≤ N → (p k).natDegree=k)
    (hzero : ∀ k,k ≤ N → 0 < (-1:ℝ)^k*(p k).eval 0)
    (hstep : ∀ k,k+2 ≤ N → ∀ x,(p (k+1)).eval x=0 →
      ∃ C : ℝ,0<C ∧ (p (k+2)).eval x= -C*(p k).eval x) :
    ∀ n,n+1 ≤ N → PositiveInterlacing (p n) (p (n+1)) n := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveInterlacing

  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_fraction_mono line 470
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interlacing_product_ratio line 474
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_product_negative_ratio line 503
  36. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_interlacing_ratio line 510
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic_sturm line 525
  38. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic_interlaces line 559

    Source documentation

    Finite moment pencils of two positive flags have real, strictly positive, interlacing roots.

    theorem flagCharacteristic_interlaces {N : ℕ} (F G : ℕ → ℝ → ℝ) (w : ℝ → ℝ)
    (hF : PositiveFlag F N) (hG : PositiveFlag G N)
    (hFc : ∀ i : Fin N,Continuous (F i)) (hGc : ∀ i : Fin N,Continuous (G i))
    (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ i j : Fin N,IntegrableOn (fun p=>F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    (h2 : ∀ i j : Fin N,IntegrableOn (fun p=>p^2*F i (p^2)*G j (p^2)*w p) (Set.Ioi 0)) :
    ∀ n,n+1 ≤ N → PositiveInterlacing (flagCharacteristic n F G w) (flagCharacteristic (n+1) F G w) n := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveFlag, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveInterlacing, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagCharacteristic

  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_ratio line 586
  40. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_one_step line 597

    Source documentation

    A one-dimensional determinant comparison for oblique chains with positive Chebyshev extensions.

    theorem flagPencil_one_step {n : ℕ} (F G : ℕ → ℝ → ℝ) (w : ℝ → ℝ)
    (hF : PositiveFlag F (n+1)) (hG : PositiveFlag G (n+1))
    (hFc : ∀ i : Fin (n+1),Continuous (F i)) (hGc : ∀ i : Fin (n+1),Continuous (G i))
    (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ i j : Fin (n+1),IntegrableOn (fun p=>F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    (h2 : ∀ i j : Fin (n+1),IntegrableOn (fun p=>p^2*F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    {A B : ℝ} (hA : 0<A) (hAB : A<B) :
    (A/B)*((flagPencil n F G w (-A)).det/(flagPencil n F G w (-B)).det) ≤
      (flagPencil (n+1) F G w (-A)).det/(flagPencil (n+1) F G w (-B)).det ∧
    (flagPencil (n+1) F G w (-A)).det/(flagPencil (n+1) F G w (-B)).det ≤
      (flagPencil n F G w (-A)).det/(flagPencil n F G w (-B)).det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveFlag, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil

  41. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil_two_steps line 614
  42. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.NonvanishingFlag line 643

    Source documentation

    For the actual second oblique chain, the bases are reordered relative to the sorted complete jets. The orientation is immaterial for a pencil ratio.

    def NonvanishingFlag (F : ℕ → ℝ → ℝ) (N : ℕ) : Prop :=
…
  43. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagAnchor line 646
  44. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagOrientation line 648
  45. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orientedFlag line 649
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagAnchor_ne_zero line 650
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_det_same_sign line 658
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagOrientation_product line 702
  49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orientedFlag_positive line 714
  50. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.moveLast line 743

    Source documentation

    Move one selected row to the end, preserving the order of the rest.

    def moveLast (n : ℕ) (p : Fin (n+1)) : Equiv.Perm (Fin (n+1)) :=
…
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.moveLast_castSucc line 745
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.moveLast_last line 748
  53. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftLastPerm line 749
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftLastPerm_castSucc line 751
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftLastPerm_last line 754
  56. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftFirstPerm line 756
  57. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftFirstPerm_zero line 758
  58. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.liftFirstPerm_succ line 759
  59. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_perm_det_ne_zero line 762
  60. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.constant_row_subtraction_det line 767
  61. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cons_zeroJet_det line 775
  62. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.prepend_permuted_det_ne_zero line 779
  63. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.append_permuted_det_ne_zero line 789
  64. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.constant_to_last_det_ne_zero line 799
  65. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cons_lastCases_swap line 809
  66. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.constant_to_penultimate_det_ne_zero line 822
  67. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_before line 841
  68. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_order_before line 843
  69. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_extended_before line 850
  70. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_monotone line 854
  71. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_nonneg line 865
  72. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_bound line 870
  73. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnot_first line 876
  74. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroInsertion line 877
  75. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_insertion_reorder line 878
  76. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_interior_appended_det_ne_zero line 891
  77. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_extended_split line 900
  78. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeft_top_det_ne_zero line 908
  79. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scalar_familyPencil_det line 930
  80. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orientedFlagPencil_ratio line 944
  81. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orientedFlag_integrable line 954
  82. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.unorientedPencil_two_steps line 964

    Source documentation

    A two-step determinant comparison for Chebyshev families.

    theorem unorientedPencil_two_steps {n : ℕ} (F G : ℕ → ℝ → ℝ) (w : ℝ → ℝ)
    (hF : NonvanishingFlag F (n+2)) (hG : NonvanishingFlag G (n+2))
    (hFc : ∀ i : Fin (n+2),Continuous (F i)) (hGc : ∀ i : Fin (n+2),Continuous (G i))
    (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ i j : Fin (n+2),IntegrableOn (fun p=>F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    (h2 : ∀ i j : Fin (n+2),IntegrableOn (fun p=>p^2*F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    {A B : ℝ} (hA : 0<A) (hAB : A<B) :
    (A/B)^2*((flagPencil n F G w (-A)).det/(flagPencil n F G w (-B)).det) ≤
      (flagPencil (n+2) F G w (-A)).det/(flagPencil (n+2) F G w (-B)).det ∧
    (flagPencil (n+2) F G w (-A)).det/(flagPencil (n+2) F G w (-B)).det ≤
      (flagPencil n F G w (-A)).det/(flagPencil n F G w (-B)).det := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.NonvanishingFlag, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flagPencil

  83. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRight_middle_det_ne_zero line 997
  84. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRight_top_det_ne_zero line 1004
  85. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.appendTwo line 1015
  86. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.appendTwo_prefix line 1017
  87. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.appendTwo_middle line 1021
  88. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.appendTwo_top line 1027
  89. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeftFlag line 1033
  90. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRightFlag line 1036
  91. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_twoKnot_nonvanishing line 1038
  92. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeft_nonvanishing line 1042
  93. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRight_nonvanishing line 1057
  94. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripKernelSpan line 1080
  95. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.kernel_mem_stripSpan line 1082
  96. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.one_mem_stripSpan line 1084
  97. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_mem_stripSpan line 1090
  98. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSpan_continuous line 1100
  99. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSpan_pair_integrable line 1106
  100. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeft_mem line 1140
  101. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRight_mem line 1150
  102. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.permutationFactor line 1165
  103. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.permutationFactor_ne_zero line 1166
  104. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_perm_factor line 1169
  105. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_append_perm_factor line 1174
  106. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.evaluation_prepend_perm_factor line 1183
  107. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.constant_to_penultimate_factor line 1192
  108. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_evaluation_factors line 1202
  109. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSpan_pair_pencil_integrable line 1220
  110. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeftFactor line 1237
  111. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRightFactor line 1239
  112. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeftFactor_ne_zero line 1241
  113. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRightFactor_ne_zero line 1243
  114. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondLeft_evaluation_factor line 1245
  115. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondRight_evaluation_factor line 1253
  116. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedZero_mem line 1266
  117. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorRaw_mem line 1268
  118. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondChain_pencil_factor line 1271
  119. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondChain_bottom_pencil line 1308
  120. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondChain_pencil_ratio line 1314
  121. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondOblique_comparison_aux line 1322
  122. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondObliqueCharacteristicComparison line 1342

    Source documentation

    The second oblique characteristic comparison follows from complete jet positivity and finite moments.

    theorem secondObliqueCharacteristicComparison : SecondObliqueCharacteristicComparison := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SecondObliqueCharacteristicComparison