feat: the bipartite regression for the successor contract (#196) - #203
Merged
Conversation
…sentation The XOR array over digraphSig: each vertex carries an i.i.d. colour on its own fresh singleton coordinate, and the edge is the parity. The diagonal is constantly false for free, since b XOR b = false. bipartiteLaw is defined from the FRESH SINGLETON LAYER ALONE — not read off any rank-two object — with exchangeability from the equivariance arr (ω ∘ supportPerm σ) = relabel σ (arr ω) plus source invariance under an index equivalence. rankOneRep : RankRepresentation 1 with P := bipartiteLaw.prod (rankLatentSource 1), the independent product. Its invariance uses the rank-one latent action being the identity; lower_recovers is trivial because no coordinate of this signature has empty support, so the rank-zero block space is a point; screening is condIndepFun_const_left transported by CondIndepFun.congr, since the singleton block reads only the constantly-false diagonal.
Proved immediately after the definition, before invariance or screening add noise, as directed: 1. rankTwoCoupling_map_fst = bipartiteLaw 2. rankTwoCoupling_map_snd = rankLatentSource 2 3. rankTwoCoupling_truncation = rankOneCoupling — the gate The third visibly consumes rankLatentSource_map_rankLatentSpaceSuccEquiv: U_∅ splits off from the singleton layer, the array reads only the latter, the truncation reads only the former, and Measure.prod_swap plus map_prod_map reassemble the independently defined product. It passed with only orientation fixes, which is exactly what proving it early was meant to surface.
lower_recovers at rank two ranges over supports of cardinality < 2, so it sees only the empty and singleton cases and never a two-point support — the two-point decoder plays no part. The empty case is vacuous for this signature (no coordinate has empty support), the singleton case is the constantly-false diagonal, transported through identity 1 (rankTwoCoupling_map_fst) as a measure-preserving projection. Statement pins (S := digraphSig) on LocalLatentSpace/BlockSpace/ localLatents: with A : Finset (Σ _ : Unit, ℕ) the signature is otherwise a metavariable.
blockMap_pair_arr: 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 — symmetry exhibited as a property of this law, not of the signature. Supporting: pairSupport / pairLocalIndex / twoPointDecoder with its measurability, coord_of_pair (a two-point block coordinate is one of the two directed pairs, the degenerate diagonal cases ruled out by u ≠ v via the two vertex witnesses), and freshLayer_vertexSupport, which is rfl — the successor split's inverse keeps the same underlying finset, so the decoder reads the fresh layer with no transport. This lemma organizes rank-two screening and the public XOR identity, and nothing else: lower_recovers at rank two ranges over cardinality < 2 and keeps its own vacuous/constant-diagonal proof.
exists_pairSupport_of_card_two normalizes an arbitrary two-point support to pairSupport u v with u ≠ v FIRST, via an obtain with rfl, so blockMap_pair_arr applies directly and no dependent block or local-latent space is transported across a later equality. Screening is then exactly the three steps: push the source-level decoder identity to an a.e. identity under rankTwoCoupling (ae_blockMap_pair, via ae_map_iff and measurableSet_eq_fun), replace the block observation with CondIndepFun.congr, and discharge conditional independence with condIndepFun_of_measurable_left — the decoder is measurable through localLatents, hence measurable for the conditioning sigma-algebra by comap_measurable. No conditional-expectation reasoning appears.
rankTwoRep assembles all seven fields from the theorems above, and bipartiteSuccessor : RankSuccessor rankOneRep is a two-field literal whose truncation proof is exactly rankTwoCoupling_truncation. The successor contract is now satisfied by an explicit rank 1 -> 2 example whose two couplings were described INDEPENDENTLY — the array law from the fresh singleton layer, the rank-one coupling as a product with U_∅ — so the truncation identity is a theorem about two separate descriptions rather than bookkeeping. Invariance came from one exact pointwise joint-action lemma proved before any measure was touched, isolating the orientation conventions; the rankSupportEquiv/supportPerm bridge is kept local, since the finitely supported rank action and the full-permutation helper serve different APIs.
ae_edge_xor: almost surely the edge at a pair of distinct vertices is the parity of their two colours. Obtained by evaluating the deterministic-block identity at one coordinate — no second pushforward calculation, as intended. support_digraphCoord records that the directed coordinate lies in that pair's block.
It is a general fact about uniform01, which is defined in SamplerSources, but it lived in the graph-specific InfiniteSampler. The bipartite regression needs it and must not import that module for it. Both existing consumers (InfiniteSampler, SampleExposure) compile unchanged, since they already import SamplerSources.
Via the repository-native route: Measure.infinitePi_map_comp_of_injective at delta := Fin 2 with f := ![vertexSupport 0, vertexSupport 1] gives the two-vertex marginal as Measure.pi (fun _ : Fin 2 => uniform01); the XOR-true event is the disjoint union of the two rectangles Iic(1/2) x Iic(1/2)ᶜ and its mirror, each of mass 1/4 by Measure.pi_pi with uniform01_Iic_half and its complement. This is the arithmetic that rules out the degenerate reading: a constant edge would also be 'a function of the colours', but could not have this mass.
…ence not_indepFun_rankTwoCoupling: the array is NOT independent of its new latent layer. The edge and colour-parity events coincide a.e., each has probability 1/2, so their joint is 1/2 against a product of marginals 1/4. A constant edge would also be 'a function of the colours' but could not achieve this, which is why the witness is numerical rather than functional. All null-set reasoning is confined to one a.e. event-equivalence lemma (ae_edgeEvent_iff_parityEvent); the final theorem is pure arithmetic. Wired into Graphon.lean with a doc bullet; audit 409 -> 415.
…rding (#196) SamplerSources' contents list now mentions uniform01_Iic — the declaration moved into the authoritative module but its header did not record it. The claim that the bipartite and i.i.d. regressions 'live in a separate shared module' is replaced by 'Adversarial examples are kept in route-independent regression modules, outside this interface'. The i.i.d. module does not exist yet, and the plan is separate modules rather than a shared one, so the previous wording was both premature and wrong about the layout. Applied consistently in Graphon.lean and the contract module's own header.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The bipartite regression for the successor contract (#196; #107 remains open) — a hand-built rank
1 → 2successor witness overdigraphSig, landed before either route is attempted so the acceptance battery cannot be shaped by an implementation.Each vertex carries an i.i.d. colour on its own fresh singleton coordinate, and the edge is the parity
colour u ⊕ colour v. The diagonal is constantlyfalsefor free, sinceb ⊕ b = false.Three independent kill switches
1. Genuinely separate descriptions.
bipartiteLawis defined from the fresh singleton layer alone, and the rank-one coupling is the independent productbipartiteLaw × rankLatentSource 1. Neither is read off the rank-two object, sorankTwoCoupling_truncation : rankTwoCoupling.map (Prod.map id (rankLatentProjection (Nat.le_succ 1))) = rankOneCouplingcompares two separately described couplings and genuinely consumes the source factorization —
U_∅splits off from the singleton layer, the array reads only the latter, the truncation only the former. DefiningCas a projection ofDwould have made this hold by unfolding and certified nothing.2. Numerical nonindependence.
not_indepFun_rankTwoCouplingshows the array is not independent of its new latent layer: the edge event and the matching colour-parity event coincide a.e. and each has probability1/2, so their joint is1/2against a product of marginals1/4. "The edge is a function of the colours" would also hold for a constant edge; the arithmetic is what excludes that.3. Both directed coordinates. The rank-two decoder recovers
X_uvandX_vuas the same parity, so symmetry is exhibited as a property of this law rather than something hidden in the signature.Contents
bipartiteExchangeable— the law, with exchangeability from array equivariance plus source invariance;rankOneRep,rankTwoRep— full representations, all seven fields each;rankTwoCoupling_map_fst/_map_snd/_truncation— the three central identities, proved immediately after the definition and before invariance or screening;blockMap_pair_arr— the organizing deterministic-block lemma, which drives rank-two screening and the XOR identity and nothing else (recovery below rank two ranges over cardinality< 2and keeps its own vacuous/constant-diagonal proof);bipartiteSuccessor : RankSuccessor rankOneRep— the witness, a two-field literal whose truncation proof is exactly the gate identity;ae_edge_xor— the public XOR identity, a coordinate projection of the block lemma.Invariance goes through one exact pointwise joint-action lemma proved before any measure is touched, isolating the orientation conventions in a single place.
Bookkeeping
Graphon/RelBipartiteRegression.lean; import and doc bullet inGraphon.lean.uniform01_Iicrelocated from the graph-specificInfiniteSamplertoSamplerSources, besideuniform01itself — both existing consumers compile unchanged, and the regression avoids a graph-specific dependency.scripts/axiom_audit.leanand the intended-set literal inscripts/check_census_and_axioms.py.lake buildclean (3405 jobs), census + axiom audit pass, zero sorries, no warnings in the new module.Next: the i.i.d.-edge regression at rank
2 → 3, then #197.