OAI/Combinatorics/HoneycombChords/ChebyshevSystems.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Chebyshev spaces, sign changes, orthogonality, and nested jet flags.

The development follows OpenAI, Uniform marked-polygon estimates and sharp finite bridge moments (2026), Sections 6 and 7.

  1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnotLabels line 13

    Source documentation

    Literal complete labels of M: N jets at 0, N at L^2.

    noncomputable def twoKnotLabels (N : ℕ) (k : ℕ) : ℝ := if k<N then 0 else angle^2

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle

  2. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnotLabels line 15

    Source documentation

    Literal complete labels of M + R C_t, with the C_t row inserted in order.

    noncomputable def interiorKnotLabels (N : ℕ) (t : ℝ) (k : ℕ) : ℝ :=
…
  3. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.FirstObliqueCharacteristicComparison line 18
  4. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination line 36
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_contDiff line 38
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_iteratedDeriv line 43
  7. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_confluent_unique line 54

    Source documentation

    The literal complete beta-jet family is Chebyshev counting multiplicities.

    theorem jetCombination_confluent_unique {n : ℕ} (b x : ℕ → ℝ) (a : Fin n → ℝ)
    (hb : Monotone (fun i : Fin n=>b i)) (hx : Monotone (fun i : Fin n=>x i))
    (hb0 : ∀ i : Fin n,0 ≤ b i) (hx0 : ∀ i : Fin n,0 ≤ x i)
    (hz : ∀ j : Fin n,iteratedDeriv (nodalOrder x j) (jetCombination b a) (x j)=0) : a=0 := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nodalOrder, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination

  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_unique line 68
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_zeros_card_lt line 81
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_finite_zeros line 97
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.continuous_nonzero_sign line 112
  12. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finite_zero_sign_polynomial line 131

    Source documentation

    For a continuous function with finitely many zeros on a ray, its sign is matched by a polynomial using a subset of these zeros, not by an assumed oscillation hypothesis. This is the sign test needed by oblique jet pencils.

    theorem finite_zero_sign_polynomial (f : ℝ → ℝ) (hf : Continuous f) (s : Finset ℝ) :
    ∀ a : ℝ,(∀ x∈s,a<x) → (∀ x,a<x → (f x=0 ↔ x∈s)) →
      ∃ t : Finset ℝ,t⊆s ∧ ∃ e : ℝ,e≠0 ∧
        ∀ x,a<x → x∉s → 0<f x*(e*∏ z∈t,(x-z)) := by
…
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.vandermonde_cons_det line 207
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetEvaluation_zero_labels line 223
  15. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetTestCoeffs line 235

    Source documentation

    Cofactor coefficients of the literal complete-jet interpolant test.

    noncomputable def jetTestCoeffs {n : ℕ} (b : ℕ → ℝ) (v : Fin n → ℝ) : Fin (n+1) → ℝ :=
…
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetTest_eq_det line 238
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetTest_sign_product line 246
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetCombination_smul line 275
  19. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_flag_sign_matching line 282
  20. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_flag_integral_nonzero line 339

    Source documentation

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

    theorem jet_flag_integral_nonzero {m : ℕ} (b : ℕ → ℝ) (f w : ℝ → ℝ)
    (hb : Monotone (fun i : Fin m=>b i)) (hb0 : ∀ i : Fin m,0 ≤ b i)
    (hf : Continuous f) (hw : ∀ p,0<p → 0<w p)
    (hi : ∀ i : Fin m,IntegrableOn (fun p=>f (p^2)*cosineKernelJet (nodalOrder b i) 0 (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)*cosineKernelJet (nodalOrder b i) 0 (b i) (p^2)*w p)≠0 := by
…

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

  21. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jet_linear_nonorthogonality line 409
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jetCombination_linear_pair_integrable line 442
  23. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_jet_linear_nonorthogonality line 458
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_angle_pos line 475
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnot_monotone line 476
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnot_nonneg line 480
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnot_le line 483
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnot_monotone line 486
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnot_nonneg line 492
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnot_le line 495
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnot_nodalOrder line 500
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.interiorKnot_nodalOrder line 521
  33. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.insertKnotIndex line 554

    Source documentation

    Insertion map for the common M rows into the (sorted) interior-knot flag.

    def insertKnotIndex (N : ℕ) (i : Fin (2*N)) : Fin (2*N+1) :=
…
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.insertKnot_row line 556
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.insertKnotIndex_injective line 566
  36. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPermutation line 582

    Source documentation

    Move the inserted t² label to the last index, leaving M in its original order. This is only a simultaneous change of basis of the actual pencil.

    def knotPermutation (N : ℕ) : Equiv.Perm (Fin (2*N+1)) :=
…
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPermutation_castSucc line 584
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.knotPermutation_last line 594