BridgeLaplace.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

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

def OAI.CriticalHoneycomb.bridgeLaplace line 19
Source documentation
The height Laplace transform of the strict bridge mass.
```
noncomputable def bridgeLaplace (s : ℝ) : ℝ :=
…
```
lemma OAI.CriticalHoneycomb.bridgeMass_toReal_bounds line 22
lemma OAI.CriticalHoneycomb.bridgeLaplace_summable line 33
theorem OAI.CriticalHoneycomb.bridgeLaplaceEstimate line 43
Source documentation
The height Laplace transform is comparable to s^(-3/4) for 0 < s ≤ 1.
```
theorem bridgeLaplaceEstimate : ∃ c C : ℝ, 0<c ∧ 0<C ∧ ∀ s : ℝ, 0<s → s≤1 →
    c*s^(-(3:ℝ)/4) ≤ bridgeLaplace s ∧ bridgeLaplace s ≤ C*s^(-(3:ℝ)/4) := by
…
```
Mentions: OAI.CriticalHoneycomb.bridgeLaplace