PhysicalMass.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Physical residual identities and strict bridge mass bounds

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

lemma OAI.CriticalHoneycomb.FiniteFunctional.F0_density_integrable line 20
lemma OAI.CriticalHoneycomb.FiniteFunctional.value_annihilates_F0 line 28
lemma OAI.CriticalHoneycomb.FiniteFunctional.value_eq_residual line 38
theorem OAI.CriticalHoneycomb.FiniteFunctional.source_physical_uneliminated_residual line 48
Source documentation
The physical bridge mass satisfies two residual equations before elimination of the scalar coefficient.
```
theorem source_physical_uneliminated_residual (N : ℕ) (hN : 1≤N) :
    ∃ (B : ℝ) (s : ℂ),0≤B ∧ bridgeMass N=ENNReal.ofReal B ∧
      2*(B:ℂ)=4*aStar*(obliqueResidual N hZero (-4)+s*obliqueResidual N hZero 0) ∧
      obliqueResidual N cThreeCorrection (-4)+s*obliqueResidual N cThreeCorrection 0=0 := by
…
```
Mentions: OAI.CriticalHoneycomb.bridgeMass, OAI.CriticalHoneycomb.FiniteFunctional.aStar, OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.hZero, OAI.CriticalHoneycomb.FiniteFunctional.cThreeCorrection
theorem OAI.CriticalHoneycomb.FiniteFunctional.source_physical_residual_formula line 70
Source documentation
The physical bridge mass equals the eliminated oblique residual expression when its denominator is nonzero.
```
theorem source_physical_residual_formula (N : ℕ) (hN : 1≤N)
    (hd : obliqueResidual N cThreeCorrection 0 ≠ 0) :
    ∃ B : ℝ,0≤B ∧ bridgeMass N=ENNReal.ofReal B ∧
      (B:ℂ)=2*aStar*(obliqueResidual N hZero (-4)-
        obliqueResidual N cThreeCorrection (-4)*obliqueResidual N hZero 0/
          obliqueResidual N cThreeCorrection 0) := by
…
```
Mentions: OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.cThreeCorrection, OAI.CriticalHoneycomb.bridgeMass, OAI.CriticalHoneycomb.FiniteFunctional.aStar, OAI.CriticalHoneycomb.FiniteFunctional.hZero
theorem OAI.CriticalHoneycomb.FiniteFunctional.physical_residual_formula line 94
Source documentation
The physical bridge mass equals an oblique residual expression.
```
theorem physical_residual_formula (N : ℕ) (hN : 1≤N) :
    ∃ B : ℝ,0≤B ∧ bridgeMass N=ENNReal.ofReal B ∧
      (B:ℂ)=2*aStar*(obliqueResidual N hZero (-4)-
        obliqueResidual N cThreeCorrection (-4)*obliqueResidual N hZero 0/
          obliqueResidual N cThreeCorrection 0) :=
…
```
Mentions: OAI.CriticalHoneycomb.bridgeMass, OAI.CriticalHoneycomb.FiniteFunctional.aStar, OAI.CriticalHoneycomb.FiniteFunctional.obliqueResidual, OAI.CriticalHoneycomb.FiniteFunctional.hZero, OAI.CriticalHoneycomb.FiniteFunctional.cThreeCorrection
lemma OAI.CriticalHoneycomb.FiniteFunctional.physical_real_residual_formula line 111
theorem OAI.CriticalHoneycomb.FiniteFunctional.physical_bridge_mass_upper line 124
Source documentation
An upper bound for the infinite strict bridge path sum.
```
theorem physical_bridge_mass_upper :
    ∃ A : ℝ,0<A ∧ ∀ᶠ N : ℕ in atTop,
      bridgeMass N≤ENNReal.ofReal (A*((N:ℝ)+1)^(-1/4:ℝ)) := by
…
```
Mentions: OAI.CriticalHoneycomb.bridgeMass
lemma OAI.CriticalHoneycomb.FiniteFunctional.corrected_bracket_lower line 162
theorem OAI.CriticalHoneycomb.FiniteFunctional.physical_bridge_mass_lower line 179
Source documentation
Matching lower estimate for the actual infinite strict-bridge path sum.
```
theorem physical_bridge_mass_lower :
    ∃ a : ℝ,0<a ∧ ∀ᶠ N : ℕ in atTop,
      ENNReal.ofReal (a*((N:ℝ)+1)^(-1/4:ℝ))≤bridgeMass N := by
…
```
Mentions: OAI.CriticalHoneycomb.bridgeMass