OAI/Combinatorics/HoneycombChords/StripPolynomial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Hyperbolic bounds for the strip density

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

  1. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sinh_le_mul_cosh_nonneg line 16
  2. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosh_add_le_twice line 28
  3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.cosh_le_sinh_add_one line 32
  4. theorem OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.stripDensity_sech_bounds line 38

    Source documentation

    Global comparison to the exact exponential rate b=3L; no asymptotic weight hypothesis is being postulated.

    theorem stripDensity_sech_bounds {p : ℝ} (hp : 0 < p) :
    1/(8*angle*Real.cosh (3*angle*p)) ≤ stripDensity p ∧
    stripDensity p ≤ (p+1/angle)/Real.cosh (3*angle*p) := by
…

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

  5. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity line 74
  6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity_pos line 75
  7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.squaredPoleDensity_bounds line 78