BridgeMass.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Uniform critical strict bridge mass estimates

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

def OAI.CriticalHoneycomb.verticalTrace line 18
Source documentation
Straight vertical bridge, parametrized by height minus one.
```
def verticalTrace : ℕ → List Center
  | 0 => [up 0 0,down 0 0]
  | n+1 => verticalTrace n ++ [up 0 (n+1),down 0 (n+1)]
```
Mentions: OAI.CriticalHoneycomb.Center, OAI.CriticalHoneycomb.up, OAI.CriticalHoneycomb.down
lemma OAI.CriticalHoneycomb.verticalTrace_bounds line 22
lemma OAI.CriticalHoneycomb.verticalTrace_last line 36
lemma OAI.CriticalHoneycomb.verticalTrace_head line 40
lemma OAI.CriticalHoneycomb.verticalTrace_nodup line 45
lemma OAI.CriticalHoneycomb.verticalTrace_chain line 57
def OAI.CriticalHoneycomb.straightBridge line 69
lemma OAI.CriticalHoneycomb.bridgeMass_pos line 76
def OAI.CriticalHoneycomb.FiniteBridgeMassEstimate line 96
Source documentation
Uniform two-sided bounds for the critical strict bridge path sum.
Also declared: ComparatorChallenges/HoneycombBridgeMassSupport.lean:66 (same declaration text).
```
def FiniteBridgeMassEstimate : Prop :=
…
```
lemma OAI.CriticalHoneycomb.finite_positive_bounds line 101
theorem OAI.CriticalHoneycomb.finiteBridgeMassEstimate line 114
Source documentation
The critical strict bridge mass is comparable to (1 + h)^(-1/4) at every height.
Distinct definitions of this name: ComparatorChallenges/HoneycombBridgeMassSupport.lean:72 (same statement text; different proof or body). Qualify references as OAI.CriticalHoneycomb.finiteBridgeMassEstimate@path.
```
theorem finiteBridgeMassEstimate : FiniteBridgeMassEstimate := by
…
```
Mentions: OAI.CriticalHoneycomb.FiniteBridgeMassEstimate