The five-observer path (A4)

Statements split from the original Statements.lean skeleton (one file per proving task). Everything in this file is proved; the order-t witness fivePath_witness and its expressible form live in InflationGraphOpen/FivePath.lean. See AUDIT-NOTES A4 for the mathematics.

FivePathAux collects the auxiliary material: the explicit enumeration of the 32 atoms and of the four sources of P₅, the decomposition of a GModel of P₅ into its four latent coordinates, and the analytic core of the bilocal inequality. Nothing in it changes any of the seven statements below, which appear in their original form.

Auxiliary material

def TriangleInflation.Graph.FivePathAux.fiveEquiv : Bool × Bool × Bool × Bool × Bool ≃ (Fin 5 → Bool)

Identify a five-bit tuple with a Boolean assignment on five vertices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TriangleInflation.Graph.FivePathAux.fiveEquiv_apply (p : Bool × Bool × Bool × Bool × Bool) : fiveEquiv p = ![p.1, p.2.1, p.2.2.1, p.2.2.2.1, p.2.2.2.2]

theorem TriangleInflation.Graph.FivePathAux.sum_five (F : (Fin 5 → Bool) → ℝ) : ∑ w : Fin 5 → Bool, F w = ∑ a : Bool, ∑ b : Bool, ∑ c : Bool, ∑ d : Bool, ∑ e : Bool, F ![a, b, c, d, e]

theorem TriangleInflation.Graph.FivePathAux.five_ind (q0 q1 q2 q3 q4 : ℝ) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then respMass q0 (w 0) * respMass q1 (w 1) * respMass q2 (w 2) * respMass q3 (w 3) * respMass q4 (w 4) else 0) = respMass q0 x * respMass q4 z

theorem TriangleInflation.Graph.FivePathAux.five_ind_sgn (q0 q1 q2 q3 q4 : ℝ) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * (respMass q0 (w 0) * respMass q1 (w 1) * respMass q2 (w 2) * respMass q3 (w 3) * respMass q4 (w 4)) else 0) = respMass q0 x * ((2 * q1 - 1) * (2 * q2 - 1) * (2 * q3 - 1)) * respMass q4 z

theorem TriangleInflation.Graph.FivePathAux.sqrt_cs {a b c d : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hc : 0 ≤ c) (hd : 0 ≤ d) : √(a * c) + √(b * d) ≤ √((a + b) * (c + d))

theorem TriangleInflation.Graph.FivePathAux.half_abs_add_le {u v : ℝ} (hu : |u| ≤ 1) (hv : |v| ≤ 1) : |(u + v) / 2| + |(u - v) / 2| ≤ 1

theorem TriangleInflation.Graph.FivePathAux.bilocal_core {Λ Λ' : Type} [Fintype Λ] [Fintype Λ'] (ν : Λ → ℝ) (ν' : Λ' → ℝ) (hν : IsLaw ν) (hν' : IsLaw ν') (b : Bool → Λ → ℝ) (c : Λ → Λ' → ℝ) (d : Bool → Λ' → ℝ) (hb : ∀ (x : Bool) (l : Λ), |b x l| ≤ 1) (hc : ∀ (l : Λ) (r : Λ'), |c l r| ≤ 1) (hd : ∀ (z : Bool) (r : Λ'), |d z r| ≤ 1) (f : Bool → Bool → ℝ) (hf : ∀ (x z : Bool), f x z = ∑ l : Λ, ∑ r : Λ', ν l * ν' r * (b x l * c l r * d z r)) : √|1 / 4 * ∑ x : Bool, ∑ z : Bool, f x z| + √|1 / 4 * ∑ x : Bool, ∑ z : Bool, sgn x * sgn z * f x z| ≤ 1

The analytic core of the bilocal inequality.

def TriangleInflation.Graph.FivePathAux.E01 : fivePathGraph.Edge

The source edge joining vertices zero and one.

Equations

• TriangleInflation.Graph.FivePathAux.E01 = ⟨s(0, 1), TriangleInflation.Graph.FivePathAux.E01._proof_1⟩

def TriangleInflation.Graph.FivePathAux.E12 : fivePathGraph.Edge

The source edge joining vertices one and two.

Equations

• TriangleInflation.Graph.FivePathAux.E12 = ⟨s(1, 2), TriangleInflation.Graph.FivePathAux.E12._proof_1⟩

def TriangleInflation.Graph.FivePathAux.E23 : fivePathGraph.Edge

The source edge joining vertices two and three.

Equations

• TriangleInflation.Graph.FivePathAux.E23 = ⟨s(2, 3), TriangleInflation.Graph.FivePathAux.E23._proof_1⟩

def TriangleInflation.Graph.FivePathAux.E34 : fivePathGraph.Edge

The source edge joining vertices three and four.

Equations

• TriangleInflation.Graph.FivePathAux.E34 = ⟨s(3, 4), TriangleInflation.Graph.FivePathAux.E34._proof_1⟩

theorem TriangleInflation.Graph.FivePathAux.edge_cases (e : fivePathGraph.Edge) : e = E01 ∨ e = E12 ∨ e = E23 ∨ e = E34

theorem TriangleInflation.Graph.FivePathAux.edge_univ : Finset.univ = {E01, E12, E23, E34}

theorem TriangleInflation.Graph.FivePathAux.inc0 (e : ↥(fivePathGraph.inc 0)) : ↑e = E01

theorem TriangleInflation.Graph.FivePathAux.inc1 (e : ↥(fivePathGraph.inc 1)) : ↑e = E01 ∨ ↑e = E12

theorem TriangleInflation.Graph.FivePathAux.inc2 (e : ↥(fivePathGraph.inc 2)) : ↑e = E12 ∨ ↑e = E23

theorem TriangleInflation.Graph.FivePathAux.inc3 (e : ↥(fivePathGraph.inc 3)) : ↑e = E23 ∨ ↑e = E34

theorem TriangleInflation.Graph.FivePathAux.inc4 (e : ↥(fivePathGraph.inc 4)) : ↑e = E34

theorem TriangleInflation.Graph.FivePathAux.prod_vert {β : Type u_1} [CommMonoid β] (g : fivePathGraph.V → β) : ∏ v : fivePathGraph.V, g v = g 0 * g 1 * g 2 * g 3 * g 4

theorem TriangleInflation.Graph.FivePathAux.prod_edge {β : Type u_1} [CommMonoid β] (g : fivePathGraph.Edge → β) : ∏ e : fivePathGraph.Edge, g e = g E01 * g E12 * g E23 * g E34

@[reducible, inline]

abbrev TriangleInflation.Graph.FivePathAux.GTup (M : GModel fivePathGraph) : Type

The latent tuple type of the five-path.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.FivePathAux.ofTup (M : GModel fivePathGraph) (p : GTup M) (e : fivePathGraph.Edge) : M.L e

The latent assignment built from a tuple.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TriangleInflation.Graph.FivePathAux.ofTup_E01 (M : GModel fivePathGraph) (p : GTup M) : ofTup M p E01 = p.1

@[simp]

theorem TriangleInflation.Graph.FivePathAux.ofTup_E12 (M : GModel fivePathGraph) (p : GTup M) : ofTup M p E12 = p.2.1

@[simp]

theorem TriangleInflation.Graph.FivePathAux.ofTup_E23 (M : GModel fivePathGraph) (p : GTup M) : ofTup M p E23 = p.2.2.1

@[simp]

theorem TriangleInflation.Graph.FivePathAux.ofTup_E34 (M : GModel fivePathGraph) (p : GTup M) : ofTup M p E34 = p.2.2.2

theorem TriangleInflation.Graph.FivePathAux.tup_congr (M : GModel fivePathGraph) {x y : (e : fivePathGraph.Edge) → M.L e} {f g : fivePathGraph.Edge} (h : f = g) (hxy : x g = y g) : x f = y f

Transport an equality of latent assignments along an equality of edges.

def TriangleInflation.Graph.FivePathAux.latEquiv (M : GModel fivePathGraph) : GTup M ≃ ((e : fivePathGraph.Edge) → M.L e)

Identify the four latent coordinates with an assignment to the path edges.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.FivePathAux.sum_lat (M : GModel fivePathGraph) (F : ((e : fivePathGraph.Edge) → M.L e) → ℝ) : ∑ x : (e : fivePathGraph.Edge) → M.L e, F x = ∑ a : M.L E01, ∑ b : M.L E12, ∑ c : M.L E23, ∑ d : M.L E34, F (ofTup M (a, b, c, d))

def TriangleInflation.Graph.FivePathAux.gResp (M : GModel fivePathGraph) (v : fivePathGraph.V) (p : GTup M) : ℝ

The response at a vertex, as a function of the whole latent tuple.

Equations

• TriangleInflation.Graph.FivePathAux.gResp M v p = M.resp v fun (e : ↥(TriangleInflation.Graph.fivePathGraph.inc v)) => TriangleInflation.Graph.FivePathAux.ofTup M p ↑e

def TriangleInflation.Graph.FivePathAux.fA (M : GModel fivePathGraph) (q : GTup M) (a : M.L E01) : ℝ

Response at the first endpoint, with the remaining coordinates fixed by q.

Equations

• TriangleInflation.Graph.FivePathAux.fA M q a = TriangleInflation.Graph.FivePathAux.gResp M 0 (a, q.2.1, q.2.2.1, q.2.2.2)

def TriangleInflation.Graph.FivePathAux.fB (M : GModel fivePathGraph) (q : GTup M) (a : M.L E01) (b : M.L E12) : ℝ

Response at vertex one, with the remaining coordinates fixed by q.

Equations

• TriangleInflation.Graph.FivePathAux.fB M q a b = TriangleInflation.Graph.FivePathAux.gResp M 1 (a, b, q.2.2.1, q.2.2.2)

def TriangleInflation.Graph.FivePathAux.fC (M : GModel fivePathGraph) (q : GTup M) (b : M.L E12) (c : M.L E23) : ℝ

Response at the middle vertex, with the remaining coordinates fixed by q.

Equations

• TriangleInflation.Graph.FivePathAux.fC M q b c = TriangleInflation.Graph.FivePathAux.gResp M 2 (q.1, b, c, q.2.2.2)

def TriangleInflation.Graph.FivePathAux.fD (M : GModel fivePathGraph) (q : GTup M) (c : M.L E23) (d : M.L E34) : ℝ

Response at vertex three, with the remaining coordinates fixed by q.

Equations

• TriangleInflation.Graph.FivePathAux.fD M q c d = TriangleInflation.Graph.FivePathAux.gResp M 3 (q.1, q.2.1, c, d)

def TriangleInflation.Graph.FivePathAux.fE (M : GModel fivePathGraph) (q : GTup M) (d : M.L E34) : ℝ

Response at the last endpoint, with the remaining coordinates fixed by q.

Equations

• TriangleInflation.Graph.FivePathAux.fE M q d = TriangleInflation.Graph.FivePathAux.gResp M 4 (q.1, q.2.1, q.2.2.1, d)

theorem TriangleInflation.Graph.FivePathAux.gResp0 (M : GModel fivePathGraph) (q p : GTup M) : gResp M 0 p = fA M q p.1

theorem TriangleInflation.Graph.FivePathAux.gResp1 (M : GModel fivePathGraph) (q p : GTup M) : gResp M 1 p = fB M q p.1 p.2.1

theorem TriangleInflation.Graph.FivePathAux.gResp2 (M : GModel fivePathGraph) (q p : GTup M) : gResp M 2 p = fC M q p.2.1 p.2.2.1

theorem TriangleInflation.Graph.FivePathAux.gResp3 (M : GModel fivePathGraph) (q p : GTup M) : gResp M 3 p = fD M q p.2.2.1 p.2.2.2

theorem TriangleInflation.Graph.FivePathAux.gResp4 (M : GModel fivePathGraph) (q p : GTup M) : gResp M 4 p = fE M q p.2.2.2

theorem TriangleInflation.Graph.FivePathAux.law_eq (M : GModel fivePathGraph) (q : GTup M) (w : fivePathGraph.V → Bool) : M.law w = ∑ a : M.L E01, ∑ b : M.L E12, ∑ c : M.L E23, ∑ d : M.L E34, M.μ E01 a * M.μ E12 b * M.μ E23 c * M.μ E34 d * (respMass (fA M q a) (w 0) * respMass (fB M q a b) (w 1) * respMass (fC M q b c) (w 2) * respMass (fD M q c d) (w 3) * respMass (fE M q d) (w 4))

theorem TriangleInflation.Graph.FivePathAux.cell_step (M : GModel fivePathGraph) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then M.law w else 0) = ∑ X : (e : fivePathGraph.Edge) → M.L e, (∏ e : fivePathGraph.Edge, M.μ e (X e)) * (respMass (M.resp 0 fun (e : ↥(fivePathGraph.inc 0)) => X ↑e) x * respMass (M.resp 4 fun (e : ↥(fivePathGraph.inc 4)) => X ↑e) z)

theorem TriangleInflation.Graph.FivePathAux.num_step (M : GModel fivePathGraph) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * M.law w else 0) = ∑ X : (e : fivePathGraph.Edge) → M.L e, (∏ e : fivePathGraph.Edge, M.μ e (X e)) * (respMass (M.resp 0 fun (e : ↥(fivePathGraph.inc 0)) => X ↑e) x * (((2 * M.resp 1 fun (e : ↥(fivePathGraph.inc 1)) => X ↑e) - 1) * ((2 * M.resp 2 fun (e : ↥(fivePathGraph.inc 2)) => X ↑e) - 1) * ((2 * M.resp 3 fun (e : ↥(fivePathGraph.inc 3)) => X ↑e) - 1)) * respMass (M.resp 4 fun (e : ↥(fivePathGraph.inc 4)) => X ↑e) z)

theorem TriangleInflation.Graph.FivePathAux.respMass_nonneg {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) (b : Bool) : 0 ≤ respMass r b

theorem TriangleInflation.Graph.FivePathAux.sgnResp_abs_le {r : ℝ} (h0 : 0 ≤ r) (h1 : r ≤ 1) : |2 * r - 1| ≤ 1

theorem TriangleInflation.Graph.FivePathAux.sum4_factor {A B C D : Type} [Fintype A] [Fintype B] [Fintype C] [Fintype D] (f : A → ℝ) (g : B → ℝ) (h : C → ℝ) (k : D → ℝ) (F : A → ℝ) (K : D → ℝ) (hg : ∑ b : B, g b = 1) (hh : ∑ c : C, h c = 1) : ∑ a : A, ∑ b : B, ∑ c : C, ∑ d : D, f a * g b * h c * k d * (F a * K d) = (∑ a : A, f a * F a) * ∑ d : D, k d * K d

Factoring a four-fold latent sum whose summand depends only on the outer coordinates.

theorem TriangleInflation.Graph.FivePathAux.sum4_chain {A B C D : Type} [Fintype A] [Fintype B] [Fintype C] [Fintype D] (f : A → ℝ) (g : B → ℝ) (h : C → ℝ) (k : D → ℝ) (F : A → ℝ) (K : D → ℝ) (BB : A → B → ℝ) (CC : B → C → ℝ) (DD : C → D → ℝ) : ∑ a : A, ∑ b : B, ∑ c : C, ∑ d : D, f a * g b * h c * k d * (F a * (BB a b * CC b c * DD c d) * K d) = ∑ b : B, ∑ c : C, g b * h c * ((∑ a : A, f a * F a * BB a b) * CC b c * ∑ d : D, k d * K d * DD c d)

Factoring a four-fold latent sum with a chain-shaped summand.

theorem TriangleInflation.Graph.FivePathAux.cell_eq (M : GModel fivePathGraph) (q : GTup M) (hM : M.Valid) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then M.law w else 0) = (∑ a : M.L E01, M.μ E01 a * respMass (fA M q a) x) * ∑ d : M.L E34, M.μ E34 d * respMass (fE M q d) z

theorem TriangleInflation.Graph.FivePathAux.num_eq (M : GModel fivePathGraph) (q : GTup M) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * M.law w else 0) = ∑ b : M.L E12, ∑ c : M.L E23, M.μ E12 b * M.μ E23 c * ((∑ a : M.L E01, M.μ E01 a * respMass (fA M q a) x * (2 * fB M q a b - 1)) * (2 * fC M q b c - 1) * ∑ d : M.L E34, M.μ E34 d * respMass (fE M q d) z * (2 * fD M q c d - 1))

theorem TriangleInflation.Graph.FivePathAux.wsum_abs_le {A : Type} [Fintype A] (f g : A → ℝ) (hf : ∀ (a : A), 0 ≤ f a) (hg : ∀ (a : A), |g a| ≤ 1) : |∑ a : A, f a * g a| ≤ ∑ a : A, f a

theorem TriangleInflation.Graph.FivePathAux.latent_nonempty (M : GModel fivePathGraph) (hM : M.Valid) (e : fivePathGraph.Edge) : Nonempty (M.L e)

def TriangleInflation.Graph.FivePathAux.alphaW (M : GModel fivePathGraph) (q : GTup M) (x : Bool) : ℝ

The endpoint weight Pr(A = x) of the model.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.FivePathAux.epsiW (M : GModel fivePathGraph) (q : GTup M) (z : Bool) : ℝ

The endpoint weight Pr(E = z) of the model.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.FivePathAux.betaW (M : GModel fivePathGraph) (q : GTup M) (x : Bool) (b : M.L E12) : ℝ

The unnormalized conditional response of B.

Equations

• One or more equations did not get rendered due to their size.

def TriangleInflation.Graph.FivePathAux.deltaW (M : GModel fivePathGraph) (q : GTup M) (z : Bool) (c : M.L E23) : ℝ

The unnormalized conditional response of D.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.FivePathAux.cell_eq' (M : GModel fivePathGraph) (q : GTup M) (hM : M.Valid) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then M.law w else 0) = alphaW M q x * epsiW M q z

theorem TriangleInflation.Graph.FivePathAux.num_eq' (M : GModel fivePathGraph) (q : GTup M) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * M.law w else 0) = ∑ b : M.L E12, ∑ c : M.L E23, M.μ E12 b * M.μ E23 c * (betaW M q x b * (2 * fC M q b c - 1) * deltaW M q z c)

The explicit target

theorem TriangleInflation.Graph.FivePathAux.fivePathTarget_ge (h : ℝ) (hh : 0 ≤ h) (w : Fin 5 → Bool) : (1 - h) / 64 ≤ fivePathTarget h w

theorem TriangleInflation.Graph.FivePathAux.target_sum (h : ℝ) : ∑ w : Fin 5 → Bool, fivePathTarget h w = 1

theorem TriangleInflation.Graph.FivePathAux.target_cell (h : ℝ) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then fivePathTarget h w else 0) = 1 / 4

theorem TriangleInflation.Graph.FivePathAux.target_num (h : ℝ) (x z : Bool) : (∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * fivePathTarget h w else 0) = 1 / 4 * ((1 + h) / 4 * (1 + sgn x * sgn z))

theorem TriangleInflation.Graph.FivePathAux.target_corr (h : ℝ) (x z : Bool) : fivePathCorr (fivePathTarget h) x z = (1 + h) / 4 * (1 + sgn x * sgn z)

Laws of models, and a compatible law

theorem TriangleInflation.Graph.FivePathAux.five_tot (q0 q1 q2 q3 q4 : ℝ) : ∑ w : Fin 5 → Bool, respMass q0 (w 0) * respMass q1 (w 1) * respMass q2 (w 2) * respMass q3 (w 3) * respMass q4 (w 4) = 1

theorem TriangleInflation.Graph.FivePathAux.sum4_one {A B C D : Type} [Fintype A] [Fintype B] [Fintype C] [Fintype D] (f : A → ℝ) (g : B → ℝ) (h : C → ℝ) (k : D → ℝ) (hf : ∑ a : A, f a = 1) (hg : ∑ b : B, g b = 1) (hh : ∑ c : C, h c = 1) (hk : ∑ d : D, k d = 1) : ∑ a : A, ∑ b : B, ∑ c : C, ∑ d : D, f a * g b * h c * k d = 1

theorem TriangleInflation.Graph.FivePathAux.model_isLaw (M : GModel fivePathGraph) (hM : M.Valid) : IsLaw M.law

noncomputable def TriangleInflation.Graph.FivePathAux.trivModel : GModel fivePathGraph

The five-path model with trivial sources and fair responses.

Equations

• One or more equations did not get rendered due to their size.

theorem TriangleInflation.Graph.FivePathAux.trivModel_valid : trivModel.Valid

theorem TriangleInflation.Graph.FivePathAux.exists_compatible : ∃ (Q : GTarget fivePathGraph), GCompatible fivePathGraph Q

theorem TriangleInflation.Graph.FivePathAux.tv_bound (P Q G : (Fin 5 → Bool) → ℝ) (hG : ∀ (w : Fin 5 → Bool), |G w| ≤ 1) (x z : Bool) : |(∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then G w * Q w else 0) - ∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then G w * P w else 0| ≤ 2 * dTV P Q

A conditional-cell functional moves by at most twice the total variation distance.

theorem TriangleInflation.Graph.FivePathAux.sgn3_abs_le (w : Fin 5 → Bool) : |sgn (w 1) * sgn (w 2) * sgn (w 3)| ≤ 1

theorem TriangleInflation.Graph.FivePathAux.dTV_nonneg {α : Type u_1} [Fintype α] (P Q : α → ℝ) : 0 ≤ dTV P Q

theorem TriangleInflation.Graph.FivePathAux.tv_cell (P Q : (Fin 5 → Bool) → ℝ) (x z : Bool) : |(∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then Q w else 0) - ∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then P w else 0| ≤ 2 * dTV P Q

theorem TriangleInflation.Graph.FivePathAux.tv_num (P Q : (Fin 5 → Bool) → ℝ) (x z : Bool) : |(∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * Q w else 0) - ∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then sgn (w 1) * sgn (w 2) * sgn (w 3) * P w else 0| ≤ 2 * dTV P Q

theorem TriangleInflation.Graph.FivePathAux.fivePathI_expand (R : (Fin 5 → Bool) → ℝ) : fivePathI R = 1 / 4 * (fivePathCorr R false false + fivePathCorr R false true + (fivePathCorr R true false + fivePathCorr R true true))

theorem TriangleInflation.Graph.FivePathAux.fivePathJ_expand (R : (Fin 5 → Bool) → ℝ) : fivePathJ R = 1 / 4 * (fivePathCorr R false false - fivePathCorr R false true + (-fivePathCorr R true false + fivePathCorr R true true))

theorem TriangleInflation.Graph.FivePathAux.targetCorr_bounds (h : ℝ) (h1 : h < 1) (h0 : 0 ≤ h) (x z : Bool) : 0 ≤ (1 + h) / 4 * (1 + sgn x * sgn z) ∧ (1 + h) / 4 * (1 + sgn x * sgn z) ≤ 1

theorem TriangleInflation.Graph.FivePathAux.sqrt_quarter : √(1 / 4) = 1 / 2

A4: the five-observer path

theorem TriangleInflation.Graph.bilocal_of_compatible (P : GTarget fivePathGraph) (hP : IsLaw P) (hc : GCompatible fivePathGraph P) (hcell : ∀ (x z : Bool), 0 < ∑ w : Fin 5 → Bool, if w 0 = x ∧ w 4 = z then P w else 0) : √|fivePathI P| + √|fivePathJ P| ≤ 1

AUDIT-NOTES A4, the bilocal inequality for the five-path. For a compatible law with positive endpoint cells, √|I| + √|J| ≤ 1. Conditioning on A = x and E = z changes only the endpoint source laws and leaves L, R independent; with p_± = E_L|(b_0 ± b_1)/2| and r_± = E_R|(d_0 ± d_1)/2| one has p_+ + p_- ≤ 1, r_+ + r_- ≤ 1, |I| ≤ p_+ r_+, |J| ≤ p_- r_-, and Cauchy–Schwarz finishes.

theorem TriangleInflation.Graph.fivePathTarget_isLaw (h : ℝ) (h0 : 0 ≤ h) (h1 : h < 1) : IsLaw (fivePathTarget h) ∧ ∀ (w : Fin 5 → Bool), (1 - h) / 64 ≤ fivePathTarget h w

The five-path target is a law, and is bounded below by (1−h)/64 at every atom (AUDIT-NOTES A4, packet equation (8)).

theorem TriangleInflation.Graph.fivePathTarget_corr (h : ℝ) : fivePathI (fivePathTarget h) = (1 + h) / 4 ∧ fivePathJ (fivePathTarget h) = (1 + h) / 4

AUDIT-NOTES A4, the correlators of the target: f_{xz} = (1+h)/2 when x = z and 0 otherwise, so I = J = (1+h)/4.

theorem TriangleInflation.Graph.fivePath_not_compatible (h : ℝ) (h0 : 0 < h) (h1 : h < 1) : ¬GCompatible fivePathGraph (fivePathTarget h)

AUDIT-NOTES A4: the five-path target is incompatible for every 0 < h < 1, since √I + √J = √(1+h) > 1 contradicts the bilocal inequality. (Finite-latent compatible set; see the header.)

theorem TriangleInflation.Graph.fivePath_distance (h : ℝ) (h0 : 0 < h) (h1 : h < 1) : h / 96 ≤ distToCompatible fivePathGraph (fivePathTarget h)

AUDIT-NOTES A4 with the corrected constant. The packet states d_TV ≥ h/16; the argument as written gives |I_R − I_P|, |J_R − J_P| ≤ 24 d for d < 1/8, so the safe constant is h/96. At h_t = 1/(16t²) this is 1/(1536 t²).