The i.i.d.-edge regression for the successor contract (R4 converse, #107, #196) #
A hand-built rank 2 → 3 successor witness over digraphSig, testing staging and recovery
together — where the bipartite regression tested independence and symmetry.
The law is the symmetric i.i.d.-edge law: one uniform per two-point support, with
X_uv = X_vu = 1{U_{u,v} ≤ 1/2} and X_uu = false.
Keying the array by a coordinate's support gives both facts by construction: the two directed
coordinates of a block share a support and therefore a value, and the diagonal has a one-element
support so it falls in the default branch. Each still needs its support computed — see arr_symm
and arr_diagonal — but neither needs a choice of orientation. Blocks at distinct two-point supports are i.i.d.,
being distinct coordinates of the source. Making X_uv and X_vu independently directed would
introduce an equivariant-orientation problem without testing staging any better.
Shape of the regression #
- the rank-two coupling is defined independently as
iidEdgeLaw.prod (rankLatentSource 2), so independence of the edges from the old latents is literal; - the rank-three coupling is built from
rankLatentSource 3, retaining the whole latent point and decoding the array from its fresh rank-two layer; - the truncation identity is proved immediately, before either representation is packaged.
The edge layer: one uniform per two-point support.
Equations
Instances For
The symmetric i.i.d.-edge array, keyed by a coordinate's support. Both directed
coordinates of a two-point block share a support, hence a value; the diagonal has a one-element
support and is false.
Equations
Instances For
Symmetry by construction: the two directed coordinates of a block share a support.
The diagonal is false: its support has one element, not two.
The i.i.d.-edge law, defined from the edge layer alone.
Equations
Instances For
Equivariance and exchangeability #
Relabeling the vertices reindexes the edge layer along rankSupportPerm, because a coordinate's
support transports covariantly and its cardinality is preserved. Exchangeability is then the
invariance of an i.i.d. product under a coordinate permutation.
Equivariance of the array: relabeling the vertices is reindexing the edge layer.
Exchangeability: the law is invariant under every sortwise relabeling.
The i.i.d.-edge law as an exchangeable law on the infinite structure space.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Conditional independence from unconditional independence #
Kept private: it has one consumer (rank-two screening below), which is below the promotion bar
for Graphon/ForMathlib/. condExp_indep_eq supplies the constant conditional expectation of an
m₁-observation, but the remaining content is the intersection identity
E[1_{A ∩ B} | m'] = μ(A) · E[1_B | m'] for A in m₁ and B in m₂, which no available lemma
provides. Recorded as a prospective upstream candidate.
If m₁ is independent of m₂, then conditioning on anything inside m₂ cannot create a
dependence. Stated for abstract σ-algebras rather than for the two coordinates of a product,
because the consumer's ambient measure is a pushforward of a product, and the current API only
transports conditional independence backward. A source-level proof would therefore require a
new forward law-transport theorem; this regression instead transports the unconditional
independence, which the existing API does supply, and applies the conditioning lemma on the
coupling.
One elaboration point is load-bearing: an abstract MeasurableSpace Ω binder enters local
instance search and can shadow the ambient instance throughout the proof body. The conclusion is
therefore written in explicit @ form and the proof opens with a letI restoring the intended
ambient instance, neither of which weakens the statement.
The two couplings, described independently #
The rank-two coupling is a product, so independence of the edges from the old latents is literal. The rank-three coupling is built from the rank-three source and decodes the array from its fresh rank-two layer. The truncation identity is proved immediately, before either representation is packaged.
The rank-two coupling: the i.i.d.-edge law together with an independent rank-two latent array. Defined without reference to the rank-three object.
Equations
Instances For
The fresh rank-two layer of a rank-three latent point.
Equations
Instances For
The rank-three coupling: the array is decoded from the fresh rank-two layer, and the whole rank-three latent point is retained.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The truncation identity — the gate: truncating the rank-three coupling's latents to rank two returns the independently defined rank-two coupling. The fresh edge layer splits off from the old latents, the array reads only the former and the truncation only the latter.
Blocks read a single edge coordinate #
Two pointwise lemmas, proved before any measure is touched: a block below rank two is constant
false, and a block at a two-point support reads exactly the edge coordinate keyed by that
support. Everything downstream — recovery at both ranks and screening at rank two — is a
consequence of these.
Rank-two invariance and recovery #
Rank-two invariance: the coupling is a product of two invariant factors.
Rank-two local recovery: below rank two every block is constant false, so the decoder
is a constant and reads no latent at all.
Rank three: deterministic recovery and a vacuous screening clause #
At rank three recovery is the substantive clause — a two-point block is decoded from the latent coordinate at its own support, which the rank-three array carries. Screening, by contrast, is vacuous: over a binary signature no coordinate reads three vertices, so a three-point block space is a single point.
The fresh rank-two layer of a rank-three latent point reads the coordinate at that support.
The rank-three decoder at a two-point support: read the local latent at that very support.
Instances For
Rank-three local recovery: below rank three a block is either constant false or, at a
two-point support, decoded from the latent coordinate at that support — which the rank-three
array carries, since 2 < 3. This is the staging clause the regression exists to exercise.
The rank hypothesis is not consumed: for this law recovery happens to hold at every support,
since a block whose support does not have two elements is constant. The hypothesis is kept because
lower_recovers supplies it.
Over a binary signature a coordinate reads at most two vertices.
No coordinate has a three-point support, so a rank-three block space is a single point — which is why the rank-three screening clause carries no probabilistic content.
Rank-two screening #
At a two-point support the block reads one coordinate of the edge source, while the remainder reads the other coordinates together with the whole latent array — an independent factor. So the block is independent of the remainder outright, and screening follows from independence rather than from determinism. That is the case the bipartite regression could not exercise: there the rank-two block was a function of the latents visible at its support, so screening was immediate.
The argument accordingly establishes the unconditional independence and transports that. This is
an API constraint, not a mathematical one: for these observables, with conditioning generated by a
function, conditional independence is determined by their joint law and would transport too — but
the repository has only backward transport (condIndepFun_comp_measurePreserving and its
relatives), so using it here would mean proving a forward law-transport theorem first. Pushing the
unconditional independence forward needs no new theorem.
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 independent of that remainder outright, and the conditioning algebra sits inside the remainder's.
Rank-three invariance, the two representations, and the successor witness #
The fresh layer intertwines the rank-three latent action with the vertex action.
The exact pointwise joint action at rank three.
Rank-three invariance: the joint action, then source invariance.
The rank-two representation of the i.i.d.-edge law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The rank-three representation of the same law.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The successor witness: the rank-three representation truncates back to the independently defined rank-two one, on the nose.
Equations
Instances For
Nondegeneracy and the decoding identity #
Two statements recording that the regression is not vacuous. The half-threshold makes each edge present with probability exactly one half, so no block is almost surely constant and the screening clause has content; and at rank three the edge at a two-point support is visibly the thresholded latent coordinate keyed by that support.
The source mass of a half-threshold event at one coordinate is exactly one half.
Nondegeneracy: each edge at a two-point support is present with probability exactly one half. The block is therefore not almost surely constant, so rank-two screening is a genuine conditional-independence statement rather than a determinism statement in disguise.
The decoding identity: under the rank-three coupling the edge at a two-point support is the thresholded latent coordinate keyed by that support — the staging property in its most concrete form.