The five-path witness at every order

AUDIT-NOTES A4 / Theorem thm:fivepath: the order-t witness fivePath_witness for the five-path target with h = 1/(16t²), built as the inflated law of a complex-weighted pair-source model, and its recursively expressible form. Everything here is proved.

Complex weights

def TriangleInflation.Graph.P5WitnessAux.cpush {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (w : α → ℂ) (F : α → β) : β → ℂ

Pushforward of a complex weight function.

Equations

• TriangleInflation.Graph.P5WitnessAux.cpush w F b = ∑ a : α, if F a = b then w a else 0

def TriangleInflation.Graph.P5WitnessAux.cprodLaw {ι : Type u_1} [Fintype ι] (w : ι → Bool → ℂ) : (ι → Bool) → ℂ

Product of independent complex per-coordinate weights on ι → Bool.

Equations

• TriangleInflation.Graph.P5WitnessAux.cprodLaw w x = ∏ i : ι, w i (x i)

def TriangleInflation.Graph.P5WitnessAux.crespMass (q : ℂ) : Bool → ℂ

respMass with a complex response weight.

Equations

• TriangleInflation.Graph.P5WitnessAux.crespMass q b = if b = true then 1 - q else q

theorem TriangleInflation.Graph.P5WitnessAux.crespMass_ofReal (q : ℝ) (b : Bool) : crespMass (↑q) b = ↑(respMass q b)

theorem TriangleInflation.Graph.P5WitnessAux.crespMass_sum (q : ℂ) : ∑ b : Bool, crespMass q b = 1

theorem TriangleInflation.Graph.P5WitnessAux.cpush_re {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (w : α → ℂ) (F : α → β) (b : β) : (cpush w F b).re = pushforward (fun (a : α) => (w a).re) F b

Generic finite-sum toolkit, complex weights

theorem TriangleInflation.Graph.P5WitnessAux.sum_pi_prod {κ : Type u_1} [Fintype κ] [DecidableEq κ] {A : κ → Type u_2} [(k : κ) → Fintype (A k)] (f : (k : κ) → A k → ℂ) : ∑ x : (k : κ) → A k, ∏ k : κ, f k (x k) = ∏ k : κ, ∑ a : A k, f k a

theorem TriangleInflation.Graph.P5WitnessAux.ite_funext_prod {κ : Type u_1} [Fintype κ] {B : κ → Type u_2} [(k : κ) → DecidableEq (B k)] (f g : (k : κ) → B k) : (if f = g then 1 else 0) = ∏ k : κ, if f k = g k then 1 else 0

theorem TriangleInflation.Graph.P5WitnessAux.sum_dprod_sel {κ : Type u_1} [Fintype κ] [DecidableEq κ] {A : κ → Type u_2} {B : κ → Type u_3} [(k : κ) → Fintype (A k)] [(k : κ) → DecidableEq (B k)] (W : (k : κ) → A k → ℂ) (sel : (k : κ) → A k → B k) (y : (k : κ) → B k) : ∑ x : (k : κ) → A k, (if (fun (k : κ) => sel k (x k)) = y then 1 else 0) * ∏ k : κ, W k (x k) = ∏ k : κ, ∑ a : A k, (if sel k a = y k then 1 else 0) * W k a

theorem TriangleInflation.Graph.P5WitnessAux.sum_mul_comp {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq β] (w : α → ℂ) (F : α → β) (G : β → ℂ) : ∑ a : α, w a * G (F a) = ∑ b : β, cpush w F b * G b

theorem TriangleInflation.Graph.P5WitnessAux.cpush_comp_equiv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Fintype α] [DecidableEq β] [DecidableEq γ] (w : α → ℂ) (F : α → β) (E : β ≃ γ) : (cpush w fun (a : α) => E (F a)) = fun (c : γ) => cpush w F (E.symm c)

theorem TriangleInflation.Graph.P5WitnessAux.cpush_mix {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] {ι : Type u_4} [Fintype ι] (c : ι → ℂ) (ν : ι → α → ℂ) (F : α → β) : cpush (fun (a : α) => ∑ i : ι, c i * ν i a) F = fun (b : β) => ∑ i : ι, c i * cpush (ν i) F b

Marginals of a product weight along an injective selection

theorem TriangleInflation.Graph.P5WitnessAux.cpush_prodLaw_sel {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] {w : ι → Bool → ℂ} (hw : ∀ (i : ι), ∑ b : Bool, w i b = 1) {ν : κ → ι} (hν : Function.Injective ν) : (cpush (cprodLaw w) fun (x : ι → Bool) (k : κ) => x (ν k)) = cprodLaw fun (k : κ) => w (ν k)

Independence of functions of disjoint coordinate blocks

def TriangleInflation.Graph.P5WitnessAux.dprod {ι : Type u_1} [Fintype ι] {A : ι → Type u_2} (w : (i : ι) → A i → ℂ) (x : (i : ι) → A i) : ℂ

The complex product weight of independent coordinates with dependent alphabets.

Equations

• TriangleInflation.Graph.P5WitnessAux.dprod w x = ∏ i : ι, w i (x i)

theorem TriangleInflation.Graph.P5WitnessAux.sum_dprod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → ℂ} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) : ∑ x : (i : ι) → A i, dprod w x = 1

def TriangleInflation.Graph.P5WitnessAux.dmix {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} (I : Finset ι) (x y : (i : ι) → A i) (i : ι) : A i

dmix I x y takes its I-coordinates from x and the others from y.

Equations

• TriangleInflation.Graph.P5WitnessAux.dmix I x y i = if i ∈ I then x i else y i

theorem TriangleInflation.Graph.P5WitnessAux.dmix_mem {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {I : Finset ι} {x y : (i : ι) → A i} {i : ι} (hi : i ∈ I) : dmix I x y i = x i

theorem TriangleInflation.Graph.P5WitnessAux.dmix_not_mem {ι : Type u_1} [DecidableEq ι] {A : ι → Type u_2} {I : Finset ι} {x y : (i : ι) → A i} {i : ι} (hi : i ∉ I) : dmix I x y i = y i

theorem TriangleInflation.Graph.P5WitnessAux.dprod_dmix_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} {w : (i : ι) → A i → ℂ} (I : Finset ι) (x y : (i : ι) → A i) : dprod w (dmix I x y) * dprod w (dmix I y x) = dprod w x * dprod w y

theorem TriangleInflation.Graph.P5WitnessAux.sum_dprod_mul_mul {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → ℂ} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) {I J : Finset ι} (hIJ : Disjoint I J) {φ ψ : ((i : ι) → A i) → ℂ} (hφ : ∀ (x y : (i : ι) → A i), (∀ i ∈ I, x i = y i) → φ x = φ y) (hψ : ∀ (x y : (i : ι) → A i), (∀ i ∈ J, x i = y i) → ψ x = ψ y) : ∑ x : (i : ι) → A i, dprod w x * (φ x * ψ x) = (∑ x : (i : ι) → A i, dprod w x * φ x) * ∑ x : (i : ι) → A i, dprod w x * ψ x

theorem TriangleInflation.Graph.P5WitnessAux.sum_dprod_prod {ι : Type u_1} [Fintype ι] [DecidableEq ι] {A : ι → Type u_2} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → ℂ} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) {n : ℕ} (I : Fin n → Finset ι) (χ : Fin n → ((i : ι) → A i) → ℂ) : (∀ (m m' : Fin n), m ≠ m' → Disjoint (I m) (I m')) → (∀ (m : Fin n) (x y : (i : ι) → A i), (∀ i ∈ I m, x i = y i) → χ m x = χ m y) → ∑ x : (i : ι) → A i, dprod w x * ∏ m : Fin n, χ m x = ∏ m : Fin n, ∑ x : (i : ι) → A i, dprod w x * χ m x

theorem TriangleInflation.Graph.P5WitnessAux.sum_sel_coord {B : Type u_1} [Fintype B] [DecidableEq B] {n : Type u_2} [Fintype n] [DecidableEq n] (ρ : B → ℂ) (hρ : ∑ b : B, ρ b = 1) (r₀ : n) (b₀ : B) : ∑ v : n → B, (if v r₀ = b₀ then 1 else 0) * ∏ r : n, ρ (v r) = ρ b₀

The complex-weighted model and its inflation witness

structure TriangleInflation.Graph.P5WitnessAux.CModel (Γ : PairGraph) : Type 1

A pair-source model with complex source weights and complex response weights. Only the normalization ∑ μ e = 1 is required; positivity is not part of the algebra.

• L : Γ.Edge → Type

  The latent alphabet of each source.

• fintypeL (e : Γ.Edge) : Fintype (self.L e)
• μ (e : Γ.Edge) : self.L e → ℂ

  The complex weight of each source.

• resp (v : Γ.V) : ((e : ↥(Γ.inc v)) → self.L ↑e) → ℂ

  The complex weight of the outcome false at v.

def TriangleInflation.Graph.P5WitnessAux.CModel.Valid {Γ : PairGraph} (M : CModel Γ) : Prop

A complex model is normalized when every source weight sums to one.

Equations

• M.Valid = ∀ (e : Γ.Edge), ∑ a : M.L e, M.μ e a = 1

def TriangleInflation.Graph.P5WitnessAux.CModel.law {Γ : PairGraph} (M : CModel Γ) : (Γ.V → Bool) → ℂ

The observed complex law of a complex model.

Equations

• M.law w = ∑ x : (e : Γ.Edge) → M.L e, (∏ e : Γ.Edge, M.μ e (x e)) * ∏ v : Γ.V, TriangleInflation.Graph.P5WitnessAux.crespMass (M.resp v fun (e : ↥(Γ.inc v)) => x ↑e) (w v)

@[reducible, inline]

abbrev TriangleInflation.Graph.P5WitnessAux.CCfg {Γ : PairGraph} (M : CModel Γ) (t : ℕ) : Type

Latent configurations of the order-t inflation.

Equations

• TriangleInflation.Graph.P5WitnessAux.CCfg M t = ((l : TriangleInflation.Graph.GLatent Γ t) → M.L l.1)

@[reducible, inline]

abbrev TriangleInflation.Graph.P5WitnessAux.CMCfg {Γ : PairGraph} (M : CModel Γ) : Type

Latent configurations of the model itself.

Equations

• TriangleInflation.Graph.P5WitnessAux.CMCfg M = ((e : Γ.Edge) → M.L e)

def TriangleInflation.Graph.P5WitnessAux.cObsResp {Γ : PairGraph} {t : ℕ} (M : CModel Γ) (o : GObs Γ t) (x : CCfg M t) : ℂ

The response weight of a copied observation under a copied latent configuration.

Equations

• TriangleInflation.Graph.P5WitnessAux.cObsResp M o x = M.resp o.fst fun (e : ↥(Γ.inc o.fst)) => x (↑e, o.snd e)

def TriangleInflation.Graph.P5WitnessAux.cInflCond {Γ : PairGraph} {t : ℕ} (M : CModel Γ) (x : CCfg M t) : GObs Γ t → Bool → ℂ

The conditional per-observation weights of the inflated model.

Equations

• TriangleInflation.Graph.P5WitnessAux.cInflCond M x o b = TriangleInflation.Graph.P5WitnessAux.crespMass (TriangleInflation.Graph.P5WitnessAux.cObsResp M o x) b

def TriangleInflation.Graph.P5WitnessAux.ccfgW {Γ : PairGraph} (M : CModel Γ) (t : ℕ) : CCfg M t → ℂ

The weight of a copied latent configuration.

Equations

• TriangleInflation.Graph.P5WitnessAux.ccfgW M t = TriangleInflation.Graph.P5WitnessAux.dprod fun (l : TriangleInflation.Graph.GLatent Γ t) (a : M.L l.1) => M.μ l.1 a

def TriangleInflation.Graph.P5WitnessAux.cmcfgW {Γ : PairGraph} (M : CModel Γ) : CMCfg M → ℂ

The weight of a latent configuration of the model.

Equations

• TriangleInflation.Graph.P5WitnessAux.cmcfgW M = TriangleInflation.Graph.P5WitnessAux.dprod fun (e : Γ.Edge) (a : M.L e) => M.μ e a

def TriangleInflation.Graph.P5WitnessAux.cInflLaw {Γ : PairGraph} (M : CModel Γ) (t : ℕ) : GAssign Γ t → ℂ

The order-t inflation witness of a complex model.

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.cInflCond_sum {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (x : CCfg M t) (o : GObs Γ t) : ∑ b : Bool, cInflCond M x o b = 1

theorem TriangleInflation.Graph.P5WitnessAux.sum_ccfgW {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (hM : M.Valid) : ∑ x : CCfg M t, ccfgW M t x = 1

theorem TriangleInflation.Graph.P5WitnessAux.sum_cprodLaw {ι : Type u_1} [Fintype ι] [DecidableEq ι] {w : ι → Bool → ℂ} (hw : ∀ (i : ι), ∑ b : Bool, w i b = 1) : ∑ x : ι → Bool, cprodLaw w x = 1

theorem TriangleInflation.Graph.P5WitnessAux.cpush_cInflLaw {Γ : PairGraph} {t : ℕ} {M : CModel Γ} {β : Type u_1} [DecidableEq β] (F : GAssign Γ t → β) : cpush (cInflLaw M t) F = fun (b : β) => ∑ x : CCfg M t, ccfgW M t x * cpush (cprodLaw (cInflCond M x)) F b

theorem TriangleInflation.Graph.P5WitnessAux.clatent_marginal {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (hM : M.Valid) (ι : Γ.Edge → Fin t) (F : CMCfg M → ℂ) : (∑ x : CCfg M t, ccfgW M t x * F fun (e : Γ.Edge) => x (e, ι e)) = ∑ y : CMCfg M, cmcfgW M y * F y

Marginalizing the copied latent configuration onto one copy of the original scenario.

def TriangleInflation.Graph.P5WitnessAux.cCfgPerm {Γ : PairGraph} {t : ℕ} (M : CModel Γ) (π : Γ.Edge → Equiv.Perm (Fin t)) : CCfg M t ≃ CCfg M t

Relabelling copy indices, as a bijection of copied latent configurations.

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.sum_cInflLaw {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (hM : M.Valid) : ∑ ω : GAssign Γ t, cInflLaw M t ω = 1

theorem TriangleInflation.Graph.P5WitnessAux.csymmetric_cInflLaw {Γ : PairGraph} (M : CModel Γ) (t : ℕ) (π : Γ.Edge → Equiv.Perm (Fin t)) (ω : GAssign Γ t) : cInflLaw M t (gRelabel π ω) = cInflLaw M t ω

The complex witness is symmetric under per-source relabelling of the copies.

theorem TriangleInflation.Graph.P5WitnessAux.cInflLaw_block {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (S : Finset (GObs Γ t)) (φ : ↥S → Bool) : cpush (cInflLaw M t) (gRestrict S) φ = ∑ x : CCfg M t, ccfgW M t x * ∏ o : ↥S, crespMass (cObsResp M (↑o) x) (φ o)

The marginal of the complex witness on a block of copied observations.

theorem TriangleInflation.Graph.P5WitnessAux.cInflLaw_injectable {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (hM : M.Valid) {S : Finset (GObs Γ t)} (hS : GInjectable S) : cpush (cInflLaw M t) (gRestrict S) = cpush M.law (gPartyRead S)

Every injectable set carries the corresponding marginal of the complex model's law.

theorem TriangleInflation.Graph.P5WitnessAux.cInflLaw_ai {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (hM : M.Valid) (n : ℕ) (S : Fin n → Finset (GObs Γ t)) (hinj : ∀ (m : Fin n), GInjectable (S m)) (hai : ∀ (m m' : Fin n), m ≠ m' → GAncestrallyIndependent (S m) (S m')) : (cpush (cInflLaw M t) fun (ω : GAssign Γ t) (m : Fin n) => gRestrict (S m) ω) = fun (φ : (m : Fin n) → ↥(S m) → Bool) => ∏ m : Fin n, cpush M.law (gPartyRead (S m)) (φ m)

The complex witness satisfies every ancestral-independence prescription.

def TriangleInflation.Graph.P5WitnessAux.cTensorPow {Γ : PairGraph} (t : ℕ) (P : (Γ.V → Bool) → ℂ) : (Fin t → Γ.V → Bool) → ℂ

The t-fold tensor power of a complex target law.

Equations

• TriangleInflation.Graph.P5WitnessAux.cTensorPow t P v = ∏ r : Fin t, P (v r)

theorem TriangleInflation.Graph.P5WitnessAux.cInflLaw_diag {Γ : PairGraph} {t : ℕ} {M : CModel Γ} (_hM : M.Valid) : cpush (cInflLaw M t) readDiag = cTensorPow t M.law

The diagonal law of the complex witness is the tensor power of the model's law.

From a complex model to the real AI feasible set

theorem TriangleInflation.Graph.P5WitnessAux.cpush_ofReal {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq β] (w : α → ℝ) (F : α → β) (b : β) : cpush (fun (a : α) => ↑(w a)) F b = ↑(pushforward w F b)

theorem TriangleInflation.Graph.P5WitnessAux.gAIFeasible_of_cModel {Γ : PairGraph} (M : CModel Γ) (t : ℕ) (P : GTarget Γ) (hM : M.Valid) (hre : ∀ (ω : GAssign Γ t), 0 ≤ (cInflLaw M t ω).re) (hlaw : ∀ (w : Γ.V → Bool), M.law w = ↑(P w)) : GAIFeasible Γ t P

The real part of a complex inflation witness whose model law is real and whose weights have nonnegative real part discharges all five obligations of GAIFeasible.

The five-path complex model

theorem TriangleInflation.Graph.P5WitnessAux.ne01_12 : FivePathAux.E01 ≠ FivePathAux.E12

theorem TriangleInflation.Graph.P5WitnessAux.ne01_23 : FivePathAux.E01 ≠ FivePathAux.E23

theorem TriangleInflation.Graph.P5WitnessAux.ne01_34 : FivePathAux.E01 ≠ FivePathAux.E34

theorem TriangleInflation.Graph.P5WitnessAux.ne12_23 : FivePathAux.E12 ≠ FivePathAux.E23

theorem TriangleInflation.Graph.P5WitnessAux.ne12_34 : FivePathAux.E12 ≠ FivePathAux.E34

theorem TriangleInflation.Graph.P5WitnessAux.ne23_34 : FivePathAux.E23 ≠ FivePathAux.E34

theorem TriangleInflation.Graph.P5WitnessAux.memE01_0 : FivePathAux.E01 ∈ fivePathGraph.inc 0

theorem TriangleInflation.Graph.P5WitnessAux.memE01_1 : FivePathAux.E01 ∈ fivePathGraph.inc 1

theorem TriangleInflation.Graph.P5WitnessAux.memE12_1 : FivePathAux.E12 ∈ fivePathGraph.inc 1

theorem TriangleInflation.Graph.P5WitnessAux.memE12_2 : FivePathAux.E12 ∈ fivePathGraph.inc 2

theorem TriangleInflation.Graph.P5WitnessAux.memE23_2 : FivePathAux.E23 ∈ fivePathGraph.inc 2

theorem TriangleInflation.Graph.P5WitnessAux.memE23_3 : FivePathAux.E23 ∈ fivePathGraph.inc 3

theorem TriangleInflation.Graph.P5WitnessAux.memE34_3 : FivePathAux.E34 ∈ fivePathGraph.inc 3

theorem TriangleInflation.Graph.P5WitnessAux.memE34_4 : FivePathAux.E34 ∈ fivePathGraph.inc 4

noncomputable def TriangleInflation.Graph.P5WitnessAux.pmu (γ : ℝ) (e : fivePathGraph.Edge) (a : Bool × Bool) : ℂ

The complex source weight of the five-path witness: the endpoint sources E01 and E34 are fair, the source E12 carries the formal weight (1 + iγu)/2 on its auxiliary sign and E23 the conjugate weight (1 - iγv)/2. Every latent alphabet is Bool × Bool: a fair mask and an auxiliary sign (the sign is unused on the endpoint sources).

Equations

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

@[simp]

theorem TriangleInflation.Graph.P5WitnessAux.pmu_E01 (γ : ℝ) (a : Bool × Bool) : pmu γ FivePathAux.E01 a = 1 / 4

@[simp]

theorem TriangleInflation.Graph.P5WitnessAux.pmu_E12 (γ : ℝ) (a : Bool × Bool) : pmu γ FivePathAux.E12 a = (1 + Complex.I * ↑γ * ↑(sgn a.2)) / 4

@[simp]

theorem TriangleInflation.Graph.P5WitnessAux.pmu_E23 (γ : ℝ) (a : Bool × Bool) : pmu γ FivePathAux.E23 a = (1 - Complex.I * ↑γ * ↑(sgn a.2)) / 4

@[simp]

theorem TriangleInflation.Graph.P5WitnessAux.pmu_E34 (γ : ℝ) (a : Bool × Bool) : pmu γ FivePathAux.E34 a = 1 / 4

theorem TriangleInflation.Graph.P5WitnessAux.pmu_sum (γ : ℝ) (e : fivePathGraph.Edge) : ∑ a : Bool × Bool, pmu γ e a = 1

def TriangleInflation.Graph.P5WitnessAux.rdE (v : fivePathGraph.V) (c : ↥(fivePathGraph.inc v) → Bool × Bool) (e : fivePathGraph.Edge) : Bool × Bool

Reading the value of a named source out of an incidence-indexed configuration.

Equations

• TriangleInflation.Graph.P5WitnessAux.rdE v c e = if h : e ∈ TriangleInflation.Graph.fivePathGraph.inc v then c ⟨e, h⟩ else (false, false)

noncomputable def TriangleInflation.Graph.P5WitnessAux.pfR (v : Fin 5) (X L R Z : Bool × Bool) : ℝ

The response weight of the vertex v given the values X, L, R, Z of the four sources: A = X, B = r u^X, C = rs when u = v and fair otherwise, D = s v^Z, E = Z. The first component of a latent value is the fair mask, the second the auxiliary sign.

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.pfR_mem (v : Fin 5) (X L R Z : Bool × Bool) : 0 ≤ pfR v X L R Z ∧ pfR v X L R Z ≤ 1

noncomputable def TriangleInflation.Graph.P5WitnessAux.prespR (v : Fin 5) (c : ↥(fivePathGraph.inc v) → Bool × Bool) : ℝ

The real response weight of the five-path witness.

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.prespR_mem (v : Fin 5) (c : ↥(fivePathGraph.inc v) → Bool × Bool) : 0 ≤ prespR v c ∧ prespR v c ≤ 1

noncomputable def TriangleInflation.Graph.P5WitnessAux.PM (γ : ℝ) : CModel fivePathGraph

The five-path complex model at auxiliary amplitude γ.

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.PM_valid (γ : ℝ) : (PM γ).Valid

theorem TriangleInflation.Graph.P5WitnessAux.presp0 (x : fivePathGraph.Edge → Bool × Bool) : (prespR 0 fun (e : ↥(fivePathGraph.inc 0)) => x ↑e) = if (x FivePathAux.E01).1 = true then 0 else 1

theorem TriangleInflation.Graph.P5WitnessAux.presp1 (x : fivePathGraph.Edge → Bool × Bool) : (prespR 1 fun (e : ↥(fivePathGraph.inc 1)) => x ↑e) = if ((x FivePathAux.E12).1 ^^ (x FivePathAux.E01).1 && (x FivePathAux.E12).2) = true then 0 else 1

theorem TriangleInflation.Graph.P5WitnessAux.presp2 (x : fivePathGraph.Edge → Bool × Bool) : (prespR 2 fun (e : ↥(fivePathGraph.inc 2)) => x ↑e) = if (x FivePathAux.E12).2 = (x FivePathAux.E23).2 then if ((x FivePathAux.E12).1 ^^ (x FivePathAux.E23).1) = true then 0 else 1 else 1 / 2

theorem TriangleInflation.Graph.P5WitnessAux.presp3 (x : fivePathGraph.Edge → Bool × Bool) : (prespR 3 fun (e : ↥(fivePathGraph.inc 3)) => x ↑e) = if ((x FivePathAux.E23).1 ^^ (x FivePathAux.E34).1 && (x FivePathAux.E23).2) = true then 0 else 1

theorem TriangleInflation.Graph.P5WitnessAux.presp4 (x : fivePathGraph.Edge → Bool × Bool) : (prespR 4 fun (e : ↥(fivePathGraph.inc 4)) => x ↑e) = if (x FivePathAux.E34).1 = true then 0 else 1

The observed law of the five-path complex model

theorem TriangleInflation.Graph.P5WitnessAux.PM_resp (γ : ℝ) (v : Fin 5) (c : ↥(fivePathGraph.inc v) → Bool × Bool) : (PM γ).resp v c = ↑(prespR v c)

theorem TriangleInflation.Graph.P5WitnessAux.crespMass_bool (b b' : Bool) : crespMass (↑(if b = true then 0 else 1)) b' = if b' = b then 1 else 0

theorem TriangleInflation.Graph.P5WitnessAux.crespMass_ite (p : Prop) [Decidable p] (b b' : Bool) : crespMass (↑(if p then if b = true then 0 else 1 else 1 / 2)) b' = if p then if b' = b then 1 else 0 else 1 / 2

def TriangleInflation.Graph.P5WitnessAux.eTup : (fivePathGraph.Edge → Bool × Bool) ≃ (Bool × Bool) × (Bool × Bool) × (Bool × Bool) × Bool × Bool

The latent tuple of the four sources.

Equations

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

noncomputable def TriangleInflation.Graph.P5WitnessAux.lawSummand (γ : ℝ) (w : Fin 5 → Bool) (X L R Z : Bool × Bool) : ℂ

One term of the observed law of the five-path model, as a function of the four source values X = (x, ·), L = (r, u), R = (s, v), Z = (z, ·).

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.law_summand_eq (γ : ℝ) (w : fivePathGraph.V → Bool) (x : fivePathGraph.Edge → Bool × Bool) : (∏ e : fivePathGraph.Edge, pmu γ e (x e)) * ∏ v : fivePathGraph.V, crespMass ((PM γ).resp v fun (e : ↥(fivePathGraph.inc v)) => x ↑e) (w v) = lawSummand γ w (x FivePathAux.E01) (x FivePathAux.E12) (x FivePathAux.E23) (x FivePathAux.E34)

theorem TriangleInflation.Graph.P5WitnessAux.lawSum (γ : ℝ) (w : Fin 5 → Bool) : ∑ p : (Bool × Bool) × (Bool × Bool) × (Bool × Bool) × Bool × Bool, lawSummand γ w p.1 p.2.1 p.2.2.1 p.2.2.2 = ↑(fivePathTarget (γ ^ 2) w)

theorem TriangleInflation.Graph.P5WitnessAux.PM_law (γ : ℝ) : (PM γ).law = fun (w : Fin 5 → Bool) => ↑(fivePathTarget (γ ^ 2) w)

Positivity of the real part of the complex witness

The copied source weights of PM γ are 1/4 on the endpoint sources and (1 ± iγ)/4 on the two middle ones, so the weight of a copied latent configuration is a positive multiple of a product of 2t complex numbers of modulus A = √(1+γ²) and real part 1. A telescoped triangle inequality plus Cauchy–Schwarz bounds A^n − Re ∏ by n² A^{n-1}(A−1), which is less than A^n for γ = 1/(4t), n = 2t.

theorem TriangleInflation.Graph.P5WitnessAux.tel_bound {ι : Type u_1} (A d : ℝ) (hA : 0 ≤ A) (_hd0 : 0 ≤ d) (f : ι → ℂ) (hn : ∀ (i : ι), ‖f i‖ = A) (hdi : ∀ (i : ι), ‖↑A - f i‖ ≤ d) (s : Finset ι) : ‖↑A ^ s.card - ∏ i ∈ s, f i‖ * A ≤ ↑s.card * A ^ s.card * d

The telescoped bound ‖A^{|s|} − ∏ f‖ · A ≤ |s| A^{|s|} d for factors of modulus A each within d of A.

theorem TriangleInflation.Graph.P5WitnessAux.re_prod_nonneg {ι : Type u_1} [Fintype ι] (A : ℝ) (hA1 : 1 ≤ A) (f : ι → ℂ) (hn : ∀ (i : ι), ‖f i‖ = A) (hdsq : ∀ (i : ι), ‖↑A - f i‖ ^ 2 = 2 * A * (A - 1)) (hkey : ↑(Fintype.card ι) ^ 2 * (A - 1) ≤ A) : 0 ≤ (∏ i : ι, f i).re

If every factor has modulus A ≥ 1 and lies within √(2A(A−1)) of A, and n²(A−1) ≤ A for n the number of factors, then the product has nonnegative real part.

theorem TriangleInflation.Graph.P5WitnessAux.sgn_not (b : Bool) : (sgn !b) = -sgn b

theorem TriangleInflation.Graph.P5WitnessAux.pmu_E12' (γ : ℝ) (hγ : 0 ≤ γ) (a : Bool × Bool) : pmu γ FivePathAux.E12 a = triAtom (γ ^ 2) a.2 / 4

theorem TriangleInflation.Graph.P5WitnessAux.pmu_E23' (γ : ℝ) (hγ : 0 ≤ γ) (a : Bool × Bool) : pmu γ FivePathAux.E23 a = (triAtom (γ ^ 2) !a.2) / 4

noncomputable def TriangleInflation.Graph.P5WitnessAux.zAt (γ : ℝ) {t : ℕ} (x : CCfg (PM γ) t) (k : Bool × Fin t) : ℂ

The auxiliary complex factor of a copied latent configuration: the t copies of the source E12 carry 1 + iγu, the t copies of E23 carry 1 - iγv.

Equations

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

theorem TriangleInflation.Graph.P5WitnessAux.ccfgW_eq (γ : ℝ) (hγ : 0 ≤ γ) (t : ℕ) (x : CCfg (PM γ) t) : ccfgW (PM γ) t x = ↑((1 / 4) ^ (4 * t)) * ∏ k : Bool × Fin t, zAt γ x k

theorem TriangleInflation.Graph.P5WitnessAux.zAt_norm (γ : ℝ) (t : ℕ) (x : CCfg (PM γ) t) (k : Bool × Fin t) : ‖zAt γ x k‖ = √(1 + γ ^ 2)

theorem TriangleInflation.Graph.P5WitnessAux.ccfgW_re_nonneg (γ : ℝ) (hγ : 0 ≤ γ) (t : ℕ) (hγt : (2 * ↑t) ^ 2 * γ ^ 2 ≤ 2) (x : CCfg (PM γ) t) : 0 ≤ (ccfgW (PM γ) t x).re

theorem TriangleInflation.Graph.P5WitnessAux.PM_respV (γ : ℝ) (v : fivePathGraph.V) (c : ↥(fivePathGraph.inc v) → Bool × Bool) : (PM γ).resp v c = ↑(prespR v c)

theorem TriangleInflation.Graph.P5WitnessAux.cInflCond_PM (γ : ℝ) (t : ℕ) (x : CCfg (PM γ) t) (o : GObs fivePathGraph t) (b : Bool) : cInflCond (PM γ) x o b = ↑(respMass (prespR o.fst fun (e : ↥(fivePathGraph.inc o.fst)) => x (↑e, o.snd e)) b)

theorem TriangleInflation.Graph.P5WitnessAux.cprodLaw_PM (γ : ℝ) (t : ℕ) (x : CCfg (PM γ) t) (ω : GAssign fivePathGraph t) : ∃ (c : ℝ), 0 ≤ c ∧ cprodLaw (cInflCond (PM γ) x) ω = ↑c

theorem TriangleInflation.Graph.P5WitnessAux.cInflLaw_re_nonneg (γ : ℝ) (hγ : 0 ≤ γ) (t : ℕ) (hγt : (2 * ↑t) ^ 2 * γ ^ 2 ≤ 2) (ω : GAssign fivePathGraph t) : 0 ≤ (cInflLaw (PM γ) t ω).re

theorem TriangleInflation.Graph.P5WitnessAux.fivePath_witness' (t : ℕ) (ht : 1 ≤ t) (h : ℝ) (hh : h = 1 / (16 * ↑t ^ 2)) : GAIFeasible fivePathGraph t (fivePathTarget h)

AUDIT-NOTES A4, the witness: the five-path target at h = γ², γ = 1/(4t), lies in the order-t ancestral-independence feasible set of P₅.

theorem TriangleInflation.Graph.fivePath_witness (t : ℕ) (ht : 1 ≤ t) (h : ℝ) (hh : h = 1 / (16 * ↑t ^ 2)) : GAIFeasible fivePathGraph t (fivePathTarget h)

AUDIT-NOTES A4, the witness. At order t with γ = 1/(4t) and h = γ² = 1/(16t²), the five-path target lies in the AI feasible set. The witness draws auxiliary signs u_i, v_j with the positive real law H_t(u,v) = 2^{-2t} Re[∏(1+iγu_i) ∏(1−iγv_j)], fair endpoint bits X_a, Z_e, fair masks r_i, s_j and fair private signs ε_{ij}, and sets A^a = X_a, B^{ai} = r_i u_i^{X_a}, D^{je} = s_j v_j^{Z_e}, E^e = Z_e, and C^{ij} = r_i s_j when u_i = v_j, r_i s_j ε_{ij} otherwise.

theorem TriangleInflation.Graph.fivePath_exp_witness (t : ℕ) (ht : 1 ≤ t) (h : ℝ) (hh : h = 1 / (16 * ↑t ^ 2)) : GExpFeasible fivePathGraph t (fivePathTarget h)

The same witness passes the recursively expressible test, by AUDIT-NOTES A2.