OAI/Combinatorics/HoneycombChords/JetCompression.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Polynomial compression of complete jet Gram matrices

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scalar_young_abs line 15
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.scalar_square_perturbation line 25
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm_sub_integrable line 33
  4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm_young line 42
  5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSpan_mono line 85
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSpan_actual_pair line 89
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripSpan_tilt_pair line 100
  8. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.monomial_mem_stripSpan line 111
  9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_mem_stripSpan line 120
  10. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetFamily line 128
  11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetFamily_mem line 130
  12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteFamilyCombination_mem_stripSpan line 132
  13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetFamily_posDef line 138
  14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TwoJetPolynomialCompression line 152

    Source documentation

    Fixed-parameter determinant compression for the complete jet family.

    def TwoJetPolynomialCompression : Prop :=
…
  15. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_error_from_norm line 168

    Source documentation

    An integral perturbation bound for polynomial compression.

    theorem familyGram_error_from_norm {n:ℕ} (w:ℝ→ℝ) (F G:Fin n→ℝ→ℝ)
    (hw:∀ p,0<p→0≤w p)
    (hFF:∀ i j,IntegrableOn (fun p=>F i (p^2)*F j (p^2)*w p) (Set.Ioi 0))
    (hGG:∀ i j,IntegrableOn (fun p=>G i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    (hFG:∀ i j,IntegrableOn (fun p=>F i (p^2)*G j (p^2)*w p) (Set.Ioi 0))
    {δ t:ℝ} (ht:0<t)
    (herr:∀ v:Fin n→ℝ,
      familySquaredNorm w (fun x=>finiteFamilyCombination F v x-finiteFamilyCombination G v x)≤
        δ*familySquaredNorm w (finiteFamilyCombination F v)) :
    ∀ v:Fin n→ℝ,
      |v ⬝ᵥ (familyGram w G G *ᵥ v)-v ⬝ᵥ (familyGram w F F *ᵥ v)|≤
        (t+(1+1/t)*δ)*(v ⬝ᵥ (familyGram w F F *ᵥ v)) := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.w, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteFamilyCombination, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram

  16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familySquaredNorm_weight_bounds line 194
  17. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJet_orthonormal_polynomial_approximation line 221

    Source documentation

    The genuine complete-jet space admits one simultaneous polynomial approximation on an orthonormal basis; constants do not depend on its vectors.

    theorem twoJet_orthonormal_polynomial_approximation :
    ∃ C N₀:ℕ,0<C ∧ ∀ N:ℕ,N₀≤N→0<N→
      ∃ (T:Matrix (Fin (2*N)) (Fin (2*N)) ℝ) (P:Fin (2*N)→Polynomial ℝ),
        IsUnit T.det ∧
        (let F:=fun i=>finiteFamilyCombination (twoJetFamily N) (T i)
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.C, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.finiteFamilyCombination, OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetFamily

  18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orthonormal_family_error line 267
  19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orthonormal_family_tilt_error line 286
  20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.posDef_real_congruence line 337
  21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.determinant_quotient_congruence line 342
  22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.posDef_of_relative_error line 349
  23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_family_compression line 358
  24. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.compressionError line 381
  25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.compressionError_nonneg line 383
  26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.compressionError_eventually_small line 385
  27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orthonormal_stripGram_transfer line 426
  28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.characteristicRatio_le_one line 492
  29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetFamily_tilt_posDef line 497
  30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.familyGram_tilt_contraction line 504
  31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJet_contains_monomials line 518
  32. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJet_polynomial_compression_upper line 535

    Source documentation

    A containment inequality for polynomial compression at every natural index.

    theorem twoJet_polynomial_compression_upper (N:ℕ) {y z:ℝ} (hy:0<y) (hyz:y<z) :
    (familyGram (fun p=>characteristicRatio y z p*stripDensity p) (twoJetFamily N) (twoJetFamily N)).det /
      (familyGram stripDensity (twoJetFamily N) (twoJetFamily N)).det≤
    (monomialGram N (fun p=>characteristicRatio y z p*stripDensity p)).det/(monomialGram N stripDensity).det := by
…

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

  33. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJetPolynomialCompression line 564

    Source documentation

    Determinant compression for the complete jet family with the strip weight.

    theorem twoJetPolynomialCompression : TwoJetPolynomialCompression := by
…

    Mentions: OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.TwoJetPolynomialCompression

  34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orthonormal_family_expansion_error line 624
  35. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.orthonormal_stripGram_expansion_transfer line 666
  36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.diagonal_compression_codimension line 732
  37. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.positive_compression_codimension line 769

    Source documentation

    The matching compression bound with the codimension factor.

    theorem positive_compression_codimension {n m:ℕ}
    (A B:Matrix (Fin m) (Fin m) ℝ) (C:Matrix (Fin n) (Fin m) ℝ)
    (hA:A.PosDef) (hB:B.PosDef) (hCB:(C*B*Cᵀ).PosDef) {l:ℝ} (hl:0≤l)
    (hAB:∀ v:Fin m→ℝ,l*(v ⬝ᵥ (B *ᵥ v))≤v ⬝ᵥ (A *ᵥ v)) :
    l^(m-n)*((C*A*Cᵀ).det/(C*B*Cᵀ).det)≤A.det/B.det := by
…

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

  38. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.twoJet_polynomial_expansion_uniform line 822

    Source documentation

    One uniform polynomial compression bound for every parameter pair with 1≤(y/z)²≤2, including the moving pair in strip-asymptotics:107.

    theorem twoJet_polynomial_expansion_uniform :
    ∃ C:ℕ,0<C ∧ ∀ᶠ N:ℕ in atTop,∀ y z:ℝ,0<z→z≤y→y^2≤2*z^2→
      (familyGram (fun p=>characteristicRatio y z p*stripDensity p) (twoJetFamily N) (twoJetFamily N)).det /
        (familyGram stripDensity (twoJetFamily N) (twoJetFamily N)).det ≤
      4*((monomialGram (C*N) (fun p=>characteristicRatio y z p*stripDensity p)).det /
        (monomialGram (C*N) stripDensity).det) := by
…

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