The order-t cycle witness (A5)

The auxiliary-sign construction of AUDIT-NOTES A5 and Lemma lem:cyclewitness of papers/inflation-nontermination/paper/sections/15-cycles.tex.

Fourier synthesis on a finite Boolean cube

noncomputable def TriangleInflation.Graph.CycleWitnessAux.fourier {ι : Type u_1} [Fintype ι] (c : Finset ι → ℝ) : (ι → Bool) → ℝ

The weight function on ι → Bool with prescribed Walsh coefficients.

Equations

• TriangleInflation.Graph.CycleWitnessAux.fourier c s = (1 / 2) ^ Fintype.card ι * ∑ F : Finset ι, c F * ∏ v ∈ F, TriangleInflation.Graph.sgn (s v)

theorem TriangleInflation.Graph.CycleWitnessAux.fourier_moment {ι : Type u_1} [Fintype ι] [DecidableEq ι] (c : Finset ι → ℝ) (F : Finset ι) : ∑ s : ι → Bool, fourier c s * ∏ v ∈ F, sgn (s v) = c F

The Walsh moments of fourier c are the coefficients c.

theorem TriangleInflation.Graph.CycleWitnessAux.sum_pow_card {ι : Type u_1} [Fintype ι] (ρ : ℝ) : ∑ F : Finset ι, ρ ^ F.card = (1 + ρ) ^ Fintype.card ι

The generating identity ∑_F ρ^{|F|} = (1+ρ)^n.

theorem TriangleInflation.Graph.CycleWitnessAux.one_add_pow_le_two {ρ : ℝ} {N : ℕ} (hρ0 : 0 ≤ ρ) (h : ↑N * ρ ≤ 1 / 2) : (1 + ρ) ^ N ≤ 2

(1+ρ)^N ≤ 2 when Nρ ≤ 1/2: Bernoulli on (1-ρ)^N together with (1-ρ²)^N ≤ 1.

theorem TriangleInflation.Graph.CycleWitnessAux.fourier_nonneg {ι : Type u_1} [Fintype ι] (c : Finset ι → ℝ) (ρ : ℝ) (_hρ0 : 0 ≤ ρ) (h0 : c ∅ = 1) (hc : ∀ (F : Finset ι), F ≠ ∅ → |c F| ≤ ρ ^ F.card) (hexp : (1 + ρ) ^ Fintype.card ι ≤ 2) (s : ι → Bool) : 0 ≤ fourier c s

Positivity of a Fourier synthesis whose nonconstant coefficients are dominated by a geometric series summing to at most the constant coefficient.

The auxiliary sign density

noncomputable def TriangleInflation.Graph.CycleWitnessAux.auxH (ι : Type u_2) [Fintype ι] (q : ℝ) : (ι → Bool) → ℝ

The auxiliary density H_{N,q}(s) = 2^{−N} ∑_{|S| even} (−q)^{|S|/2} ∏_S s.

Equations

• TriangleInflation.Graph.CycleWitnessAux.auxH ι q = TriangleInflation.Graph.CycleWitnessAux.fourier fun (S : Finset ι) => if Even S.card then (-q) ^ (S.card / 2) else 0

theorem TriangleInflation.Graph.CycleWitnessAux.auxH_moment {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℝ) (S : Finset ι) : ∑ s : ι → Bool, auxH ι q s * ∏ l ∈ S, sgn (s l) = if Even S.card then (-q) ^ (S.card / 2) else 0

The Walsh moments of the auxiliary density.

theorem TriangleInflation.Graph.CycleWitnessAux.auxH_sum {ι : Type u_1} [Fintype ι] [DecidableEq ι] (q : ℝ) : ∑ s : ι → Bool, auxH ι q s = 1

The auxiliary density has total mass one.

theorem TriangleInflation.Graph.CycleWitnessAux.auxH_nonneg {ι : Type u_1} [Fintype ι] (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑(Fintype.card ι) ^ 2 * q ≤ 1 / 4) (s : ι → Bool) : 0 ≤ auxH ι q s

The auxiliary density is nonnegative when N²q ≤ 1/4.

The parity witness of a general pair-source scenario

theorem TriangleInflation.Graph.CycleWitnessAux.prod_sgn_eq_neg_one_pow {L : Type u_1} (A : Finset L) (s : L → Bool) : ∏ l ∈ A, sgn (s l) = (-1) ^ {l ∈ A | s l = true}.card

A Walsh character as a power of -1.

def TriangleInflation.Graph.CycleWitnessAux.parityRead {Γ : PairGraph} {t : ℕ} (s : GLatent Γ t → Bool) : GAssign Γ t

The parity read: a copied observation answers with the parity of the signs of its copied latent ancestors (O_v^{ij} = s_{v−1,i} s_{v,j} for the cycle).

Equations

• TriangleInflation.Graph.CycleWitnessAux.parityRead s o = decide ({l ∈ TriangleInflation.Graph.gAncestors o | s l = true}.card % 2 = 1)

theorem TriangleInflation.Graph.CycleWitnessAux.sgn_parityRead {Γ : PairGraph} {t : ℕ} (s : GLatent Γ t → Bool) (o : GObs Γ t) : sgn (parityRead s o) = ∏ l ∈ gAncestors o, sgn (s l)

def TriangleInflation.Graph.CycleWitnessAux.latBd {Γ : PairGraph} {t : ℕ} (A : Finset (GObs Γ t)) : Finset (GLatent Γ t)

The latent boundary of a set of copied observations: the copied sources that an odd number of members of the set touch.

Equations

• TriangleInflation.Graph.CycleWitnessAux.latBd A = {l : TriangleInflation.Graph.GLatent Γ t | {o ∈ A | l ∈ TriangleInflation.Graph.gAncestors o}.card % 2 = 1}

theorem TriangleInflation.Graph.CycleWitnessAux.mem_latBd {Γ : PairGraph} {t : ℕ} {A : Finset (GObs Γ t)} {l : GLatent Γ t} : l ∈ latBd A ↔ {o ∈ A | l ∈ gAncestors o}.card % 2 = 1

theorem TriangleInflation.Graph.CycleWitnessAux.prod_sgn_parityRead {Γ : PairGraph} {t : ℕ} (A : Finset (GObs Γ t)) (s : GLatent Γ t → Bool) : ∏ o ∈ A, sgn (parityRead s o) = ∏ l ∈ latBd A, sgn (s l)

A character of a set of copied observations, read through the parity witness, is the character of its latent boundary.

theorem TriangleInflation.Graph.CycleWitnessAux.auxH_perm {ι : Type u_1} [Fintype ι] (q : ℝ) (e : ι ≃ ι) (s : ι → Bool) : (auxH ι q fun (l : ι) => s (e l)) = auxH ι q s

The auxiliary density is invariant under every permutation of its signs.

noncomputable def TriangleInflation.Graph.CycleWitnessAux.parWit (Γ : PairGraph) (t : ℕ) (q : ℝ) : GAssign Γ t → ℝ

The parity witness of a pair-source scenario at order t: push the auxiliary sign density forward along the parity read.

Equations

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

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_moment {Γ : PairGraph} {t : ℕ} (q : ℝ) (A : Finset (GObs Γ t)) : ∑ ω : GAssign Γ t, parWit Γ t q ω * ∏ o ∈ A, sgn (ω o) = if Even (latBd A).card then (-q) ^ ((latBd A).card / 2) else 0

The master moment identity. Every Walsh character of the parity witness is the auxiliary moment of the latent boundary of its index set.

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_nonneg {Γ : PairGraph} {t : ℕ} (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑(Fintype.card (GLatent Γ t)) ^ 2 * q ≤ 1 / 4) (ω : GAssign Γ t) : 0 ≤ parWit Γ t q ω

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_sum {Γ : PairGraph} {t : ℕ} (q : ℝ) : ∑ ω : GAssign Γ t, parWit Γ t q ω = 1

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_isLaw {Γ : PairGraph} {t : ℕ} (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑(Fintype.card (GLatent Γ t)) ^ 2 * q ≤ 1 / 4) : IsLaw (parWit Γ t q)

Symmetry

theorem TriangleInflation.Graph.CycleWitnessAux.gAncestors_gPerm {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (o : GObs Γ t) : gAncestors (gPerm π o) = Finset.image (⇑(Sound.gLatentPerm π)) (gAncestors o)

theorem TriangleInflation.Graph.CycleWitnessAux.parityRead_gLatentPerm {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) (s : GLatent Γ t → Bool) : (parityRead fun (l : GLatent Γ t) => s ((Sound.gLatentPerm π) l)) = gRelabel π (parityRead s)

theorem TriangleInflation.Graph.CycleWitnessAux.gRelabel_injective {Γ : PairGraph} {t : ℕ} (π : Γ.Edge → Equiv.Perm (Fin t)) : Function.Injective (gRelabel π)

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_symmetric {Γ : PairGraph} {t : ℕ} (q : ℝ) : GSymmetric t (parWit Γ t q)

The latent boundary of an ancestrally disjoint family

theorem TriangleInflation.Graph.CycleWitnessAux.latBd_subset_anc {Γ : PairGraph} {t : ℕ} (A : Finset (GObs Γ t)) : latBd A ⊆ gAncestorsOf A

theorem TriangleInflation.Graph.CycleWitnessAux.latBd_biUnion {Γ : PairGraph} {t : ℕ} {n : Type u_1} [Fintype n] (A : n → Finset (GObs Γ t)) (hd : ∀ (k k' : n), k ≠ k' → Disjoint (gAncestorsOf (A k)) (gAncestorsOf (A k'))) : latBd (Finset.univ.biUnion A) = Finset.univ.biUnion fun (k : n) => latBd (A k)

theorem TriangleInflation.Graph.CycleWitnessAux.latBd_biUnion_card {Γ : PairGraph} {t : ℕ} {n : Type u_1} [Fintype n] (A : n → Finset (GObs Γ t)) (hd : ∀ (k k' : n), k ≠ k' → Disjoint (gAncestorsOf (A k)) (gAncestorsOf (A k'))) : (latBd (Finset.univ.biUnion A)).card = ∑ k : n, (latBd (A k)).card

The edge structure of the cycle

def TriangleInflation.Graph.CycleWitnessAux.cyclePrev {m : ℕ} (v : Fin m) : Fin m

The predecessor vertex on the cycle.

Equations

• TriangleInflation.Graph.CycleWitnessAux.cyclePrev v = ⟨(↑v + (m - 1)) % m, ⋯⟩

theorem TriangleInflation.Graph.CycleWitnessAux.cycleNext_cyclePrev {m : ℕ} (v : Fin m) : cycleNext (cyclePrev v) = v

theorem TriangleInflation.Graph.CycleWitnessAux.cyclePrev_cycleNext {m : ℕ} (v : Fin m) : cyclePrev (cycleNext v) = v

theorem TriangleInflation.Graph.CycleWitnessAux.cycleNext_ne {m : ℕ} (hm : 2 ≤ m) (v : Fin m) : cycleNext v ≠ v

theorem TriangleInflation.Graph.CycleWitnessAux.cyclePrev_ne {m : ℕ} (hm : 2 ≤ m) (v : Fin m) : cyclePrev v ≠ v

theorem TriangleInflation.Graph.CycleWitnessAux.cycleNext_cycleNext_ne {m : ℕ} (hm : 3 ≤ m) (v : Fin m) : cycleNext (cycleNext v) ≠ v

theorem TriangleInflation.Graph.CycleWitnessAux.cycleAdj_next {m : ℕ} (hm : 2 ≤ m) (v : Fin m) : (cycleAdj m).Adj v (cycleNext v)

def TriangleInflation.Graph.CycleWitnessAux.ce {m : ℕ} (hm : 3 ≤ m) (j : Fin m) : (cycle m hm).Edge

The source of the cycle recorded by its lower endpoint: the edge {j, j+1}.

Equations

• TriangleInflation.Graph.CycleWitnessAux.ce hm j = ⟨s(j, TriangleInflation.Graph.cycleNext j), ⋯⟩

theorem TriangleInflation.Graph.CycleWitnessAux.ce_val {m : ℕ} (hm : 3 ≤ m) (j : Fin m) : ↑(ce hm j) = s(j, cycleNext j)

theorem TriangleInflation.Graph.CycleWitnessAux.mem_ce {m : ℕ} (hm : 3 ≤ m) (j v : Fin m) : v ∈ ↑(ce hm j) ↔ v = j ∨ v = cycleNext j

theorem TriangleInflation.Graph.CycleWitnessAux.ce_injective {m : ℕ} (hm : 3 ≤ m) : Function.Injective (ce hm)

theorem TriangleInflation.Graph.CycleWitnessAux.ce_surjective {m : ℕ} (hm : 3 ≤ m) (e : (cycle m hm).Edge) : ∃ (j : Fin m), e = ce hm j

theorem TriangleInflation.Graph.CycleWitnessAux.mem_inc_iff {Γ : PairGraph} (v : Γ.V) (e : Γ.Edge) : e ∈ Γ.inc v ↔ v ∈ ↑e

theorem TriangleInflation.Graph.CycleWitnessAux.mem_inc_ce {m : ℕ} (hm : 3 ≤ m) (v j : Fin m) : ce hm j ∈ (cycle m hm).inc v ↔ v = j ∨ v = cycleNext j

theorem TriangleInflation.Graph.CycleWitnessAux.mem_inc_cycle {m : ℕ} (hm : 3 ≤ m) (v : Fin m) (e : (cycle m hm).Edge) : e ∈ (cycle m hm).inc v ↔ e = ce hm (cyclePrev v) ∨ e = ce hm v

def TriangleInflation.Graph.CycleWitnessAux.incPrev {m : ℕ} (hm : 3 ≤ m) (v : Fin m) : ↥((cycle m hm).inc v)

The incident source recorded by the predecessor vertex.

Equations

• TriangleInflation.Graph.CycleWitnessAux.incPrev hm v = ⟨TriangleInflation.Graph.CycleWitnessAux.ce hm (TriangleInflation.Graph.CycleWitnessAux.cyclePrev v), ⋯⟩

def TriangleInflation.Graph.CycleWitnessAux.incSelf {m : ℕ} (hm : 3 ≤ m) (v : Fin m) : ↥((cycle m hm).inc v)

The incident source recorded by the vertex itself.

Equations

• TriangleInflation.Graph.CycleWitnessAux.incSelf hm v = ⟨TriangleInflation.Graph.CycleWitnessAux.ce hm v, ⋯⟩

theorem TriangleInflation.Graph.CycleWitnessAux.univ_inc_cycle {m : ℕ} (hm : 3 ≤ m) (v : Fin m) : Finset.univ = {incPrev hm v, incSelf hm v}

theorem TriangleInflation.Graph.CycleWitnessAux.mem_gAncestors_copyObs {m : ℕ} (hm : 3 ≤ m) {t : ℕ} (ι : (cycle m hm).Edge → Fin t) (v j : Fin m) (r : Fin t) : (ce hm j, r) ∈ gAncestors (copyObs ι v) ↔ r = ι (ce hm j) ∧ (v = cycleNext j ∨ v = j)

The latent boundary of a block of a copy of the cycle

def TriangleInflation.Graph.CycleWitnessAux.vtx {m : ℕ} (hm : 3 ≤ m) (v : (cycle m hm).V) : Fin m

The vertices of the cycle scenario are Fin m; this is that identification, written out so that equations between vertices elaborate at the type Fin m.

Equations

• TriangleInflation.Graph.CycleWitnessAux.vtx hm v = v

theorem TriangleInflation.Graph.CycleWitnessAux.vtx_copyObs {m t : ℕ} (hm : 3 ≤ m) (ι : (cycle m hm).Edge → Fin t) (v : Fin m) : vtx hm (copyObs ι v).fst = v

theorem TriangleInflation.Graph.CycleWitnessAux.eq_copyObs' {m t : ℕ} (hm : 3 ≤ m) {ι : (cycle m hm).Edge → Fin t} {o : GObs (cycle m hm) t} (h : o ∈ copySet ι) : o = copyObs ι (vtx hm o.fst)

def TriangleInflation.Graph.CycleWitnessAux.vertSet {m t : ℕ} (hm : 3 ≤ m) (A : Finset (GObs (cycle m hm) t)) : Finset (Fin m)

The vertex set of a set of copied observations.

Equations

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

theorem TriangleInflation.Graph.CycleWitnessAux.fst_injOn {m t : ℕ} (hm : 3 ≤ m) {ι : (cycle m hm).Edge → Fin t} {A : Finset (GObs (cycle m hm) t)} (hA : A ⊆ copySet ι) : Set.InjOn (fun (o : GObs (cycle m hm) t) => vtx hm o.fst) ↑A

theorem TriangleInflation.Graph.CycleWitnessAux.card_filter_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (A : Finset α) (f : α → β) (hinj : Set.InjOn f ↑A) (Q : β → Prop) [DecidablePred Q] : (Finset.filter Q (Finset.image f A)).card = {a ∈ A | Q (f a)}.card

theorem TriangleInflation.Graph.CycleWitnessAux.card_filter_pair {α : Type u_1} [DecidableEq α] (G : Finset α) (a b : α) (hab : a ≠ b) : {v ∈ G | v = a ∨ v = b}.card = (if a ∈ G then 1 else 0) + if b ∈ G then 1 else 0

theorem TriangleInflation.Graph.CycleWitnessAux.count_copy {m t : ℕ} (hm : 3 ≤ m) (ι : (cycle m hm).Edge → Fin t) {A : Finset (GObs (cycle m hm) t)} (hA : A ⊆ copySet ι) (j : Fin m) (r : Fin t) : {o ∈ A | (ce hm j, r) ∈ gAncestors o}.card = if r = ι (ce hm j) then {v ∈ vertSet hm A | v = cycleNext j ∨ v = j}.card else 0

theorem TriangleInflation.Graph.CycleWitnessAux.latBd_copy {m t : ℕ} (hm : 3 ≤ m) (ι : (cycle m hm).Edge → Fin t) {A : Finset (GObs (cycle m hm) t)} (hA : A ⊆ copySet ι) : latBd A = Finset.image (fun (j : Fin m) => (ce hm j, ι (ce hm j))) (cycleBoundary m (vertSet hm A))

theorem TriangleInflation.Graph.CycleWitnessAux.latBd_copy_card {m t : ℕ} (hm : 3 ≤ m) (ι : (cycle m hm).Edge → Fin t) {A : Finset (GObs (cycle m hm) t)} (hA : A ⊆ copySet ι) : (latBd A).card = (cycleBoundary m (vertSet hm A)).card

Moments of the cycle witness

theorem TriangleInflation.Graph.CycleWitnessAux.eq_of_moments {α : Type u_1} [Fintype α] {ι : Type u_2} [Finite ι] (E : α ≃ (ι → Bool)) (P Q : α → ℝ) (h : ∀ (F : Finset ι), ∑ a : α, P a * ∏ v ∈ F, sgn (E a v) = ∑ a : α, Q a * ∏ v ∈ F, sgn (E a v)) : P = Q

Walsh uniqueness transported along an identification of the sample space with a Boolean cube.

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_block_moment {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) (ι : (cycle m hm).Edge → Fin t) {A : Finset (GObs (cycle m hm) t)} (hA : A ⊆ copySet ι) : ∑ ω : GAssign (cycle m hm) t, parWit (cycle m hm) t q ω * ∏ o ∈ A, sgn (ω o) = (-q) ^ ((cycleBoundary m (vertSet hm A)).card / 2)

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_family_moment {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) {n : Type u_1} [Fintype n] (A : n → Finset (GObs (cycle m hm) t)) (ιf : n → (cycle m hm).Edge → Fin t) (hA : ∀ (k : n), A k ⊆ copySet (ιf k)) (hd : ∀ (k k' : n), k ≠ k' → Disjoint (gAncestorsOf (A k)) (gAncestorsOf (A k'))) : ∑ ω : GAssign (cycle m hm) t, parWit (cycle m hm) t q ω * ∏ o ∈ Finset.univ.biUnion A, sgn (ω o) = ∏ k : n, (-q) ^ ((cycleBoundary m (vertSet hm (A k))).card / 2)

theorem TriangleInflation.Graph.CycleWitnessAux.snd_of_mem_gAncestorsOf {Γ : PairGraph} {t : ℕ} {ι : Γ.Edge → Fin t} {A : Finset (GObs Γ t)} (hA : A ⊆ copySet ι) {l : GLatent Γ t} (hl : l ∈ gAncestorsOf A) : l.2 = ι l.1

Every copied ancestor of a member of a copy of the original scenario carries that copy's index.

The injectable marginals

theorem TriangleInflation.Graph.CycleWitnessAux.cycleTarget_moment' {m : ℕ} (hm : 3 ≤ m) (q : ℝ) (F : Finset (Fin m)) : ∑ w : (cycle m hm).V → Bool, cycleTarget m q w * ∏ v ∈ F, sgn (w v) = (-q) ^ ((cycleBoundary m F).card / 2)

The moments of the cycle target, read at the vertex type of the scenario.

theorem TriangleInflation.Graph.CycleWitnessAux.vertSet_image {m t : ℕ} (hm : 3 ≤ m) {S : Finset (GObs (cycle m hm) t)} (B : Finset ↥S) : vertSet hm (Finset.image (fun (p : ↥S) => ↑p) B) = Finset.image (fun (p : ↥S) => vtx hm (↑p).fst) B

theorem TriangleInflation.Graph.CycleWitnessAux.image_val_subset {m t : ℕ} (hm : 3 ≤ m) {S : Finset (GObs (cycle m hm) t)} (B : Finset ↥S) : Finset.image (fun (p : ↥S) => ↑p) B ⊆ S

theorem TriangleInflation.Graph.CycleWitnessAux.val_inj_on {m t : ℕ} {hm : 3 ≤ m} {S : Finset (GObs (cycle m hm) t)} (B : Finset ↥S) (_x : ↥S) : _x ∈ B → ∀ _y ∈ B, ↑_x = ↑_y → _x = _y

theorem TriangleInflation.Graph.CycleWitnessAux.target_block_moment {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) {S : Finset (GObs (cycle m hm) t)} (hS : GInjectable S) (B : Finset ↥S) : ∑ ψ : ↥S → Bool, pushforward (cycleTarget m q) (gPartyRead S) ψ * ∏ y ∈ B, sgn (ψ y) = (-q) ^ ((cycleBoundary m (Finset.image (fun (p : ↥S) => vtx hm (↑p).fst) B)).card / 2)

The target moment of a Walsh character of an injectable block.

theorem TriangleInflation.Graph.CycleWitnessAux.wit_block_moment {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) {S : Finset (GObs (cycle m hm) t)} (hS : GInjectable S) (B : Finset ↥S) : ∑ φ : ↥S → Bool, pushforward (parWit (cycle m hm) t q) (gRestrict S) φ * ∏ y ∈ B, sgn (φ y) = (-q) ^ ((cycleBoundary m (Finset.image (fun (p : ↥S) => vtx hm (↑p).fst) B)).card / 2)

The witness moment of a Walsh character of an injectable block.

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_injectable {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) : GInjectableMarginals t (parWit (cycle m hm) t q) (cycleTarget m q)

theorem TriangleInflation.Graph.CycleWitnessAux.gAncestorsOf_mono {Γ : PairGraph} {t : ℕ} {A A' : Finset (GObs Γ t)} (h : A ⊆ A') : gAncestorsOf A ⊆ gAncestorsOf A'

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_ai {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) : GAncestralProducts t (parWit (cycle m hm) t q) (cycleTarget m q)

The ancestral-independence prescriptions.

theorem TriangleInflation.Graph.CycleWitnessAux.card_cycle_edge {m : ℕ} (hm : 3 ≤ m) : Fintype.card (cycle m hm).Edge = m

theorem TriangleInflation.Graph.CycleWitnessAux.card_cycle_latent {m t : ℕ} (hm : 3 ≤ m) : Fintype.card (GLatent (cycle m hm) t) = m * t

theorem TriangleInflation.Graph.CycleWitnessAux.parWit_diag {m t : ℕ} (hm : 3 ≤ m) (q : ℝ) : pushforward (parWit (cycle m hm) t q) readDiag = gTensorPow t (cycleTarget m q)

The diagonal law of the witness is the tensor power of the cycle target.

theorem TriangleInflation.Graph.cycle_witness' (m t : ℕ) (hm : 3 ≤ m) (ht : 1 ≤ t) (q : ℝ) (hq : q = 1 / (4 * ↑m ^ 2 * ↑t ^ 2)) : GAIFeasible (cycle m hm) t (cycleTarget m q)

AUDIT-NOTES A5, the cycle witness. With N = mt auxiliary signs s_{v,i} carrying the positive density H_{N,q}(s) = 2^{−N} ∑_{|S| even} (−q)^{|S|/2} ∏_S s, and copied observations O_v^{ij} = s_{v−1,i} s_{v,j}, the target P_{m,q} with moments (−q)^{|∂F|/2} passes every AI prescription at order t, for q = 1/(4m²t²): the boundaries of ancestrally disjoint injectable blocks are disjoint, so their moments multiply.