Inflation for pair-source graphs: definitions

Definitions for the pair-source generalization of TriangleInflation: a finite simple graph G without isolated vertices, one binary observed variable per vertex, one independent latent source per edge. The triangle of TriangleInflation is the case G = C₃.

The mathematics formalized here is the 2026-09-13 packet as corrected in papers/inflation-nontermination/research-handoffs/2026-09-13/claude-code/review/AUDIT-NOTES.md, items A1–A7 and B; the source is sources/B5-pair-source-classification.md (§1, §3, §5). This file carries definitions only. The statements live in the per-topic modules of this directory (proved) and InflationGraphOpen/ (statements not yet proved).

Representational decisions

• Reuse of the triangle file. IsLaw, pushforward, prodLaw, bern, respMass, ThreeBit, and the triangle hierarchies are imported from TriangleInflation.Defs rather than redefined. Laws stay bare real weight functions with the predicate IsLaw, for the reasons given in that file's header.

• A scenario is a bundled PairGraph. The vertex type, its Fintype and DecidableEq instances, the SimpleGraph, decidable adjacency and the no-isolated-vertex condition are fields of one structure, so that a scenario can be quantified over. Edges are the subtype {e : Sym2 V // e ∈ G.edgeFinset}; incidence PairGraph.inc v is the Finset of edges containing v.

• Copied observations are dependent pairs. GObs Γ t = Σ v : Γ.V, (Γ.inc v → Fin t): a copied observation is a vertex together with one copy index per incident edge. For the triangle this has 3t² elements, matching TriangleInflation.Obs t, but the identification is a theorem (Statements.exists_triObsEquiv) and not a definitional coincidence: GObs carries the incidence structure in its second component, TriangleInflation.Obs in its constructor names.

• Bit convention and signs. Outcomes are Bool; false is the paper's 0. The sign of a bit is sgn false = 1, sgn true = -1, the convention of AUDIT-NOTES ("signs ±1 with false = 0 ↔ +1").

• d-separation is the trail criterion for the depth-one inflation DAG, not a general Pearl definition; see the docstring of dsep. AUDIT-NOTES A2 corrects the packet's stated criterion, and dsep formalizes the corrected one.

• Finite latent alphabets. GCompatible quantifies over a GModel, whose latent spaces are arbitrary Fintypes, while the mathematics allows arbitrary measurable latent spaces. As AUDIT-NOTES D1 phrases it: the formal incompatibility statements are for the finite-latent compatible set; the arbitrary-latent statement needs either the Rosset–Gisin–Wolfe cardinality reduction (quoted, not formalized) or a direct measure-theoretic proof. So the finite-latent compatible set is a subset of the general one, and a Lean theorem ¬ GCompatible Γ P is the weaker statement: it does not by itself say that P has no model with an infinite latent alphabet.

• Division conventions. Real division by zero is zero in Lean. glueLaw nonetheless branches explicitly on 0 < μ_Z(z), because Definition 7 of Wolfe–Spekkens–Fritz prescribes the value 0 on null fibres and the branch records that prescription rather than relying on the junk value. fivePathCorr does rely on it, and every statement about it assumes the conditioning cell is positive.

Pair-source scenarios

structure TriangleInflation.Graph.PairGraph : Type 1

A pair-source scenario (AUDIT-NOTES A1): a finite simple graph without isolated vertices. Each vertex carries one binary observed variable, each edge one independent latent source shared by its two endpoints.

• V : Type

  The observed vertices.

• fintypeV : Fintype self.V
• decEqV : DecidableEq self.V
• G : SimpleGraph self.V

  The source graph; an edge is an independent latent source.

• decAdj : DecidableRel self.G.Adj
• no_isolated (v : self.V) : ∃ (w : self.V), self.G.Adj v w

  No isolated vertices: an observation with no source has no copying convention.

@[reducible, inline]

abbrev TriangleInflation.Graph.PairGraph.Edge (Γ : PairGraph) : Type

The latent sources of a pair-source scenario: the edges of its graph.

Equations

• Γ.Edge = ↥Γ.G.edgeFinset

def TriangleInflation.Graph.PairGraph.inc (Γ : PairGraph) (v : Γ.V) : Finset Γ.Edge

The sources incident to a vertex.

Equations

• Γ.inc v = {e : Γ.Edge | v ∈ ↑e}

@[reducible, inline]

abbrev TriangleInflation.Graph.GTarget (Γ : PairGraph) : Type

A target law: a weight function on the binary observed vertices.

Equations

• TriangleInflation.Graph.GTarget Γ = ((Γ.V → Bool) → ℝ)

Order-t copied observations

@[reducible, inline]

abbrev TriangleInflation.Graph.GObs (Γ : PairGraph) (t : ℕ) : Type

The copied observations of the order-t inflation (AUDIT-NOTES A1): one observation for each vertex v and each choice of a copy index for every source incident to v.

Equations

• TriangleInflation.Graph.GObs Γ t = ((v : Γ.V) × (↥(Γ.inc v) → Fin t))

@[reducible, inline]

abbrev TriangleInflation.Graph.GAssign (Γ : PairGraph) (t : ℕ) : Type

A deterministic assignment of all copied observations.

Equations

• TriangleInflation.Graph.GAssign Γ t = (TriangleInflation.Graph.GObs Γ t → Bool)

@[reducible, inline]

abbrev TriangleInflation.Graph.GLatent (Γ : PairGraph) (t : ℕ) : Type

The copied latent sources: a source together with a copy index.

Equations

• TriangleInflation.Graph.GLatent Γ t = (Γ.Edge × Fin t)

def TriangleInflation.Graph.gPerm {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (o : GObs Γ t) : GObs Γ t

The action of a per-source permutation of copy indices on copied observations.

Equations

• TriangleInflation.Graph.gPerm π o = ⟨o.fst, fun (e : ↥(Γ.inc o.fst)) => (π ↑e) (o.snd e)⟩

def TriangleInflation.Graph.gRelabel {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (ω : GAssign Γ t) : GAssign Γ t

The induced action on assignments.

Equations

• TriangleInflation.Graph.gRelabel π ω o = ω (TriangleInflation.Graph.gPerm π o)

def TriangleInflation.Graph.GSymmetric {Γ : PairGraph} (t : ℕ) (Δ : GAssign Γ t → ℝ) : Prop

Symmetry of a witness under independent permutations of the copy indices of each source (AUDIT-NOTES A1; the pair-source form of TriangleInflation.SymmetricLaw).

Equations

• TriangleInflation.Graph.GSymmetric t Δ = ∀ (π : Γ.Edge → Equiv.Perm (Fin t)) (ω : TriangleInflation.Graph.GAssign Γ t), Δ (TriangleInflation.Graph.gRelabel π ω) = Δ ω

The copied original scenarios

def TriangleInflation.Graph.copyObs {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) (v : Γ.V) : GObs Γ t

The copied observation of the vertex v in the copy of the original scenario selected by the index vector ι.

Equations

• TriangleInflation.Graph.copyObs ι v = ⟨v, fun (e : ↥(Γ.inc v)) => ι ↑e⟩

def TriangleInflation.Graph.copySet {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) : Finset (GObs Γ t)

The copied original scenario selected by ι: one copied observation per vertex.

Equations

• TriangleInflation.Graph.copySet ι = Finset.image (TriangleInflation.Graph.copyObs ι) Finset.univ

def TriangleInflation.Graph.readCopy {Γ : PairGraph} {t : ℕ} (ι : Γ.Edge → Fin t) (ω : GAssign Γ t) : Γ.V → Bool

The observed outcome that an assignment gives to the copied scenario selected by ι.

Equations

• TriangleInflation.Graph.readCopy ι ω v = ω (TriangleInflation.Graph.copyObs ι v)

def TriangleInflation.Graph.readDiag {Γ : PairGraph} {t : ℕ} (ω : GAssign Γ t) : Fin t → Γ.V → Bool

The t diagonal rows: row r takes the copy index r on every source (AUDIT-NOTES A1).

Equations

• TriangleInflation.Graph.readDiag ω r = TriangleInflation.Graph.readCopy (fun (x : Γ.Edge) => r) ω

def TriangleInflation.Graph.gTensorPow {Γ : PairGraph} (t : ℕ) (P : GTarget Γ) : (Fin t → Γ.V → Bool) → ℝ

The t-fold tensor power of a target law.

Equations

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

Ancestry

def TriangleInflation.Graph.gAncestors {Γ : PairGraph} {t : ℕ} (o : GObs Γ t) : Finset (GLatent Γ t)

The copied latent ancestors of a copied observation: for each incident source, the copy selected by that observation.

Equations

• TriangleInflation.Graph.gAncestors o = Finset.image (fun (e : ↥(Γ.inc o.fst)) => (↑e, o.snd e)) Finset.univ

def TriangleInflation.Graph.gAncestorsOf {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : Finset (GLatent Γ t)

The copied latent ancestors of a set of copied observations.

Equations

• TriangleInflation.Graph.gAncestorsOf S = S.biUnion TriangleInflation.Graph.gAncestors

def TriangleInflation.Graph.GAncestrallyIndependent {Γ : PairGraph} {t : ℕ} (S T : Finset (GObs Γ t)) : Prop

Two sets of copied observations are ancestrally independent when their copied latent ancestors are disjoint (TriangleInflation.AncestrallyIndependent for a general pair graph).

Equations

• TriangleInflation.Graph.GAncestrallyIndependent S T = Disjoint (TriangleInflation.Graph.gAncestorsOf S) (TriangleInflation.Graph.gAncestorsOf T)

def TriangleInflation.Graph.edgesOf {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : Finset Γ.Edge

The sources that a set of copied observations touches, ignoring copy indices. Two blocks with disjoint edgesOf are the "source-disjoint blocks" of AUDIT-NOTES A3(i).

Equations

• TriangleInflation.Graph.edgesOf S = S.biUnion fun (o : TriangleInflation.Graph.GObs Γ t) => Γ.inc o.fst

Injectable sets

def TriangleInflation.Graph.GInjectable {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : Prop

The working definition of injectability: a set of copied observations lies inside one copied original scenario.

Equations

• TriangleInflation.Graph.GInjectable S = ∃ (ι : Γ.Edge → Fin t), S ⊆ TriangleInflation.Graph.copySet ι

def TriangleInflation.Graph.GSharedAgree {Γ : PairGraph} {t : ℕ} (o p : GObs Γ t) : Prop

Two copied observations agree in the copy index of every source incident to both.

Equations

• TriangleInflation.Graph.GSharedAgree o p = ∀ (e : Γ.Edge) (ho : e ∈ Γ.inc o.fst) (hp : e ∈ Γ.inc p.fst), o.snd ⟨e, ho⟩ = p.snd ⟨e, hp⟩

def TriangleInflation.Graph.GInjectableRaw {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : Prop

The primitive Wolfe–Spekkens–Fritz condition (Definition 4) for a pair-source scenario: erasing copy indices is injective on the set, and any two members agree in the copy index of every shared source. Statements.gInjectable_iff_raw records the equivalence with GInjectable, as TriangleInflation.injectable_iff_injectableRaw does for the triangle.

Equations

• TriangleInflation.Graph.GInjectableRaw S = ((∀ o ∈ S, ∀ p ∈ S, o.fst = p.fst → o = p) ∧ ∀ o ∈ S, ∀ p ∈ S, TriangleInflation.Graph.GSharedAgree o p)

def TriangleInflation.Graph.gRestrict {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) (ω : GAssign Γ t) : ↥S → Bool

The restriction of an assignment to a set of copied observations.

Equations

• TriangleInflation.Graph.gRestrict S ω o = ω ↑o

def TriangleInflation.Graph.gPartyRead {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) (w : Γ.V → Bool) : ↥S → Bool

The outcome pattern that a target law prescribes on a set of copied observations: each member reads the bit of the vertex it is a copy of.

Equations

• TriangleInflation.Graph.gPartyRead S w o = w (↑o).fst

def TriangleInflation.Graph.subRestrict {Γ : PairGraph} {t : ℕ} {S T : Finset (GObs Γ t)} (h : S ⊆ T) (φ : ↥T → Bool) : ↥S → Bool

The restriction map between laws on nested sets of copied observations.

Equations

• TriangleInflation.Graph.subRestrict h φ o = φ ⟨↑o, ⋯⟩

def TriangleInflation.Graph.readOnBlock {Γ : PairGraph} {t : ℕ} (B S : Finset (GObs Γ t)) (φ : ↥S → Bool) : ↥B → Bool

Reading a block inside an ambient set. When B ⊆ S this is subRestrict; the else branch is unreachable and is present only so that the block may be given as a bare Finset, without carrying the inclusion proof.

Equations

• TriangleInflation.Graph.readOnBlock B S φ o = if h : ↑o ∈ S then φ ⟨↑o, h⟩ else false

The finite inflation tests

def TriangleInflation.Graph.GInjectableMarginals {Γ : PairGraph} (t : ℕ) (Δ : GAssign Γ t → ℝ) (P : GTarget Γ) : Prop

Every injectable set carries the corresponding marginal of the target.

Equations

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

def TriangleInflation.Graph.GAncestralProducts {Γ : PairGraph} (t : ℕ) (Δ : GAssign Γ t → ℝ) (P : GTarget Γ) : Prop

Every finite family of pairwise ancestrally independent injectable sets carries the product of the corresponding marginals.

Equations

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

def TriangleInflation.Graph.GNWFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) : Prop

The Navascués–Wolfe feasible set of a pair-source scenario (AUDIT-NOTES A1): a symmetric law on the copied observations whose diagonal law is the tensor power of the target.

Equations

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

def TriangleInflation.Graph.GAIFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) : Prop

The ancestral-independence feasible set of a pair-source scenario (AUDIT-NOTES A1).

Equations

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

Recursive expressibility

The inflation DAG of a pair-source scenario has depth one: the copied latent sources are roots, the copied observations are sinks, and the parents of a copied observation are exactly its gAncestors.

def TriangleInflation.Graph.SharesParent {Γ : PairGraph} {t : ℕ} (o p : GObs Γ t) : Prop

Two copied observations share a copied latent parent.

Equations

• TriangleInflation.Graph.SharesParent o p = ¬Disjoint (TriangleInflation.Graph.gAncestors o) (TriangleInflation.Graph.gAncestors p)

def TriangleInflation.Graph.ActiveTrail {Γ : PairGraph} {t : ℕ} (X Y Z : Finset (GObs Γ t)) (o₀ : GObs Γ t) (mid : List (GObs Γ t)) (o₁ : GObs Γ t) : Prop

A trail from X to Y that is active given Z: a sequence of copied observations o₀ ∈ X, mid, o₁ ∈ Y (so of length at least two) in which consecutive members share a copied latent parent and every internal member lies in Z.

Equations

• TriangleInflation.Graph.ActiveTrail X Y Z o₀ mid o₁ = (o₀ ∈ X ∧ o₁ ∈ Y ∧ (∀ o ∈ mid, o ∈ Z) ∧ List.IsChain TriangleInflation.Graph.SharesParent (o₀ :: (mid ++ [o₁])))

def TriangleInflation.Graph.dsep {Γ : PairGraph} {t : ℕ} (X Y Z : Finset (GObs Γ t)) : Prop

d-separation in the order-t inflation DAG, by the trail criterion.

This is the specialization of Pearl d-separation to a DAG in which every latent node is a root and every observed node is a sink. In such a DAG a trail between two observed nodes alternates observed node, shared latent parent, observed node; every latent on it is a fork and every internal observed node is a collider; and no node has descendants, so a collider is unblocked exactly when it is itself conditioned on. Hence a trail is active given Z exactly when all of its internal observed nodes lie in Z, and X ⊥_d Y | Z exactly when no such trail exists.

AUDIT-NOTES A2 corrects the packet's stated criterion ("no component of the shared-parent graph on X ∪ Y ∪ Z meets both X and Y", which is only sufficient); this definition is the corrected trail criterion, and the component statement becomes a theorem for AI sets (Statements.expressible_iff_ai).

Equations

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

theorem TriangleInflation.Graph.sub_left_union {Γ : PairGraph} {t : ℕ} (X Y Z : Finset (GObs Γ t)) : X ∪ Z ⊆ X ∪ Y ∪ Z

theorem TriangleInflation.Graph.sub_right_union {Γ : PairGraph} {t : ℕ} (X Y Z : Finset (GObs Γ t)) : Y ∪ Z ⊆ X ∪ Y ∪ Z

theorem TriangleInflation.Graph.sub_mid_union {Γ : PairGraph} {t : ℕ} (X Y Z : Finset (GObs Γ t)) : Z ⊆ X ∪ Y ∪ Z

theorem TriangleInflation.Graph.sub_mid_left {Γ : PairGraph} {t : ℕ} (X Z : Finset (GObs Γ t)) : Z ⊆ X ∪ Z

noncomputable def TriangleInflation.Graph.glueLaw {Γ : PairGraph} {t : ℕ} (X Y Z : Finset (GObs Γ t)) (μ₁ : (↥(X ∪ Z) → Bool) → ℝ) (μ₂ : (↥(Y ∪ Z) → Bool) → ℝ) : (↥(X ∪ Y ∪ Z) → Bool) → ℝ

The glued law of Wolfe–Spekkens–Fritz Definition 7: μ(x,y,z) = μ₁(x,z) μ₂(y,z) / μ_Z(z) when the common Z-marginal μ_Z(z) is positive, and 0 otherwise. μ_Z is taken as the Z-marginal of μ₁; on the sets where the rule is applied the two marginals agree.

Equations

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

inductive TriangleInflation.Graph.Expressible {Γ : PairGraph} (t : ℕ) (P : GTarget Γ) (S : Finset (GObs Γ t)) : ((↥S → Bool) → ℝ) → Prop

The recursively expressible sets of the order-t inflation, each with its prescribed law (paper Definition 2.5, Wolfe–Spekkens–Fritz Definition 7). Expressible t P S μ says that the closure prescribes the law μ on the set S of copied observations.

The three rules are: an injectable set carries the pushforward of the target under the party-read map; two prescribed sets X ∪ Z and Y ∪ Z with X, Y, Z pairwise disjoint and dsep X Y Z glue to X ∪ Y ∪ Z; and marginals of prescribed sets are prescribed.

This is the definition that TriangleInflation.Defs deliberately omits.

• inj {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {S : Finset (GObs Γ t)} (h : GInjectable S) : Expressible t P S (pushforward P (gPartyRead S))
• glue {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {X Y Z : Finset (GObs Γ t)} {μ₁ : (↥(X ∪ Z) → Bool) → ℝ} {μ₂ : (↥(Y ∪ Z) → Bool) → ℝ} (h₁ : Expressible t P (X ∪ Z) μ₁) (h₂ : Expressible t P (Y ∪ Z) μ₂) (hXY : Disjoint X Y) (hXZ : Disjoint X Z) (hYZ : Disjoint Y Z) (hd : dsep X Y Z) : Expressible t P (X ∪ Y ∪ Z) (glueLaw X Y Z μ₁ μ₂)
• marg {Γ : PairGraph} {t : ℕ} {P : GTarget Γ} {S T : Finset (GObs Γ t)} {μ : (↥T → Bool) → ℝ} (hST : S ⊆ T) (h : Expressible t P T μ) : Expressible t P S (pushforward μ (subRestrict hST))

def TriangleInflation.Graph.GExpFeasible (Γ : PairGraph) (t : ℕ) (P : GTarget Γ) : Prop

The recursively expressible feasible set of a pair-source scenario (paper Definition 2.3).

Equations

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

AI sets

The sets and laws that the ancestral-independence prescriptions cover. AUDIT-NOTES A2 identifies these with the recursively expressible ones.

def TriangleInflation.Graph.sharedComponent {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : ↥S → ↥S → Prop

Connectivity in the shared-parent graph on a set of copied observations.

Equations

• TriangleInflation.Graph.sharedComponent S = Relation.ReflTransGen fun (a b : ↥S) => TriangleInflation.Graph.SharesParent ↑a ↑b

def TriangleInflation.Graph.IsAISet {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : Prop

An AI set: every connected component of the shared-parent graph on S is injectable (AUDIT-NOTES A2). The component of o is described by its membership predicate rather than constructed, so that no decidability of sharedComponent is needed.

Equations

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

structure TriangleInflation.Graph.AIDecomposition {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) : Type

A presentation of a set of copied observations as a union of pairwise ancestrally independent injectable blocks.

• n : ℕ

  The number of blocks.

• block : Fin self.n → Finset (GObs Γ t)

  The blocks.

• inj (m : Fin self.n) : GInjectable (self.block m)
• ai (m m' : Fin self.n) : m ≠ m' → GAncestrallyIndependent (self.block m) (self.block m')
• cover : S = Finset.univ.biUnion self.block

def TriangleInflation.Graph.aiProduct {Γ : PairGraph} {t : ℕ} (S : Finset (GObs Γ t)) (D : AIDecomposition S) (P : GTarget Γ) : (↥S → Bool) → ℝ

The AI product law of a decomposition: the product of the injectable marginals of the blocks.

Equations

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

Compatibility

structure TriangleInflation.Graph.GModel (Γ : PairGraph) : Type 1

A model of a pair-source scenario with finite latent alphabets: one latent alphabet and source law per edge, and for each vertex the probability resp v of the outcome false = 0 given the values of the sources incident to it.

• L : Γ.Edge → Type

  The latent alphabet of each source.

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

  The law of each source.

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

  resp v c = Pr(outcome at v is 0 | incident sources take the values c).

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

A model is valid when every source law is a law and every response probability lies in [0,1].

Equations

• M.Valid = ((∀ (e : Γ.Edge), TriangleInflation.IsLaw (M.μ e)) ∧ ∀ (v : Γ.V) (c : (e : ↥(Γ.inc v)) → M.L ↑e), 0 ≤ M.resp v c ∧ M.resp v c ≤ 1)

def TriangleInflation.Graph.GModel.law {Γ : PairGraph} (M : GModel Γ) : GTarget Γ

The observed law of a model: the sources are independent and the responses are conditionally independent given the sources.

Equations

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

def TriangleInflation.Graph.GCompatible (Γ : PairGraph) (P : GTarget Γ) : Prop

The compatible set C_G of a pair-source scenario, with the finite-latent-alphabet boundary described in the file header (AUDIT-NOTES D1).

Equations

• TriangleInflation.Graph.GCompatible Γ P = ∃ (M : TriangleInflation.Graph.GModel Γ), M.Valid ∧ M.law = P

Named scenarios

def TriangleInflation.Graph.pathAdj (k : ℕ) : SimpleGraph (Fin k)

The path P_k on Fin k.

Equations

• TriangleInflation.Graph.pathAdj k = { Adj := fun (a b : Fin k) => ↑a + 1 = ↑b ∨ ↑b + 1 = ↑a, symm := ⋯, loopless := ⋯ }

@[instance_reducible]

instance TriangleInflation.Graph.instDecidableAdjFinPathAdj (k : ℕ) (a b : Fin k) : Decidable ((pathAdj k).Adj a b)

Equations

• TriangleInflation.Graph.instDecidableAdjFinPathAdj k a b = { decide := decide (↑a + 1 = ↑b) || decide (↑b + 1 = ↑a), reflects_decide := ⋯ }

theorem TriangleInflation.Graph.path_no_isolated {k : ℕ} (hk : 2 ≤ k) (v : Fin k) : ∃ (w : Fin k), (pathAdj k).Adj v w

def TriangleInflation.Graph.cycleAdj (m : ℕ) : SimpleGraph (Fin m)

The cycle C_m on Fin m. For m ≥ 3 the adjacency a ≠ b ∧ (a+1 ≡ b ∨ b+1 ≡ a) is the m-cycle; the explicit a ≠ b makes the relation irreflexive for every m.

Equations

• TriangleInflation.Graph.cycleAdj m = { Adj := fun (a b : Fin m) => a ≠ b ∧ ((↑a + 1) % m = ↑b ∨ (↑b + 1) % m = ↑a), symm := ⋯, loopless := ⋯ }

@[instance_reducible]

instance TriangleInflation.Graph.instDecidableAdjFinCycleAdj (m : ℕ) (a b : Fin m) : Decidable ((cycleAdj m).Adj a b)

Equations

• TriangleInflation.Graph.instDecidableAdjFinCycleAdj m a b = { decide := decide (a ≠ b) && decide ((↑a + 1) % m = ↑b ∨ (↑b + 1) % m = ↑a), reflects_decide := ⋯ }

theorem TriangleInflation.Graph.cycle_no_isolated {m : ℕ} (hm : 3 ≤ m) (v : Fin m) : ∃ (w : Fin m), (cycleAdj m).Adj v w

inductive TriangleInflation.Graph.DoubleStarV (p q : ℕ) : Type

The vertices of a double star: two centres and their leaves.

• left {p q : ℕ} : DoubleStarV p q
• right {p q : ℕ} : DoubleStarV p q
• leftLeaf {p q : ℕ} (i : Fin p) : DoubleStarV p q
• rightLeaf {p q : ℕ} (j : Fin q) : DoubleStarV p q

def TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq {p✝ q✝ : ℕ} (x✝ x✝¹ : DoubleStarV p✝ q✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.left TriangleInflation.Graph.DoubleStarV.left = isTrue ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.left TriangleInflation.Graph.DoubleStarV.right = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.left (TriangleInflation.Graph.DoubleStarV.leftLeaf i) = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.left (TriangleInflation.Graph.DoubleStarV.rightLeaf j) = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.right TriangleInflation.Graph.DoubleStarV.left = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.right TriangleInflation.Graph.DoubleStarV.right = isTrue ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.right (TriangleInflation.Graph.DoubleStarV.leftLeaf i) = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq TriangleInflation.Graph.DoubleStarV.right (TriangleInflation.Graph.DoubleStarV.rightLeaf j) = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq (TriangleInflation.Graph.DoubleStarV.leftLeaf i) TriangleInflation.Graph.DoubleStarV.left = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq (TriangleInflation.Graph.DoubleStarV.leftLeaf i) TriangleInflation.Graph.DoubleStarV.right = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq (TriangleInflation.Graph.DoubleStarV.leftLeaf i) (TriangleInflation.Graph.DoubleStarV.rightLeaf j) = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq (TriangleInflation.Graph.DoubleStarV.rightLeaf j) TriangleInflation.Graph.DoubleStarV.left = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq (TriangleInflation.Graph.DoubleStarV.rightLeaf j) TriangleInflation.Graph.DoubleStarV.right = isFalse ⋯
• TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq (TriangleInflation.Graph.DoubleStarV.rightLeaf j) (TriangleInflation.Graph.DoubleStarV.leftLeaf i) = isFalse ⋯

@[instance_reducible]

instance TriangleInflation.Graph.instDecidableEqDoubleStarV {p✝ q✝ : ℕ} : DecidableEq (DoubleStarV p✝ q✝)

Equations

• TriangleInflation.Graph.instDecidableEqDoubleStarV = TriangleInflation.Graph.instDecidableEqDoubleStarV.decEq

@[instance_reducible]

instance TriangleInflation.Graph.instFintypeDoubleStarV {p✝ q✝ : ℕ} : Fintype (DoubleStarV p✝ q✝)

Equations

• TriangleInflation.Graph.instFintypeDoubleStarV = Fintype.ofEquiv (Unit ⊕ Unit ⊕ Fin p✝ ⊕ Fin q✝) (TriangleInflation.Graph.DoubleStarV.proxyTypeEquiv p✝ q✝)

def TriangleInflation.Graph.doubleStarRel (p q : ℕ) : DoubleStarV p q → DoubleStarV p q → Prop

Adjacency of the double star: the centre edge, and each leaf to its centre.

Equations

• TriangleInflation.Graph.doubleStarRel p q TriangleInflation.Graph.DoubleStarV.left TriangleInflation.Graph.DoubleStarV.right = True
• TriangleInflation.Graph.doubleStarRel p q TriangleInflation.Graph.DoubleStarV.right TriangleInflation.Graph.DoubleStarV.left = True
• TriangleInflation.Graph.doubleStarRel p q TriangleInflation.Graph.DoubleStarV.left (TriangleInflation.Graph.DoubleStarV.leftLeaf i) = True
• TriangleInflation.Graph.doubleStarRel p q (TriangleInflation.Graph.DoubleStarV.leftLeaf i) TriangleInflation.Graph.DoubleStarV.left = True
• TriangleInflation.Graph.doubleStarRel p q TriangleInflation.Graph.DoubleStarV.right (TriangleInflation.Graph.DoubleStarV.rightLeaf j) = True
• TriangleInflation.Graph.doubleStarRel p q (TriangleInflation.Graph.DoubleStarV.rightLeaf j) TriangleInflation.Graph.DoubleStarV.right = True
• TriangleInflation.Graph.doubleStarRel p q x✝¹ x✝ = False

@[instance_reducible]

instance TriangleInflation.Graph.instDecidableDoubleStarRel (p q : ℕ) (a b : DoubleStarV p q) : Decidable (doubleStarRel p q a b)

Equations

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

def TriangleInflation.Graph.doubleStarAdj (p q : ℕ) : SimpleGraph (DoubleStarV p q)

The double star with p left leaves and q right leaves.

Equations

• TriangleInflation.Graph.doubleStarAdj p q = { Adj := TriangleInflation.Graph.doubleStarRel p q, symm := ⋯, loopless := ⋯ }

@[instance_reducible]

instance TriangleInflation.Graph.instDecidableAdjDoubleStarVDoubleStarAdj (p q : ℕ) (a b : DoubleStarV p q) : Decidable ((doubleStarAdj p q).Adj a b)

Equations

• TriangleInflation.Graph.instDecidableAdjDoubleStarVDoubleStarAdj p q a b = TriangleInflation.Graph.instDecidableAdjDoubleStarVDoubleStarAdj._aux_1 p q a b

theorem TriangleInflation.Graph.doubleStar_no_isolated (p q : ℕ) (v : DoubleStarV p q) : ∃ (w : DoubleStarV p q), (doubleStarAdj p q).Adj v w

def TriangleInflation.Graph.path (k : ℕ) (hk : 2 ≤ k) : PairGraph

The path scenario P_k, k ≥ 2.

Equations

• TriangleInflation.Graph.path k hk = { V := Fin k, fintypeV := inferInstance, decEqV := inferInstance, G := TriangleInflation.Graph.pathAdj k, decAdj := inferInstance, no_isolated := ⋯ }

def TriangleInflation.Graph.cycle (m : ℕ) (hm : 3 ≤ m) : PairGraph

The cycle scenario C_m, m ≥ 3.

Equations

• TriangleInflation.Graph.cycle m hm = { V := Fin m, fintypeV := inferInstance, decEqV := inferInstance, G := TriangleInflation.Graph.cycleAdj m, decAdj := inferInstance, no_isolated := ⋯ }

def TriangleInflation.Graph.doubleStar (p q : ℕ) : PairGraph

The double-star scenario with p and q leaves.

Equations

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

def TriangleInflation.Graph.triangleGraph : PairGraph

The triangle scenario, C₃.

Equations

• TriangleInflation.Graph.triangleGraph = TriangleInflation.Graph.cycle 3 TriangleInflation.Graph.triangleGraph._proof_1

def TriangleInflation.Graph.squareGraph : PairGraph

The square scenario, C₄.

Equations

• TriangleInflation.Graph.squareGraph = TriangleInflation.Graph.cycle 4 TriangleInflation.Graph.squareGraph._proof_1

def TriangleInflation.Graph.fivePathGraph : PairGraph

The five-observer path P₅ (AUDIT-NOTES A4).

Equations

• TriangleInflation.Graph.fivePathGraph = TriangleInflation.Graph.path 5 TriangleInflation.Graph.fivePathGraph._proof_1

def TriangleInflation.Graph.IsDoubleStarForest {V : Type} (G : SimpleGraph V) : Prop

A double-star forest: every connected component is a tree of diameter at most three (AUDIT-NOTES A3). Stated as acyclicity together with a diameter bound inside each component.

Equations

• TriangleInflation.Graph.IsDoubleStarForest G = (G.IsAcyclic ∧ ∀ (u v : V), G.Reachable u v → G.dist u v ≤ 3)

Signs, flips and explicit laws

def TriangleInflation.Graph.sgn (b : Bool) : ℝ

The sign of a bit: sgn false = 1, sgn true = -1 (AUDIT-NOTES convention).

Equations

• TriangleInflation.Graph.sgn b = if b = true then -1 else 1

def TriangleInflation.Graph.flipKernel {ι : Type} [Fintype ι] (η : ℝ) (x y : ι → Bool) : ℝ

The kernel of independent flips with probability η at every coordinate.

Equations

• TriangleInflation.Graph.flipKernel η x y = ∏ i : ι, if x i = y i then 1 - η else η

def TriangleInflation.Graph.flipLaw {ι : Type} [Fintype ι] [DecidableEq ι] (η : ℝ) (P : (ι → Bool) → ℝ) : (ι → Bool) → ℝ

A law after independent flips of each coordinate with probability η. Applied to a target on Γ.V → Bool it is the noisy target of AUDIT-NOTES A7; applied to a witness on GObs Γ t → Bool it is the local flip of every copied observation.

Equations

• TriangleInflation.Graph.flipLaw η P y = ∑ x : ι → Bool, P x * TriangleInflation.Graph.flipKernel η x y

noncomputable def TriangleInflation.Graph.dTV {α : Type u_1} [Fintype α] (P Q : α → ℝ) : ℝ

The total variation distance, half the ℓ¹ distance.

Equations

• TriangleInflation.Graph.dTV P Q = 1 / 2 * ∑ a : α, |P a - Q a|

noncomputable def TriangleInflation.Graph.distToCompatible (Γ : PairGraph) (P : GTarget Γ) : ℝ

The total variation distance from a target to the compatible set.

Equations

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

noncomputable def TriangleInflation.Graph.fivePathTarget (h : ℝ) : (Fin 5 → Bool) → ℝ

The five-path target of AUDIT-NOTES A4 (packet equation (1)): P_h(x,b,c,d,z) = (1/32)[1 + bcd (1+h)/4 (1 + (−1)^{x+z})], with vertex 0 the left endpoint A, vertices 1,2,3 the middle observations B,C,D and vertex 4 the right endpoint E.

Equations

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

noncomputable def TriangleInflation.Graph.fivePathCorr (P : (Fin 5 → Bool) → ℝ) (x z : Bool) : ℝ

The conditional correlator f_{xz} = E[BCD | A = x, E = z] of AUDIT-NOTES A4. The denominator is the conditioning cell; the value is junk 0 when that cell is null, and every statement about it assumes the cell is positive.

Equations

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

noncomputable def TriangleInflation.Graph.fivePathI (P : (Fin 5 → Bool) → ℝ) : ℝ

I = ¼ Σ_{x,z} f_{xz} (AUDIT-NOTES A4).

Equations

• TriangleInflation.Graph.fivePathI P = 1 / 4 * ∑ x : Bool, ∑ z : Bool, TriangleInflation.Graph.fivePathCorr P x z

noncomputable def TriangleInflation.Graph.fivePathJ (P : (Fin 5 → Bool) → ℝ) : ℝ

J = ¼ Σ_{x,z} (−1)^{x+z} f_{xz} (AUDIT-NOTES A4).

Equations

• TriangleInflation.Graph.fivePathJ P = 1 / 4 * ∑ x : Bool, ∑ z : Bool, TriangleInflation.Graph.sgn x * TriangleInflation.Graph.sgn z * TriangleInflation.Graph.fivePathCorr P x z

def TriangleInflation.Graph.cycleBoundary (m : ℕ) (F : Finset (Fin m)) : Finset (Fin m)

The source boundary ∂F of a set of vertices of the cycle C_m, encoded by its lower endpoint: the edge {v, v+1} is recorded by v, and lies in ∂F exactly when exactly one of v, v+1 lies in F (AUDIT-NOTES A5).

Equations

• TriangleInflation.Graph.cycleBoundary m F = {v : Fin m | (v ∈ F) ≠ (⟨(↑v + 1) % m, ⋯⟩ ∈ F)}

noncomputable def TriangleInflation.Graph.cycleTarget (m : ℕ) (q : ℝ) : (Fin m → Bool) → ℝ

The cycle target P_{m,q} of AUDIT-NOTES A5, given by its Fourier expansion: the character of F ⊆ V has moment (−q)^{|∂F|/2}. The boundary has even size, so the natural division is exact.

Equations

• TriangleInflation.Graph.cycleTarget m q w = (1 / 2) ^ m * ∑ F : Finset (Fin m), (-q) ^ ((TriangleInflation.Graph.cycleBoundary m F).card / 2) * ∏ v ∈ F, TriangleInflation.Graph.sgn (w v)

noncomputable def TriangleInflation.Graph.squareTarget (q : ℝ) : (Fin 4 → Bool) → ℝ

The square parity target of AUDIT-NOTES B2(i): the case m = 4 of cycleTarget.

Equations

• TriangleInflation.Graph.squareTarget q = TriangleInflation.Graph.cycleTarget 4 q

noncomputable def TriangleInflation.Graph.triParity (q : ℝ) : ThreeBit → ℝ

The parity-perfect triangle target Π(−q,−q,−q) of AUDIT-NOTES B2(ii): supported on the even-parity triples, where it equals (1 − q(α+β+γ))/4 with α,β,γ the signs of the three bits. All one- and two-point moments are −q and the triple moment is 1. Stated in the three-bit type of TriangleInflation.

Equations

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

def TriangleInflation.Graph.triMeanA (P : ThreeBit → ℝ) : ℝ

E[A] for a three-bit law, in the sign convention.

Equations

• TriangleInflation.Graph.triMeanA P = ∑ w : TriangleInflation.ThreeBit, TriangleInflation.Graph.sgn w.1 * P w

def TriangleInflation.Graph.triMeanB (P : ThreeBit → ℝ) : ℝ

E[B] for a three-bit law.

Equations

• TriangleInflation.Graph.triMeanB P = ∑ w : TriangleInflation.ThreeBit, TriangleInflation.Graph.sgn w.2.1 * P w

def TriangleInflation.Graph.triMeanC (P : ThreeBit → ℝ) : ℝ

E[C] for a three-bit law.

Equations

• TriangleInflation.Graph.triMeanC P = ∑ w : TriangleInflation.ThreeBit, TriangleInflation.Graph.sgn w.2.2 * P w

noncomputable def TriangleInflation.Graph.transportTarget (G H : PairGraph) (φ : H.V → G.V) (P : GTarget H) : GTarget G

The transported target of AUDIT-NOTES A6: the H-target on the image of an induced embedding, tensored with fair bits on the remaining vertices of G.

Equations

• TriangleInflation.Graph.transportTarget G H φ P w = (P fun (u : H.V) => w (φ u)) * (1 / 2) ^ (Fintype.card G.V - Fintype.card H.V)

The triangle re-encoding

The triangle scenario triangleGraph has vertex type Fin 3; the triangle file uses ThreeBit = Bool × Bool × Bool. Under the identification below, vertex 0 is the party A (sources {0,1} and {2,0}, the paper's X and Z), vertex 1 is B (sources {0,1} and {1,2}, the paper's X and Y) and vertex 2 is C (sources {1,2} and {2,0}, the paper's Y and Z).

def TriangleInflation.Graph.threeBitEquiv : (Fin 3 → Bool) ≃ ThreeBit

The re-encoding of a three-bit outcome as a function on Fin 3.

Equations

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