OAI/Combinatorics/HoneycombChords/ObliqueBounds.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Oblique residual and denominator bounds

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.obliqueProjection_sub line 17
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual_sub line 27
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.familyGram_neg_left line 33
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_neg_residual_positiveEvaluation line 38
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_residual_gram_neg line 49
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_residual_zero_neg line 69
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOne_residual_positiveEvaluation line 76
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.hOne_residual_zero_pos line 96
  9. theorem OAI.CriticalHoneycomb.FiniteFunctional.source_residual_denominator_neg line 108

    Source documentation

    The residual denominator is strictly negative.

    theorem source_residual_denominator_neg {N : ℕ} (hN : 1 ≤ N) :
    (obliqueResidual N cThreeCorrection 0).re<0 := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.cThreeCorrection

  10. theorem OAI.CriticalHoneycomb.FiniteFunctional.source_residual_denominator_ne_zero line 114
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_minus_four_pos line 131
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.extended_negative_phase line 138
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_residual_evaluation_minus_four_nonpos line 144
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.familyGram_det_nonneg_of_sorted line 181
  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.cThree_residual_minus_four_nonpos line 196
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_det_le_of_sorted line 238
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetFixedMean_zero_bounds line 256
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.physical_means_at_zero_upper line 288

    Source documentation

    A decaying upper bound for residual means at the origin.

    lemma physical_means_at_zero_upper :
    ∃ A : ℝ,0<A ∧ ∀ᶠ N : ℕ in atTop,∀ s t : ℝ,0<s → s<angle → 0<t → t<angle →
      let P:=((N:ℝ)+1)^(-5/8:ℝ)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.angle

  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinned_residual_det line 337
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_as_tail line 383
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.hZero_residual_zero_pos line 400
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.residual_ofReal_re line 428
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.correction_ofReal_re line 433
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.aStar_eq_ofReal line 438
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.aStar_ofReal_re line 440
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.aStar_re_pos line 442
  27. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily line 458
  28. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedHZero line 460
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_zero line 462
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.hZero_minus_four_gt_one line 464
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedHZero_minus_four_pos line 477
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_positiveEvaluation line 481
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinned_kernel_ratio line 488
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinned_kernel_lower line 505
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.strip_jet_constant_pair_integrable line 567
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_pair_integrable line 572
  37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_characteristic_pair_integrable line 585
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_jet_Gram_pos line 602
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedHZero_jet_integrable line 607
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_measurable line 617
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_cosh_integrable line 623
  42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedHZero_measurable line 637
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedHZero_cosh_integrable line 640
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_mixed_pair_integrable line 653
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily_mixed_Gram_pos line 669
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinned_density_lower line 684
  47. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinned_mean_lower line 704
  48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedGram_ratio_lower line 721
  49. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinned_mixed_mean_lower line 747

    Source documentation

    A lower bound for the zero-pinned interpolation functional.

    theorem pinned_mixed_mean_lower :
    ∃ a : ℝ,0<a ∧ ∀ᶠ N : ℕ in atTop,
      a*((N:ℝ)+1)^(-1/4:ℝ) ≤
        meanResidualRatio stripDensity (pinnedFamily N) (mixedFamily N) pinnedHZero (-4) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedFamily, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedFamily, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pinnedHZero

  50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.meanResidualRatio_realization line 778
  51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_span_of_eq_zero line 818
  52. lemma OAI.CriticalHoneycomb.FiniteFunctional.real_projection_mem line 841
  53. lemma OAI.CriticalHoneycomb.FiniteFunctional.real_projection_cast line 848
  54. lemma OAI.CriticalHoneycomb.FiniteFunctional.extended_span_contains_fixed line 853
  55. lemma OAI.CriticalHoneycomb.FiniteFunctional.extended_span_contains_cThree line 862
  56. lemma OAI.CriticalHoneycomb.FiniteFunctional.extended_span_contains_one line 870
  57. theorem OAI.CriticalHoneycomb.FiniteFunctional.pinned_realization line 880

    Source documentation

    The zero-pinned mean is realized by the mixed Gram system.

    theorem pinned_realization {N : ℕ} (hN : 1≤N) :
    pinnedHZero (-4)*meanResidualRatio stripDensity (pinnedFamily N) (mixedFamily N) pinnedHZero (-4)=
      (obliqueResidual N hZero (-4)).re-
        (obliqueResidual N (C (3*angle/2)) (-4)).re *
          (obliqueResidual N hZero 0).re/(obliqueResidual N (C (3*angle/2)) 0).re := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.hZero, OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.angle

  58. theorem OAI.CriticalHoneycomb.FiniteFunctional.pinned_source_residual_lower line 964

    Source documentation

    A lower bound for the zero-pinned residual in the physical bridge formula.

    theorem pinned_source_residual_lower :
    ∃ a : ℝ,0<a ∧ ∀ᶠ N : ℕ in atTop,
      a*((N:ℝ)+1)^(-1/4:ℝ) ≤
        (obliqueResidual N hZero (-4)).re-
          (obliqueResidual N (C (3*angle/2)) (-4)).re *
            (obliqueResidual N hZero 0).re/(obliqueResidual N (C (3*angle/2)) 0).re := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.hZero, OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.angle

  59. theorem OAI.CriticalHoneycomb.FiniteFunctional.source_h_residuals_at_zero_upper line 987

    Source documentation

    A decaying upper bound at the origin for the two mixed residuals.

    theorem source_h_residuals_at_zero_upper :
    ∃ A : ℝ, 0 < A ∧ ∀ᶠ N : ℕ in atTop,
      let P := ((N:ℝ)+1)^(-5/8:ℝ)
…