OAI/Combinatorics/HoneycombChords/CharacteristicProducts.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Oblique characteristic product estimates

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_ratio_reversal line 15
  2. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pole_knot_expansion_comparison line 21
  3. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJet_characteristic_bounds line 87

    Source documentation

    The fixed positive-parameter characteristic product for the literal symmetric complete-jet space and the original strip density.

    theorem twoJet_characteristic_bounds {y z:ℝ} (hy:0<y) (hyz:y<z) :
    ∃ a A:ℝ,0<a ∧ 0<A ∧ ∀ᶠ N:ℕ in atTop,
      a*((N:ℝ)+1)^(3*(y-z)/8)≤
        (familyGram (fun p=>characteristicRatio y z p*stripDensity p) (twoJetFamily N) (twoJetFamily N)).det /
          (familyGram stripDensity (twoJetFamily N) (twoJetFamily N)).det ∧
      (familyGram (fun p=>characteristicRatio y z p*stripDensity p) (twoJetFamily N) (twoJetFamily N)).det /
          (familyGram stripDensity (twoJetFamily N) (twoJetFamily N)).det≤A*((N:ℝ)+1)^(3*(y-z)/8) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetFamily

  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polePencil_characteristic_gram line 127
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polePencil_original_gram line 135
  6. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.first_oblique_characteristic_product_bounds line 143

    Source documentation

    A uniform determinant product bound for the first nonsymmetric family.

    theorem first_oblique_characteristic_product_bounds {y z:ℝ} (hy:0<y) (hyz:y<z) :
    ∃ a A:ℝ,0<a ∧ 0<A ∧ ∀ᶠ N:ℕ in atTop,∀ s t:ℝ,0<s→s<angle→0<t→t<angle→
      a*((N:ℝ)+1)^(3*(y-z)/8)≤
        (jetGram (n:=2*N+1) (fun p=>characteristicRatio y z p*stripDensity p)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A, OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_characteristic_le_one_square line 180
  8. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.first_oblique_growing_product_bound line 197

    Source documentation

    A uniform subexponential characteristic bound for the first nonsymmetric family at the moving scale y² = 2z² = 2N^(3/2).

    theorem first_oblique_growing_product_bound :
    ∃ D:ℕ,0<D ∧ ∃ c C:ℝ,0<c ∧ 0<C ∧ ∀ᶠ N:ℕ in atTop,
      ∀ y z:ℝ,1≤z→z≤y→y^2≤2*z^2→1/2≤c*y/Real.pi→
      ∀ s t:ℝ,0<s→s<angle→0<t→t<angle→
      (jetGram (n:=2*N+1) (fun p=>characteristicRatio y z p*stripDensity p)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D, OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  9. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetMatrix line 246
  10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetMatrix_representation line 248
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJetMatrix_transpose_injective line 255
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_gram_compression line 261
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_tilt_lower line 272
  14. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_characteristic_sandwich line 287

    Source documentation

    Removing the evaluation-at-zero direction changes the characteristic quotient by at most its single uniform eigenvalue bound.

    theorem zeroJet_characteristic_sandwich {m N:ℕ} (hm:m+1=2*N) (hN:0<N) {y z:ℝ} (hy:0<y) (hyz:y<z) :
    let w:=fun p=>characteristicRatio y z p*stripDensity p
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleZeroPencil_characteristic_gram line 330
  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleZeroPencil_original_gram line 338
  17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleMixedZeroPencil_characteristic_gram line 346
  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poleMixedZeroPencil_original_gram line 355
  19. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.second_oblique_characteristic_product_bounds line 364

    Source documentation

    A characteristic product bound for the second nonsymmetric family, uniform over its interior label.

    theorem second_oblique_characteristic_product_bounds {y z:ℝ} (hy:0<y) (hyz:y<z) :
    ∃ a A:ℝ,0<a ∧ 0<A ∧ ∀ᶠ N:ℕ in atTop,∀ t:ℝ,0<t→t<angle→
      let F:=fun i:Fin (2*N+1)=>zeroJet (extendedKnotLabels N) i
…

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

  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_tilt_det_pos line 406
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.secondOblique_expansion_aux line 421
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_expansion_lower line 456
  23. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet_expansion_upper line 470

    Source documentation

    Removing the evaluation direction under an expanding characteristic factor only decreases the characteristic determinant quotient.

    theorem zeroJet_expansion_upper {m N:ℕ} (hm:m+1=2*N) (hN:0<N) {y z:ℝ} (hz:0<z) (hzy:z≤y) :
    (familyGram (fun p=>characteristicRatio y z p*stripDensity p)
      (fun i:Fin m=>zeroJet (twoKnotLabels N) i) (fun i:Fin m=>zeroJet (twoKnotLabels N) i)).det/
    (familyGram stripDensity (fun i:Fin m=>zeroJet (twoKnotLabels N) i) (fun i:Fin m=>zeroJet (twoKnotLabels N) i)).det ≤
    (jetGram (n:=2*N) (fun p=>characteristicRatio y z p*stripDensity p) (twoKnotLabels N) (twoKnotLabels N)).det/
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoKnotLabels, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram

  24. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.second_oblique_growing_product_bound line 505

    Source documentation

    A moving-parameter characteristic bound for the second nonsymmetric family.

    theorem second_oblique_growing_product_bound :
    ∃ D:ℕ,0<D ∧ ∃ c C:ℝ,0<c ∧ 0<C ∧ ∀ᶠ N:ℕ in atTop,
      ∀ y z:ℝ,1≤z→z<y→y^2≤2*z^2→1/2≤c*y/Real.pi→
      ∀ t:ℝ,0<t→t<angle→
      let F:=fun i:Fin (2*N+1)=>zeroJet (extendedKnotLabels N) i
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D, OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnotLabels

  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rpow_log_isLittleO_id line 568

    Source documentation

    A scalar estimate for moving-parameter characteristic products with exponent 3/4.

    lemma rpow_log_isLittleO_id {r:ℝ} (hr:r<1) :
    (fun x:ℝ=>x^r*log x)=o[atTop] fun x=>x := by
…
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rpow_isLittleO_id line 576
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.log_majorant_isLittleO_id line 584
  28. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_power_product_subexponential line 597

    Source documentation

    Polynomial power products are exponentially negligible at every fixed sublinear moving exponent.

    theorem polynomial_power_product_subexponential {A d r:ℝ} (hA:0<A) (hd:0<d) (hr:r<1)
    (a b c:ℝ) {ε:ℝ} (hε:0<ε) :
    ∀ᶠ x:ℝ in atTop,A*x^a*(d*x)^(b*x^r+c)≤exp (ε*x) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.A

  29. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.moving_majorant_subexponential line 616

    Source documentation

    The characteristic product is exp(o(N)) at a moving pole of order N^(3/4).

    theorem moving_majorant_subexponential (D:ℕ) {C k ε:ℝ} (hC:0≤C) (hk:0≤k) (hε:0<ε) :
    ∀ᶠ N:ℕ in atTop,
      16*(1+C*((N:ℝ)^(3/4:ℝ))^4*((D*N:ℕ)+1:ℝ)^3*
        (4*((D*N:ℕ)+1:ℝ))^(k*(N:ℝ)^(3/4:ℝ)+1)) ≤ exp (ε*N) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.D, OAI.CriticalHoneycomb.FiniteFunctional.C

  30. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingPole line 670
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingPole_conditions line 671
  32. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.first_oblique_moving_subexponential line 687

    Source documentation

    First actual two-endpoint ensemble has exp(o(N)) characteristic moment at y²=2z²=2N^(3/2), uniformly in both interior labels.

    theorem first_oblique_moving_subexponential {ε:ℝ} (hε:0 < ε) :
    ∀ᶠ N:ℕ in atTop,∀ s t:ℝ,0 < s→s < angle→0 < t→t < angle→
      (jetGram (n:=2*N+1) (fun p=>characteristicRatio (sqrt 2*movingPole N) (movingPole N) p*stripDensity p)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jetGram, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.movingPole, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity

  33. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.second_oblique_moving_subexponential line 704

    Source documentation

    A subexponential moving-parameter bound for the second nonsymmetric family.

    theorem second_oblique_moving_subexponential {ε:ℝ} (hε:0 < ε) :
    ∀ᶠ N:ℕ in atTop,∀ t:ℝ,0 < t→t < angle→
      let F:=fun i:Fin (2*N+1)=>zeroJet (extendedKnotLabels N) i
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.angle, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.zeroJet, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.extendedKnotLabels