The auxiliary vertex pool (R4 converse, #107)

Law-free geometry for the stationary extension: each sort's carrier is enlarged by a fresh pool copy,

PoolVertex S s := Vinfinite S s ⊕ Vinfinite S s,

with the original and pool embeddings, definitional disjointness and exhaustivity, a fixed sortwise identification with ℕ, structure transport along sortwise equivalences as a measurable equivalence, the two restriction maps, and the naturality laws between restriction, transport, and relabeling.

There is deliberately no "mixed permutation" subtype. The relabeling action on the extension quantifies over the raw full permutation family ∀ s, Equiv.Perm (PoolVertex S s) — permutations may move vertices between the two summands, and that freedom is load-bearing for the polling argument. Split permutations (Equiv.sumCongr) appear only in the naturality law for restriction, which is exactly the setting where the split hypothesis is honest: restriction does not commute with a permutation that crosses the boundary, and no such law is stated.

No law, no measure, no basis appears in this file.

The pooled carrier

@[reducible, inline]

abbrev RelSignature.PoolVertex (S : RelSignature) : S.Srt → Type

The enlarged carrier: an original copy and a fresh pool copy of the vertices, per sort.

Equations

• S.PoolVertex s = (S.Vinfinite s ⊕ S.Vinfinite s)

def RelSignature.originalVertex (S : RelSignature) (s : S.Srt) : S.Vinfinite s ↪ S.PoolVertex s

The original-vertex embedding.

Equations

• S.originalVertex s = { toFun := Sum.inl, inj' := ⋯ }

def RelSignature.poolVertex (S : RelSignature) (s : S.Srt) : S.Vinfinite s ↪ S.PoolVertex s

The pool-vertex embedding.

Equations

• S.poolVertex s = { toFun := Sum.inr, inj' := ⋯ }

theorem RelSignature.originalVertex_ne_poolVertex {S : RelSignature} (s : S.Srt) (v w : S.Vinfinite s) : (S.originalVertex s) v ≠ (S.poolVertex s) w

The two embeddings have disjoint images — definitionally, from Sum.

theorem RelSignature.originalVertex_or_poolVertex {S : RelSignature} (s : S.Srt) (x : S.PoolVertex s) : (∃ (v : S.Vinfinite s), x = (S.originalVertex s) v) ∨ ∃ (w : S.Vinfinite s), x = (S.poolVertex s) w

Every pooled vertex is an original vertex or a pool vertex — definitionally, from Sum.

def RelSignature.poolVertexEquiv (S : RelSignature) (s : S.Srt) : S.PoolVertex s ≃ S.Vinfinite s

The fixed sortwise identification of the pooled carrier with the vertex set: both summands together are again a countably infinite carrier. This is what transports the law in the cheap existence theorem.

Equations

• S.poolVertexEquiv s = Equiv.natSumNatEquivNat

Structure transport along sortwise equivalences

def RelSignature.RelStructure.congrCarrier {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ≃ W s) : S.RelStructure V ≃ᵐ S.RelStructure W

Transport of structures along a sortwise family of equivalences, as a measurable equivalence: the forward map carries a structure on V to a structure on W, reading each W-coordinate through e⁻¹. Both directions are comaps — the forward map is comap of the inverse family — so the inverse laws reduce to comap_comp and the equivalence cancellations.

Equations

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

@[simp]

theorem RelSignature.RelStructure.congrCarrier_apply {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ≃ W s) (X : S.RelStructure V) : (congrCarrier e) X = comap (fun (s : S.Srt) => ⇑(e s).symm) X

theorem RelSignature.RelStructure.congrCarrier_relabel {S : RelSignature} {V : S.Srt → Type u_1} {W : S.Srt → Type u_2} (e : (s : S.Srt) → V s ≃ W s) (σ : (s : S.Srt) → Equiv.Perm (V s)) (X : S.RelStructure V) : (congrCarrier e) (relabel σ X) = relabel (fun (s : S.Srt) => (e s).symm.trans (Equiv.trans (σ s) (e s))) ((congrCarrier e) X)

Transport–relabel naturality: relabeling by σ before transport is relabeling by the conjugated family after transport.

Restriction to the two halves

def RelSignature.restrictOriginal (S : RelSignature) : S.RelStructure S.PoolVertex → S.RelStructure S.Vinfinite

Restriction of an extended structure to the original vertices.

Equations

• S.restrictOriginal = RelSignature.RelStructure.restrict S.originalVertex

def RelSignature.restrictPool (S : RelSignature) : S.RelStructure S.PoolVertex → S.RelStructure S.Vinfinite

Restriction of an extended structure to the pool vertices.

Equations

• S.restrictPool = RelSignature.RelStructure.restrict S.poolVertex

theorem RelSignature.measurable_restrictOriginal {S : RelSignature} : Measurable S.restrictOriginal

theorem RelSignature.measurable_restrictPool {S : RelSignature} : Measurable S.restrictPool

theorem RelSignature.restrictOriginal_relabel_sumCongr {S : RelSignature} (σ τ : (s : S.Srt) → Equiv.Perm (S.Vinfinite s)) (X : S.RelStructure S.PoolVertex) : S.restrictOriginal (RelStructure.relabel (fun (s : S.Srt) => Equiv.sumCongr (σ s) (τ s)) X) = RelStructure.relabel σ (S.restrictOriginal X)

Restriction–relabel naturality, split case: a permutation that respects the original/pool split commutes with restriction to the original half — the original component acts before restriction. Definitional. Stated only for split permutations: restriction does not commute with a permutation crossing the boundary, and no such law holds or is claimed.

theorem RelSignature.restrictPool_relabel_sumCongr {S : RelSignature} (σ τ : (s : S.Srt) → Equiv.Perm (S.Vinfinite s)) (X : S.RelStructure S.PoolVertex) : S.restrictPool (RelStructure.relabel (fun (s : S.Srt) => Equiv.sumCongr (σ s) (τ s)) X) = RelStructure.relabel τ (S.restrictPool X)

The pool half of the split naturality law. Definitional.