feat: i.i.d.-edge regression for the successor contract (#196) - #205
Merged
Conversation
One uniform per two-point support, with the array keyed by a coordinate's SUPPORT. That makes both required facts definitional: X_uv and X_vu share a support and hence a value, and the diagonal has a one-element support so it falls in the false branch. Blocks at distinct two-point supports are i.i.d., being distinct source coordinates. No equivariant-orientation problem arises, because the directed coordinates are never given independent values. measurable_decideLe promoted from the bipartite regression to SamplerSources: thresholding a measurable real is general infrastructure and now has a genuine second consumer, which is the condition for extracting it. The two regression modules stay independent of each other.
rankTwoCoupling := iidEdgeLaw.prod (rankLatentSource 2) — a product, so independence of the edges from the old latents is literal rather than argued. rankThreeCoupling is built from rankLatentSource 3, retaining the whole latent point and decoding the array from its fresh rank-two layer. rankThreeCoupling_truncation is proved immediately, before either representation is packaged: the fresh edge layer splits off from the old latents, the array reads only the former and the truncation only the latter. It went through on the first attempt, the bipartite version having established the rewrite pattern.
) `condIndepFun_of_prod_right`: on a product space, a function of the first coordinate is conditionally independent of a function of the second given any sub-algebra of the second coordinate's algebra. This is the screening engine for the rank-two representation, where the old latents live in the second factor and the edges are decoded from the first. Two elaboration notes worth keeping: * `CondIndepFun` takes the conditioning algebra *before* the ambient one, so the statement is written in explicit `@` form. * An abstract `{m' : MeasurableSpace (α × β)}` binder enters local instance search and shadows `Prod.instMeasurableSpace`, so the proof opens with `letI mΩ : MeasurableSpace (α × β) := Prod.instMeasurableSpace` and annotates the standalone projections (`Prod.fst : α × β → α`). Kept private here; recorded as a Provisional upstream candidate on #160.
`rankSupportPerm` acts by an arbitrary sortwise permutation, not only a finitely supported one: cardinality is preserved by injectivity alone, and a law's exchangeability is invariance under *all* sortwise permutations. `rankSupportEquiv` is now its finitely supported instance, and the bipartite regression's rank-one `supportPerm` is a wrapper rather than a third hand-written copy. Definitionally unchanged in both cases, so the existing `show`-style proofs are untouched.
Relabeling the vertices reindexes the edge layer: a coordinate's support transports covariantly and injectivity preserves its cardinality, so `arr (e ∘ rankSupportPerm σ 2) = RelStructure.relabel σ (arr e)`. Exchangeability is then invariance of an i.i.d. product under a coordinate permutation, and `iidEdgeExchangeable` packages the law. `mem_rankSupportPerm` is stated **without an image** so that no `DecidableEq` instance appears in its type. Over a concrete carrier the natural instance (`instDecidableEqNat`) is not definitionally the classical one used to form the image, which makes `rankSupportPerm_coe` unusable there; the membership form is instance-agnostic. Stated in the abstract-signature file, where no natural instance exists to compete.
) Two pointwise block lemmas carry everything: a block whose support does not have two elements is constant `false`, and a block at a two-point support reads exactly the edge coordinate keyed by that support. Rank two: invariance is a product of two invariant factors; recovery below rank two is a constant decoder that reads no latent. Rank three: recovery is the substantive staging clause — a two-point block is decoded from the latent coordinate at its own support, which the rank-three array carries because 2 < 3. Screening at a three-point support is vacuous: over a binary signature no coordinate reads three vertices, so the block space is a single point. `RelCoord.card_support_le` is stated over an abstract carrier for the same reason as `mem_rankSupportPerm`: no natural `DecidableEq` competes with the classical instance used to form the support's image.
…ness (#196) Rank-two screening is the clause this regression exists to exercise. At a two-point support the block reads **one** coordinate of the edge source, while the remainder reads the other coordinates plus 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. The bipartite regression could not test this: there the rank-two block was a function of the latents visible at its support, so screening was immediate. The private lemma is accordingly generalized from the two coordinates of a product to abstract σ-algebras: **if m₁ is independent of m₂, conditioning on anything inside m₂ cannot create a dependence.** The generalization is forced, not cosmetic — the ambient measure here is a pushforward of a product along the non-injective thresholding map, and conditional independence does not transport forward along such a map, whereas independence, being a property of a joint law, does. The repository has no forward transport for the conditional statement and this is why none is needed. The supporting split is `Equiv.sumCompl` at the distinguished support followed by `infinitePi_map_comp_equiv` and `infinitePi_map_sumPiEquivProdPi`, then `prodAssoc_prod` to put the single coordinate against everything else. With rank-three invariance from the joint pointwise action, both representations package and `iidEdgeSuccessor` witnesses the rank 2 → 3 step with exact truncation.
…e regression (#196) `iidEdgeLaw_edge_eq_half` pins the edge probability at exactly one half, so no block is almost surely constant and rank-two screening is a genuine conditional- independence statement rather than determinism in disguise — the numerical counterpart of the bipartite regression's 1/2-vs-1/4 check. `ae_edge_eq_decode` states the staging property concretely: under the rank-three coupling the edge at a two-point support is the thresholded latent coordinate keyed by that support. Module wired into `Graphon.lean` with its index entry; audit 415 → 424 in both `scripts/axiom_audit.lean` and the intended-set literal in `scripts/check_census_and_axioms.py` (counted directly). Gates: lake build clean (3407 jobs), census + axiom audit pass, zero sorries.
…cy claims (#196) Three factual corrections, no proof changes. * The claim that conditional independence cannot transport forward along a non-injective pushforward was too strong. For these observables, with conditioning generated by a function, conditional independence is determined by their joint law and non-injectivity is not an obstruction. What is actually true is narrower and about this repository: the current API transports conditional independence only **backward**, so a source-level proof would first require a new forward law-transport theorem, whereas pushing the unconditional independence forward needs no new theorem. Corrected in both the module and the `Graphon.lean` index entry. * Symmetry and the empty diagonal are **by construction**, not definitional: each is still proved from a support computation (`arr_symm`, `arr_diagonal`). What the support keying buys is that neither needs a choice of orientation. * Edge probability `1/2` rules out a *constant* block; it does not by itself rule out measurability from the old latents. That second fact comes from the product independence built into the rank-two coupling, and the index entry now says so. Also drops the unused `hSamb` and replaces the temporally fragile "Neither Mathlib nor TauCeti has it" with the missing intersection identity itself. Gates: lake build clean (3407 jobs), census + axiom audit pass, audit 424.
`support_digraphCoord` and its off-diagonal cardinality corollary
`card_support_digraphCoord` move beside `digraphCoord` in `Graphon.InfiniteDigraph`,
generalized over an arbitrary vertex type. Both regressions were proving the same
geometry independently, so this has two genuine consumers.
The pair is stated with `[DecidableEq V]` and proved by **membership** rather than
by unfolding an image, so the instance forming `{⟨(), a⟩, ⟨(), b⟩}` is the caller's
and not the classical one used to build `RelCoord.support`; the two are not
definitionally equal over a concrete carrier, and an image-shaped statement would
be unusable at exactly the sites that need it. The bipartite regression keeps a
one-line adapter onto its own `pairSupport`, so the geometry is shared while the
local naming is not disturbed.
`InfiniteDigraph` gains `Graphon.RelEqualityPattern` — a sibling under
`RelationalStructure`, so no cycle — which is where `RelCoord.support` lives.
Also makes `measurable_colour` a direct consumer of `measurable_decideLe` instead
of re-deriving thresholding measurability by hand.
Audit 424 → 426 in both files. Gates: lake build clean (3407 jobs), census +
axiom audit pass, zero sorries.
`InfiniteDigraph` is a D1 module, and importing the equality-pattern layer there would push an upward dependency onto every D1 consumer for the sake of two lemmas none of them use. The absence of an import cycle does not make that desirable. `support_digraphCoord` and `card_support_digraphCoord` therefore move unchanged into `Graphon.DigraphCoordSupport`, which imports both `Graphon.InfiniteDigraph` and `Graphon.RelEqualityPattern` — the same separation `SimpleGraphDigraphBridge` already maintains to keep `SimpleGraph` out of D1. `InfiniteDigraph.lean` is restored byte-for-byte to its state on master. Both regressions import the bridge; `Graphon.lean` gains the module and its index entry. Statements, proofs, and audit entries are unchanged. Gates: lake build clean (3408 jobs), census + axiom audit pass, audit 426, zero sorries.
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 i.i.d.-edge regression for the successor contract (#196; #107 remains open) — a hand-built rank
2 → 3witness overdigraphSigthat tests staging and recovery, 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}andX_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 is still proved from a support computation (arr_symm,arr_diagonal); what the keying buys is that neither needs a choice of orientation.What makes it a regression rather than a construction
Recovery is genuinely staged, and the two ranks exercise opposite sides of
lower_recovers. At rank three a two-point block is decoded from the latent coordinate at its own support — carried by the rank-three array precisely because2 < 3. At rank two the very same blocks are not latent-measurable at all; below rank two every block is constantfalseand the decoder reads no latent. A representation that confused the fresh layer with the old ones would fail one of these two clauses.Rank-two screening is a genuine conditional-independence statement. The block at a two-point support reads one coordinate of the edge source; 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, not from determinism — which is the case the bipartite regression could not reach, since there the rank-two block was a function of the latents visible at its support and
condIndepFun_of_measurable_leftclosed it immediately.iidEdgeLaw_edge_eq_halfpins the edge probability at exactly1/2, which rules out a constant block; that the block is not measurable from the old latents is a separate fact, supplied by the product independence built into the rank-two coupling.Rank-three screening is vacuous, for a stated reason. Over a binary signature no coordinate reads three vertices, so a three-point block space is a single point (
isEmpty_blockIndex_of_card_eq_three). The clause is discharged by constancy, and the file says so rather than leaving a reader to wonder whether something was missed.The private conditional-independence lemma, and why it is stated abstractly
condIndepFun_of_indep_of_le: ifm₁is independent ofm₂, conditioning on anything insidem₂cannot create a dependence. The generalization from "the two coordinates of a product" to abstract σ-algebras is forced by the available API, not cosmetic.The ambient measure here is a pushforward of a product along the thresholding map that builds the structure. The obstruction is not mathematical: for these observables, with conditioning generated by a function, conditional independence is determined by their joint law, and the non-injectivity of the pushforward is not in itself an obstruction. The obstruction is that this repository transports conditional independence only backward — every transport it owns (
condIndepFun_comp_measurePreservingand its relatives) runs from target to source, or along an equivalence as inRelRankOneCoupling. A source-level proof would therefore have to prove a new forward law-transport theorem first. Transporting the unconditional independence needs no new theorem, so the argument establishes that and applies the conditioning lemma on the coupling.The supporting split is
Equiv.sumComplat the distinguished support, theninfinitePi_map_comp_equivandinfinitePi_map_sumPiEquivProdPi, thenprodAssoc_prodto place the single coordinate against everything else.Two elaboration points are recorded in the file because they cost real time:
CondIndepFuntakes the conditioning algebra before the ambient one, so the conclusion is written in explicit@form; and an abstractMeasurableSpace Ωbinder enters local instance search and shadows the ambient instance, which the openingletIrestores without weakening the statement.Shared generalizations extracted
rankSupportPerm— the rank-support action for an arbitrary sortwise permutation, not only a finitely supported one: cardinality is preserved by injectivity alone, and a law's exchangeability is invariance under all sortwise permutations.rankSupportEquivis now its finitely supported instance and the bipartite regression's rank-onesupportPermis a wrapper, replacing a third hand-written copy. Definitionally unchanged in both cases, so existingshow-style proofs are untouched.mem_rankSupportPermandRelCoord.card_support_leare stated over an abstract carrier without an image in the type, because over a concrete carrier the naturalDecidableEqis not definitionally the classical instance used to form the image; the membership and cardinality forms are instance-agnostic where the image forms are not.Bookkeeping
Graphon.RelIidEdgeRegression, wired intoGraphon.leanwith its index entry.scripts/axiom_audit.leanand the intended-set literal inscripts/check_census_and_axioms.py.lake buildclean (3407 jobs), census + axiom audit pass, zero sorries.iidEdgeSuccessor : RankSuccessor rankTwoRepis the witness itself, with exact truncation against an independently defined rank-two coupling.