BoundedContradiction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.WeakPinned.arithmetic_no_bounded line 21

Source documentation

The bounded arithmetic regime is impossible as well. The embedding and normalization are chosen from the actual global mass and finite graph laws.

theorem arithmetic_no_bounded (hθ : 0<θ) (hγ : 0<γ) (hγ1 : γ<1) (hc : 0<c) (hcγ : c<γ)
    (hn : Tendsto (fun j => (Fintype.card (V j):ℝ)) atTop atTop)
    (hη : Tendsto η atTop (𝓝 0)) (hη0 : ∀ j,0≤η j) (hηb : ∀ j,η j≤θ/2)
    (hG : ∀ j,PreparedGraph (V j) (I j) (G j) θ γ c (η j))
    (t : ∀ j,I j → K j) (ht : ∀ j e y,y∈(G j).targets e →
      (Z₁ j ((G j).source e)-Z₁ j y)*(Z₂ j ((G j).source e)-Z₂ j y)=t j e)
    (C : ℝ) (hC : 0≤C) (hscale : ∀ j,overlapScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)+
      potentialScale (Z₁ j) (Z₂ j) (h₁ j) (h₂ j)≤C) : False := by
…

Mentions: OAI.WeakPinned.PreparedGraph, OAI.WeakPinned.overlapScale, OAI.WeakPinned.potentialScale