The bipartite regression for the successor contract (R4 converse, #107)

A hand-built rank 1 → 2 successor witness for the one-sort binary signature digraphSig, whose purpose is to test that RankSuccessor is an expressive specification — before either general route is attempted, so that the acceptance battery cannot be shaped by an implementation.

The array is the bipartite XOR law: each vertex carries an i.i.d. colour, and the edge X_uv is the parity colour u ⊕ colour v.

What makes this a regression rather than merely a construction

• the array law bipartiteLaw is defined from the fresh singleton layer alone, and the rank-one coupling C is defined as the independent product bipartiteLaw × rankLatentSource 1. Neither is read off the rank-two coupling, so the truncation identity compares two separately described couplings and genuinely uses the source factorization;
• the nonindependence witness is numerical, not merely functional: X_01 and the matching colour-parity event have joint probability 1/2 against a product of marginals 1/4. "The edge is a function of the colours" would also hold for a constant edge and would certify nothing;
• the rank-two decoder recovers both directed coordinates X_uv and X_vu of the support-{u,v} block as the same parity, so symmetry is exhibited as a property of this law rather than something hidden in the signature. The diagonal singleton block is constantly false, which the XOR definition delivers for free.

@[reducible, inline]

abbrev RelSignature.BipartiteRegression.Colours : Type

The fresh singleton layer of the rank-two latent cube: one uniform per vertex.

Equations

• RelSignature.BipartiteRegression.Colours = (digraphSig.RankSupport 1 → ℝ)

def RelSignature.BipartiteRegression.vertexSupport (v : ℕ) : digraphSig.RankSupport 1

The singleton support at a vertex.

Equations

• RelSignature.BipartiteRegression.vertexSupport v = ⟨{⟨(), v⟩}, ⋯⟩

noncomputable def RelSignature.BipartiteRegression.colour (ω : Colours) (v : ℕ) : Bool

The colour of a vertex, read off its own fresh coordinate.

Equations

• RelSignature.BipartiteRegression.colour ω v = decide (ω (RelSignature.BipartiteRegression.vertexSupport v) ≤ 1 / 2)

noncomputable def RelSignature.BipartiteRegression.arr (ω : Colours) : digraphSig.RelStructure digraphSig.Vinfinite

The bipartite array: the edge at an ordered pair is the parity of the two colours. The diagonal is constantly false because b ⊕ b = false.

Equations

• RelSignature.BipartiteRegression.arr ω c = (RelSignature.BipartiteRegression.colour ω (c.snd 0) ^^ RelSignature.BipartiteRegression.colour ω (c.snd 1))

@[simp]

theorem RelSignature.BipartiteRegression.arr_apply (ω : Colours) (u v : ℕ) : arr ω (digraphCoord u v) = (colour ω u ^^ colour ω v)

@[simp]

theorem RelSignature.BipartiteRegression.arr_diagonal (ω : Colours) (v : ℕ) : arr ω (digraphCoord v v) = false

The diagonal is constantly false — the singleton-support block of this law carries no information, which is what makes its rank-one recovery and screening deterministic.

theorem RelSignature.BipartiteRegression.measurable_colour (v : ℕ) : Measurable fun (ω : Colours) => colour ω v

theorem RelSignature.BipartiteRegression.measurable_arr : Measurable arr

The relabeling action on the fresh layer

noncomputable def RelSignature.BipartiteRegression.supportPerm (σ : Equiv.Perm ℕ) : digraphSig.RankSupport 1 ≃ digraphSig.RankSupport 1

A permutation of the vertices permutes the singleton supports — the rank-one instance of the generic rankSupportPerm.

Equations

• RelSignature.BipartiteRegression.supportPerm σ = RelSignature.rankSupportPerm (fun (x : Unit) => σ) 1

@[simp]

theorem RelSignature.BipartiteRegression.supportPerm_vertexSupport (σ : Equiv.Perm ℕ) (v : ℕ) : (supportPerm σ) (vertexSupport v) = vertexSupport (σ v)

theorem RelSignature.BipartiteRegression.colour_comp_supportPerm (σ : Equiv.Perm ℕ) (ω : Colours) (v : ℕ) : colour (fun (A : digraphSig.RankSupport 1) => ω ((supportPerm σ) A)) v = colour ω (σ v)

theorem RelSignature.BipartiteRegression.arr_comp_supportPerm (σ : Equiv.Perm ℕ) (ω : Colours) : (arr fun (A : digraphSig.RankSupport 1) => ω ((supportPerm σ) A)) = RelStructure.relabel (fun (x : Unit) => σ) (arr ω)

Equivariance of the array: relabeling the vertices is reindexing the fresh layer.

The array law

noncomputable def RelSignature.BipartiteRegression.bipartiteLaw : MeasureTheory.Measure (digraphSig.RelStructure digraphSig.Vinfinite)

The bipartite law, defined from the fresh singleton layer alone — deliberately not read off the rank-two coupling, so that the truncation identity later compares two independently described couplings.

Equations

• RelSignature.BipartiteRegression.bipartiteLaw = MeasureTheory.Measure.map RelSignature.BipartiteRegression.arr (MeasureTheory.iidUniformSource (digraphSig.RankSupport 1))

instance RelSignature.BipartiteRegression.instIsProbabilityMeasureRelStructureDigraphSigVinfiniteBipartiteLaw : MeasureTheory.IsProbabilityMeasure bipartiteLaw

theorem RelSignature.BipartiteRegression.bipartiteLaw_map_relabel (σ : Unit → Equiv.Perm ℕ) : MeasureTheory.Measure.map (RelStructure.relabel σ) bipartiteLaw = bipartiteLaw

noncomputable def RelSignature.BipartiteRegression.bipartiteExchangeable : digraphSig.InfiniteRelExchangeableLaw

The bipartite law as an exchangeable law on the infinite structure space.

Equations

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

Blocks of this signature

For digraphSig every coordinate has a two-element or one-element support, never the empty one, and a singleton support forces the diagonal coordinate.

instance RelSignature.BipartiteRegression.instIsEmptyBlockIndexEmptyCollectionFinsetSigmaUnitNat : IsEmpty (BlockIndex ∅)

@[implicit_reducible]

instance RelSignature.BipartiteRegression.instUniqueBlockSpaceEmptyCollectionFinsetSigmaUnitNat : Unique (BlockSpace ∅)

Equations

• RelSignature.BipartiteRegression.instUniqueBlockSpaceEmptyCollectionFinsetSigmaUnitNat = Pi.uniqueOfIsEmpty fun (a : RelSignature.BlockIndex ∅) => Bool

theorem RelSignature.BipartiteRegression.eq_digraphCoord_of_support_singleton {v : ℕ} (c : BlockIndex {⟨(), v⟩}) : ↑c = digraphCoord v v

A coordinate whose support is the singleton {v} is the diagonal coordinate at v.

theorem RelSignature.BipartiteRegression.blockMap_singleton_arr (ω : Colours) (v : ℕ) : blockMap {⟨(), v⟩} (arr ω) = fun (x : BlockIndex {⟨(), v⟩}) => false

The singleton block of this law is constantly false — it reads only the diagonal.

The rank-one coupling, defined independently of the rank-two one

noncomputable def RelSignature.BipartiteRegression.rankOneCoupling : MeasureTheory.Measure (digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 1)

The rank-one coupling: the bipartite law together with an independent global uniform U_∅. At rank one the latent cube is exactly that one coordinate — it is not trivial, and this coupling is described without reference to the rank-two object.

Equations

• RelSignature.BipartiteRegression.rankOneCoupling = RelSignature.BipartiteRegression.bipartiteLaw.prod (digraphSig.rankLatentSource 1)

instance RelSignature.BipartiteRegression.instIsProbabilityMeasureProdRelStructureDigraphSigVinfiniteRankLatentSpaceOfNatNatRankOneCoupling : MeasureTheory.IsProbabilityMeasure rankOneCoupling

@[simp]

theorem RelSignature.BipartiteRegression.rankOneCoupling_map_fst : MeasureTheory.Measure.map Prod.fst rankOneCoupling = bipartiteLaw

@[simp]

theorem RelSignature.BipartiteRegression.rankOneCoupling_map_snd : MeasureTheory.Measure.map Prod.snd rankOneCoupling = digraphSig.rankLatentSource 1

theorem RelSignature.BipartiteRegression.ae_blockMap_singleton (v : ℕ) : ∀ᵐ (X : digraphSig.RelStructure digraphSig.Vinfinite) ∂bipartiteLaw, blockMap {⟨(), v⟩} X = fun (x : BlockIndex {⟨(), v⟩}) => false

The singleton block is a.e. constant under the bipartite law.

noncomputable def RelSignature.BipartiteRegression.rankOneRep : bipartiteExchangeable.RankRepresentation 1

The rank-one representation, built directly from the independently described coupling.

Equations

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

The rank-two coupling and the three central identities

The identities are proved immediately after the definition, before invariance or screening add noise. The third is the real gate: it visibly consumes the source factorization.

noncomputable def RelSignature.BipartiteRegression.freshLayer (ω : digraphSig.RankLatentSpace 2) : Colours

The fresh singleton layer of a rank-two latent point.

Equations

• RelSignature.BipartiteRegression.freshLayer ω = ((RelSignature.rankLatentSpaceSuccEquiv 1) ω).2

theorem RelSignature.BipartiteRegression.measurable_freshLayer : Measurable freshLayer

noncomputable def RelSignature.BipartiteRegression.rankTwoCoupling : MeasureTheory.Measure (digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2)

The rank-two coupling: the array is built from the fresh singleton layer, and the whole rank-two latent point is retained.

Equations

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

theorem RelSignature.BipartiteRegression.measurable_rankTwoMap : Measurable fun (ω : digraphSig.RankLatentSpace 2) => (arr (freshLayer ω), ω)

instance RelSignature.BipartiteRegression.instIsProbabilityMeasureProdRelStructureDigraphSigVinfiniteRankLatentSpaceOfNatNatRankTwoCoupling : MeasureTheory.IsProbabilityMeasure rankTwoCoupling

theorem RelSignature.BipartiteRegression.map_freshLayer : MeasureTheory.Measure.map freshLayer (digraphSig.rankLatentSource 2) = MeasureTheory.iidUniformSource (digraphSig.RankSupport 1)

The fresh layer carries the i.i.d. singleton source — the second factor of the successor split.

@[simp]

theorem RelSignature.BipartiteRegression.rankTwoCoupling_map_fst : MeasureTheory.Measure.map Prod.fst rankTwoCoupling = bipartiteLaw

Identity 1: the structure marginal is the bipartite law.

@[simp]

theorem RelSignature.BipartiteRegression.rankTwoCoupling_map_snd : MeasureTheory.Measure.map Prod.snd rankTwoCoupling = digraphSig.rankLatentSource 2

Identity 2: the latent marginal is the rank-two source.

theorem RelSignature.BipartiteRegression.rankTwoCoupling_truncation : MeasureTheory.Measure.map (Prod.map id (rankLatentProjection ⋯)) rankTwoCoupling = rankOneCoupling

Identity 3 — the gate: truncating the rank-two coupling's latents to rank one returns the independently defined rank-one coupling. This is where the source factorization is consumed: U_∅ splits off from the singleton layer, the array depends only on the latter, and the truncation reads only the former.

Recovery below rank two

lower_recovers at rank two ranges over supports of cardinality < 2, so it sees only the empty and singleton cases — never a two-point support. Both blocks are deterministic: the empty one is vacuous for this signature, the singleton one is the constantly-false diagonal. The two-point decoder plays no part here.

theorem RelSignature.BipartiteRegression.lower_recovers_rank_two (A : Finset ((_ : Unit) × ℕ)) (hA : A.card < 2) : ∃ (g : LocalLatentSpace A 2 → BlockSpace A), Measurable g ∧ (fun (p : digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2) => blockMap A p.1) =ᵐ[rankTwoCoupling] fun (p : digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2) => g (localLatents A 2 p.2)

The two-point deterministic block

The organizing lemma for rank-two screening and for the public XOR identity: on a two-point support the whole directed block — both coordinates X_uv and X_vu — is a deterministic function of the two singleton latents visible there. Recovering both as the same parity is what exhibits symmetry as a property of this law rather than of the signature.

def RelSignature.BipartiteRegression.pairSupport (u v : ℕ) : Finset ((_ : Unit) × ℕ)

The two-point support at a pair of distinct vertices.

Equations

• RelSignature.BipartiteRegression.pairSupport u v = {⟨(), u⟩, ⟨(), v⟩}

@[simp]

theorem RelSignature.BipartiteRegression.mem_pairSupport_left (u v : ℕ) : ⟨(), u⟩ ∈ pairSupport u v

@[simp]

theorem RelSignature.BipartiteRegression.mem_pairSupport_right (u v : ℕ) : ⟨(), v⟩ ∈ pairSupport u v

def RelSignature.BipartiteRegression.pairLocalIndex (u v w : ℕ) (h : ⟨(), w⟩ ∈ pairSupport u v) : LocalLatentIndex (pairSupport u v) 2

A vertex of the pair, as a latent index visible at that support.

Equations

• RelSignature.BipartiteRegression.pairLocalIndex u v w h = ⟨⟨{⟨(), w⟩}, ⋯⟩, ⋯⟩

noncomputable def RelSignature.BipartiteRegression.twoPointDecoder (u v : ℕ) : LocalLatentSpace (pairSupport u v) 2 → BlockSpace (pairSupport u v)

The two-point decoder: read the two singleton latents and return their parity, for every coordinate of the block.

Equations

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

theorem RelSignature.BipartiteRegression.measurable_twoPointDecoder (u v : ℕ) : Measurable (twoPointDecoder u v)

theorem RelSignature.BipartiteRegression.coord_of_pair {u v : ℕ} (huv : u ≠ v) (c : BlockIndex (pairSupport u v)) : (↑c).snd 0 = u ∧ (↑c).snd 1 = v ∨ (↑c).snd 0 = v ∧ (↑c).snd 1 = u

A coordinate of a two-point block is one of the two directed pairs.

theorem RelSignature.BipartiteRegression.freshLayer_vertexSupport (ω : digraphSig.RankLatentSpace 2) (w : ℕ) : freshLayer ω (vertexSupport w) = ω ⟨{⟨(), w⟩}, ⋯⟩

The fresh layer at a vertex is the rank-two latent at that singleton support.

theorem RelSignature.BipartiteRegression.blockMap_pair_arr {u v : ℕ} (huv : u ≠ v) (ω : digraphSig.RankLatentSpace 2) : blockMap (pairSupport u v) (arr (freshLayer ω)) = twoPointDecoder u v (localLatents (pairSupport u v) 2 ω)

The organizing lemma: on a two-point support the whole directed block is the deterministic parity of the two singleton latents visible there. Both X_uv and X_vu decode to the same value, so the symmetry of this law is exhibited rather than assumed.

Rank-two screening

The arbitrary two-point support is normalized to pairSupport u v first, so that the deterministic-block lemma applies directly and no dependent block or local-latent space has to be transported across a later equality.

theorem RelSignature.BipartiteRegression.exists_pairSupport_of_card_two {A : Finset ((_ : Unit) × ℕ)} (hA : A.card = 2) : ∃ (u : ℕ) (v : ℕ), u ≠ v ∧ A = pairSupport u v

A support of cardinality two is a pairSupport at distinct vertices.

theorem RelSignature.BipartiteRegression.ae_blockMap_pair {u v : ℕ} (huv : u ≠ v) : (fun (p : digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2) => blockMap (pairSupport u v) p.1) =ᵐ[rankTwoCoupling] fun (p : digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2) => twoPointDecoder u v (localLatents (pairSupport u v) 2 p.2)

The decoder identity holds a.e. under the rank-two coupling.

theorem RelSignature.BipartiteRegression.screening_rank_two (A : Finset ((_ : Unit) × ℕ)) (hA : A.card = 2) : ProbabilityTheory.CondIndepFun (MeasurableSpace.comap (localLatents A 2 ∘ Prod.snd) inferInstance) ⋯ (blockMap A ∘ Prod.fst) (restObservation 2 A) rankTwoCoupling

Rank-two screening: at a two-point support the block is conditionally independent of the rank-truncated remainder given the latents visible there — because it is a measurable function of them.

The joint action

One exact pointwise lemma, proved before any measure is touched, so that the inverse and orientation conventions are isolated in a single place.

theorem RelSignature.BipartiteRegression.rankSupportEquiv_eq_supportPerm (σ : ↥digraphSig.FinSuppPerm) (A : digraphSig.RankSupport 1) : (rankSupportEquiv σ 1) A = (supportPerm (↑σ ())) A

The finitely supported rank-support action agrees with the full-permutation helper. Kept local to this file: the two serve genuinely different APIs.

theorem RelSignature.BipartiteRegression.freshLayer_rankLatentRelabel (σ : ↥digraphSig.FinSuppPerm) (ω : digraphSig.RankLatentSpace 2) : freshLayer ((rankLatentRelabel σ 2) ω) = fun (A : digraphSig.RankSupport 1) => freshLayer ω ((supportPerm (↑σ ())) A)

The fresh layer intertwines the rank-two latent action with the vertex action.

theorem RelSignature.BipartiteRegression.jointMap_rankLatentRelabel (σ : ↥digraphSig.FinSuppPerm) (ω : digraphSig.RankLatentSpace 2) : (arr (freshLayer ((rankLatentRelabel σ 2) ω)), (rankLatentRelabel σ 2) ω) = Prod.map (RelStructure.relabel ↑σ) ⇑(rankLatentRelabel σ 2) (arr (freshLayer ω), ω)

The exact pointwise joint action. Relabeling the rank-two latent point and then building the pair is the same as building the pair and acting diagonally.

theorem RelSignature.BipartiteRegression.rankTwoCoupling_invariant (σ : ↥digraphSig.FinSuppPerm) : MeasureTheory.Measure.map (Prod.map (RelStructure.relabel ↑σ) ⇑(rankLatentRelabel σ 2)) rankTwoCoupling = rankTwoCoupling

Rank-two invariance, now just Measure.map_map, the joint action, and source invariance.

The representation and the successor witness

noncomputable def RelSignature.BipartiteRegression.rankTwoRep : bipartiteExchangeable.RankRepresentation 2

The rank-two representation. Every field is one of the theorems above.

Equations

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

noncomputable def RelSignature.BipartiteRegression.bipartiteSuccessor : InfiniteRelExchangeableLaw.RankSuccessor rankOneRep

The successor witness: a two-field literal whose truncation proof is exactly the gate identity. This is the regression's headline — the contract is satisfied by an explicit rank 1 → 2 example whose two couplings were described independently.

Equations

• RelSignature.BipartiteRegression.bipartiteSuccessor = { next := RelSignature.BipartiteRegression.rankTwoRep, truncation := RelSignature.BipartiteRegression.rankTwoCoupling_truncation }

The public XOR identity

A coordinate projection of the deterministic-block lemma — no second pushforward calculation.

theorem RelSignature.BipartiteRegression.support_digraphCoord {u v : ℕ} : (digraphCoord u v).support = pairSupport u v

The directed coordinate at a pair of distinct vertices lies in that pair's block.

theorem RelSignature.BipartiteRegression.ae_edge_xor {u v : ℕ} (huv : u ≠ v) : ∀ᵐ (p : digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2) ∂rankTwoCoupling, p.1 (digraphCoord u v) = (colour (freshLayer p.2) u ^^ colour (freshLayer p.2) v)

The XOR identity: almost surely the edge at a pair of distinct vertices is the parity of their two colours. Obtained by evaluating the block identity at one coordinate.

The numerical nonindependence witness

"The edge is a function of the colours" would also hold for a constant edge. What rules that out is arithmetic: the edge event and the matching colour-parity event each have probability 1/2, they coincide, and so their joint probability is 1/2 against a product of marginals 1/4.

def RelSignature.BipartiteRegression.pairIndex : Fin 2 → digraphSig.RankSupport 1

The two vertices 0 and 1, as fresh-layer indices.

Equations

• RelSignature.BipartiteRegression.pairIndex = ![RelSignature.BipartiteRegression.vertexSupport 0, RelSignature.BipartiteRegression.vertexSupport 1]

theorem RelSignature.BipartiteRegression.vertexSupport_injective : Function.Injective vertexSupport

theorem RelSignature.BipartiteRegression.pairIndex_injective : Function.Injective pairIndex

theorem RelSignature.BipartiteRegression.source_map_pairIndex : MeasureTheory.Measure.map (fun (x : digraphSig.RankSupport 1 → ℝ) (d : Fin 2) => x (pairIndex d)) (MeasureTheory.iidUniformSource (digraphSig.RankSupport 1)) = MeasureTheory.Measure.pi fun (x : Fin 2) => MeasureTheory.uniform01

The two-vertex marginal of the fresh source is the two-fold uniform product.

theorem RelSignature.BipartiteRegression.uniform01_Iic_half : MeasureTheory.uniform01 (Set.Iic (1 / 2)) = 1 / 2

theorem RelSignature.BipartiteRegression.uniform01_Iic_half_compl : MeasureTheory.uniform01 (Set.Iic (1 / 2))ᶜ = 1 / 2

theorem RelSignature.BipartiteRegression.measure_xorTrue : (MeasureTheory.Measure.pi fun (x : Fin 2) => MeasureTheory.uniform01) {y : Fin 2 → ℝ | (decide (y 0 ≤ 1 / 2) ^^ decide (y 1 ≤ 1 / 2)) = true} = 1 / 2

The XOR event has mass one half on the two-vertex marginal: it is the disjoint union of two rectangles, each of mass 1/4.

Nonindependence

All null-set reasoning lives in one a.e. event-equivalence lemma; the final theorem is purely numerical.

def RelSignature.BipartiteRegression.parityEvent : Set (digraphSig.RankLatentSpace 2)

The latent-side parity event.

Equations

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

def RelSignature.BipartiteRegression.edgeEvent : Set (digraphSig.RelStructure digraphSig.Vinfinite)

The structure-side edge event.

Equations

• RelSignature.BipartiteRegression.edgeEvent = {X : digraphSig.RelStructure digraphSig.Vinfinite | X (digraphCoord 0 1) = true}

theorem RelSignature.BipartiteRegression.measurableSet_parityEvent : MeasurableSet parityEvent

theorem RelSignature.BipartiteRegression.measurableSet_edgeEvent : MeasurableSet edgeEvent

theorem RelSignature.BipartiteRegression.measure_parityEvent : rankTwoCoupling (Prod.snd ⁻¹' parityEvent) = 1 / 2

The latent parity event has probability one half, transported from the two-vertex marginal.

theorem RelSignature.BipartiteRegression.ae_edgeEvent_iff_parityEvent : ∀ᵐ (p : digraphSig.RelStructure digraphSig.Vinfinite × digraphSig.RankLatentSpace 2) ∂rankTwoCoupling, p ∈ Prod.fst ⁻¹' edgeEvent ↔ p ∈ Prod.snd ⁻¹' parityEvent

The one a.e. event equivalence: the pulled-back edge and parity events agree.

theorem RelSignature.BipartiteRegression.measure_edgeEvent : rankTwoCoupling (Prod.fst ⁻¹' edgeEvent) = 1 / 2

The edge event has probability one half.

theorem RelSignature.BipartiteRegression.measure_edge_inter_parity : rankTwoCoupling (Prod.fst ⁻¹' edgeEvent ∩ Prod.snd ⁻¹' parityEvent) = 1 / 2

Their intersection also has probability one half — they coincide.

theorem RelSignature.BipartiteRegression.not_indepFun_rankTwoCoupling : ¬ProbabilityTheory.IndepFun Prod.fst Prod.snd rankTwoCoupling

The array is not independent of its new latent layer. A constant edge would also be "a function of the colours"; what rules that out is that 1/2 ≠ 1/4.