OAI/Combinatorics/HoneycombChords/FiniteFunctional.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The finite strip functional and its polynomial and hyperbolic interpolation space.

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

  1. def OAI.CriticalHoneycomb.FiniteFunctional.C line 13

    Source documentation

    Entire real continuation of cosh(t sqrt x), also at negative x.

    noncomputable def C (t x : ℝ) : ℂ :=
…
  2. def OAI.CriticalHoneycomb.FiniteFunctional.D line 17
  3. def OAI.CriticalHoneycomb.FiniteFunctional.aStar line 18
  4. def OAI.CriticalHoneycomb.FiniteFunctional.M line 21

    Source documentation

    Both blocks of the exact 2N-dimensional interpolation space.

    noncomputable def M (N : ℕ) : Submodule ℂ (ℝ → ℂ) :=
…
  5. def OAI.CriticalHoneycomb.FiniteFunctional.g line 28

    Source documentation

    Integral of the entire cosine continuation, with removable value g 0 = angle.

    noncomputable def g (x : ℝ) : ℂ := ∫ t in (0:ℝ)..angle, C t x

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

  6. def OAI.CriticalHoneycomb.FiniteFunctional.admissibleDensity line 30
  7. def OAI.CriticalHoneycomb.FiniteFunctional.pairing line 34

    Source documentation

    Bilinear pairing for the positive strip measure, without complex conjugation.

    noncomputable def pairing (H f : ℝ → ℂ) : ℂ :=
…
  8. def OAI.CriticalHoneycomb.FiniteFunctional.value line 39
  9. def OAI.CriticalHoneycomb.FiniteFunctional.PhysicalFiniteFunctional line 43

    Source documentation

    Representation of the physical bridge mass by the finite strip functional.

    def PhysicalFiniteFunctional : Prop :=
…