OAI/Combinatorics/HoneycombChords/TranslatedJets.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Translated differential equations, Rolle estimates, and confluent positivity.

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_square_cos line 15
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_first_negative line 20
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_ode_at_square line 35
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosineKernelJet_shifted_ode line 77
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ordered_rolle line 122
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.ordered_rolle_from_zero line 143
  7. structure OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily line 182

    Source documentation

    The exact two-step positive differential system supplied by translating the cosine kernel below its first zero. It does not assume any determinant sign.

    structure SturmPowerFamily (T : ℝ) where
…
  8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.combination line 199
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.combination_continuous line 202
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.combination_Fderiv line 207
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.combination_Hderiv line 218
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.lower_H_roots line 232
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.sparse_unique_bounded line 245
  14. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.SturmPowerFamily.sparse_unique line 304
  15. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU line 323
  16. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedUPrime line 325
  17. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedF line 327
  18. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedH line 329
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_hasDerivAt line 332
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedUPrime_hasDerivAt line 338
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedUPrime_zero_deriv line 346
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedUPrime_succ_deriv line 349
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_zero_eq_cos line 353
  24. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_zero_pos line 357
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedF_hasDerivAt line 367
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedH_succ_deriv line 371
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_initial line 377
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedH_initial line 386
  29. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedSturmFamily line 389
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_parameter_continuous line 424
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_parameter_zero line 428
  32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_det_ne_zero line 433
  33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_det_pos_zero line 453
  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translatedU_det_pos line 468
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translated_beta_eval_det_pos line 496
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.newtonKernel_det_pos_strict line 508
  37. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardNodes line 521
  38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardNodes_pos line 524
  39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardNodes_le line 527
  40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardNodes_lt line 532
  41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardNodes_strictMono line 537
  42. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardPerturb line 546
  43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardPerturb_range line 549
  44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.inwardPerturb_strict line 560
  45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translated_newton_det_nonneg line 580
  46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.translated_beta_jet_det_nonneg line 610