FirstPaperContextBox.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Literal boxed physical context transport

Auxiliary defect counts use the actual box and total-degree zero extension. The energy is exactly the bounded physical exchange graph energy. Endpoint masses and weighted means remain the literal completion-count sums.

lemma OAI.ContingencyTables.FirstPaperContextTransport.contextHard_nonnegative line 24

theorem OAI.ContingencyTables.FirstPaperContextTransport.context_box_transport line 34

Source documentation

The physical contextual transport inequality, with every auxiliary profile and energy endpoint restricted to the declared box and degree.

theorem context_box_transport (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ) (Ms : List ℕ)
    (e : (C ⊕ Coordinates Bool Ms) ≃ SmallView (fun a : I×J => small a.1 a.2))
    (σ mC : C → ℕ) (m z : Bool → ℕ) (R W : ℕ)
    (hprefix : InBox mC σ)
    (hlarge : ∀ i j, small i j=false → 2 ≤ B i j)
    (hlower : ∀ U ∈ Ms, 2 ≤ U) (hupper : ∀ U ∈ Ms, U ≤ W)
    (hz : InBox m z) (htotal : (∑ i, z i)=R+1)
    (H : (Coordinates Bool Ms → ℕ) → ℝ)
    (V : Finset (Coordinates Bool Ms → ℕ)) (hV : leafVertices Ms z ⊆ V)
    (hs : 0 < oneHole (eliminate Ms (contextHard small B r c L Ms e σ)) z false)
    (ht : 0 < oneHole (eliminate Ms (contextHard small B r c L Ms e σ)) z true) :
…

Mentions: OAI.ContingencyTables.FirstPaperContextTransport.contextHard