OAI/Combinatorics/HoneycombChords/PositiveFlags.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Positive function flags and orthogonality

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

  1. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_jet_flag_integral_nonzero line 18

    Source documentation

    Orthogonality forces at least m distinct zeros (indeed m sign changes) for continuous functions against a m-dimensional zero-at-origin jet flag. The measure and the squared p-coordinate are those used by the actual strip pairing.

    theorem zero_jet_flag_integral_nonzero {m : ℕ} (b : ℕ → ℝ) (f w : ℝ → ℝ)
    (hb : Monotone (fun i : Fin (m+1)=>b i)) (hb0 : ∀ i : Fin (m+1),0 ≤ b i) (hbfirst : b 0=0)
    (hf : Continuous f) (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ i : Fin m,IntegrableOn (fun p=>f (p^2)*zeroJet b i (p^2)*w p) (Set.Ioi 0))
    (s : Finset ℝ) (hs : ∀ x ∈ s,0 < x) (hz : ∀ x,0 < x → (f x = 0 ↔ x ∈ s)) (hc : s.card < m) :
    ∃ i : Fin m,(∫ p in Set.Ioi (0:ℝ),f (p^2)*zeroJet b i (p^2)*w p)≠0 := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet

  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_linear_zero_set line 87
  3. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_jet_linear_nonorthogonality line 110

    Source documentation

    The constant removed at zero gives exactly the stronger zero count required for the first step of the second interlacing chain.

    theorem zero_jet_linear_nonorthogonality {n m : ℕ} (b c : ℕ → ℝ) (a : Fin n → ℝ)
    (w : ℝ → ℝ) (t : ℝ) (hnm : n < m)
    (hb : Monotone (fun i : Fin (n+1)=>b i)) (hc : Monotone (fun i : Fin m=>c i))
    (hb0 : ∀ i : Fin (n+1),0 ≤ b i) (hc0 : ∀ i : Fin m,0 ≤ c i)
    (hbfirst : b 0=0) (ha : a ≠ 0) (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ j : Fin m,IntegrableOn (fun p=>(p^2-t)*zeroJetCombination b a (p^2)*
      cosineKernelJet (nodalOrder c j) 0 (c j) (p^2)*w p) (Set.Ioi 0)) :
    ∃ j : Fin m,(∫ p in Set.Ioi (0:ℝ),(p^2-t)*zeroJetCombination b a (p^2)*
      cosineKernelJet (nodalOrder c j) 0 (c j) (p^2)*w p) ≠ 0 := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetCombination, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder

  4. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_jet_linear_zero_nonorthogonality line 123
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_zeroJetCombination_linear_pair_integrable line 134
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_zeroJetCombination_linear_zero_pair_integrable line 143
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnot_first line 165
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnot_first line 167
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_interior_row_before line 169
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_interior_row_at line 172
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zero_interior_row_after line 183
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_unique line 199
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_zeros_card_lt line 211
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_finite_zeros line 227
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.family_linear_zero_set line 234
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyTestCoeffs_last line 261
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyTest_zero line 265
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_sub line 271
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination_last_zero line 274
  20. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monic_family_sign line 280

    Source documentation

    A monic combination with the maximum number of positive zeros has the same orientation at those zeros as a monic ordinary polynomial.

    theorem monic_family_sign {n : ℕ} (F : ℕ → ℝ → ℝ) (a : Fin (n+1) → ℝ) (v : Fin n → ℝ)
    (hF : PositiveEvaluation (fun i : Fin (n+1)=>F i))
    (hF0 : PositiveEvaluation (fun i : Fin n=>F i))
    (ha : a (Fin.last n)=1) (hv : StrictMono v) (hv0 : ∀ i,0 < v i)
    (haz : ∀ i,familyCombination F a (v i)=0) {x : ℝ} (hx : 0 < x) (hxv : ∀ i,x ≠ v i) :
    0 < familyCombination F a x*(∏ i,(x-v i)) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination

  21. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_flag_integral_nonzero line 332

    Source documentation

    Orthogonality forces at least m distinct zeros (indeed m sign changes) for continuous functions against a positive m-dimensional function flag. The measure and the squared p-coordinate are those used by the actual strip pairing.

    theorem positive_flag_integral_nonzero {m : ℕ} (B : ℕ → ℝ → ℝ) (f w : ℝ → ℝ)
    (hB : PositiveFlag B m) (hBc : ∀ i : Fin m,Continuous (B i))
    (hf : Continuous f) (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ i : Fin m,IntegrableOn (fun p=>f (p^2)*B i (p^2)*w p) (Set.Ioi 0))
    (s : Finset ℝ) (hs : ∀ x ∈ s,0 < x) (hz : ∀ x,0 < x → (f x = 0 ↔ x ∈ s)) (hc : s.card < m) :
    ∃ i : Fin m,(∫ p in Set.Ioi (0:ℝ),f (p^2)*B i (p^2)*w p)≠0 := by
…

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

  22. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.flag_orthogonal_linear_zeros line 403

    Source documentation

    The maximal zero count at a real pencil root. In particular the root is positive and distinct from the zeros of its root function.

    theorem flag_orthogonal_linear_zeros {n : ℕ} (F G : ℕ → ℝ → ℝ) (a : Fin (n+1) → ℝ)
    (w : ℝ → ℝ) (r : ℝ)
    (hF : PositiveEvaluation (fun i : Fin (n+1)=>F i))
    (hG : PositiveFlag G (n+1)) (hFc : ∀ i : Fin (n+1),Continuous (F i))
    (hGc : ∀ i : Fin (n+1),Continuous (G i)) (ha : a ≠ 0) (hw : ∀ p,0 < p → 0 < w p)
    (hi : ∀ i : Fin (n+1),IntegrableOn (fun p=>(p^2-r)*familyCombination F a (p^2)*G i (p^2)*w p) (Set.Ioi 0))
    (ho : ∀ i : Fin (n+1),(∫ p in Set.Ioi (0:ℝ),(p^2-r)*familyCombination F a (p^2)*G i (p^2)*w p)=0) :
    ∃ Z : Finset ℝ,Z.card=n ∧ (∀ x,x ∈ Z ↔ 0 < x ∧ familyCombination F a x=0) ∧ 0 < r ∧ r ∉ Z := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveEvaluation, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.PositiveFlag, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyCombination

  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_continuous_pairing line 453
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.family_pairing_integral line 478
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.family_pairing_last line 496
  26. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monic_cross_pairing_pos line 517

    Source documentation

    Chebyshev interpolation gives positive orientation of a border pairing at a real root.

    theorem monic_cross_pairing_pos {n : ℕ} (F G : ℕ → ℝ → ℝ) (a : Fin (n+1) → ℝ)
    (w : ℝ → ℝ) (r : ℝ) (hF : PositiveFlag F (n+1)) (hG : PositiveFlag G (n+2))
    (hFc : ∀ i : Fin (n+1),Continuous (F i)) (hGc : ∀ i : Fin (n+2),Continuous (G i))
    (ha : a (Fin.last n)=1) (hw : ∀ p,0 < p → 0 < w p)
    (hi : ∀ i : Fin (n+2),IntegrableOn (fun p=>(p^2-r)*familyCombination F a (p^2)*G i (p^2)*w p) (Set.Ioi 0))
    (ho : ∀ i : Fin (n+1),(∫ p in Set.Ioi (0:ℝ),(p^2-r)*familyCombination F a (p^2)*G i (p^2)*w p)=0) :
    0 < (∫ p in Set.Ioi (0:ℝ),(p^2-r)*familyCombination F a (p^2)*G (n+1) (p^2)*w p) := by
…

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

  27. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.det_border_last_column line 618
  28. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.det_double_border_at_nullvectors line 649