Repository navigation
R4: successor contracts (interface-only) + shared regressions for both routes (#107) #196
Description
Child of #107 (R4 converse). Depends on the route-neutral gate #195.
Compile both successor constructions as interface-only structures and theorem statements, before either hard core is attempted, and run the shared regression suite against both.
The two theorems are identically typed
nonempty_rankRepresentation_succ_via_kallenberg :
M.RankRepresentation n → Nonempty (M.RankRepresentation (n + 1))
nonempty_rankRepresentation_succ_via_austin :
M.RankRepresentation n → Nonempty (M.RankRepresentation (n + 1))Same type, two proofs. They will not produce canonically equal representations, and no equality between their outputs should be stated or assumed; the point is two independent proofs of one existence theorem, not a canonical construction.
The public induction theorem uses whichever route lands first. The other remains an independently audited proof path — which is the entire value of building the second.
Regressions, run against both
- bipartite (the Austin §3.6 configuration that refuted the shell theorem on 2026-08-03);
- i.i.d.;
- rank-zero / nullary;
- mixed-pool.
Running these against interface-only statements is what makes the later pricing honest: a regression that cannot even be stated against one route's interface is a design defect found cheaply.
Deliverable
Statements and structures only, with no proof of either successor theorem. The hard cores are #197 and #198.
Activity
refactor: real rank-zero regression; drop redundant restatement (#196)
cameronfreer commentedon Aug 16, 2026
Contract landed on
r4-successor-contract(interface only, no construction).RankSuccessor Ccarries the next representation together with the load-bearing observable:Exact, law-level, not a.e. and not up to isomorphism. Without it a theorem returning merely
Nonempty (RankRepresentation (n + 1))could ignoreCentirely and would not characterize a successor construction at all — the same underdetermination that sank the shell attempt.No independence field beyond
RankRepresentation's own, and no asserted equality between the two routes' outputs.AustinSuccessorandKallenbergSuccessorare the same proposition by construction (rfl), so whichever lands first discharges the induction step while the other stands as an independent proof of the same statement.Regression status.
truncation_zeroproves the truncation equation is automatic at rank zero, since the rank-zero latent cube is a single point and both sides are then determined by their structure marginals.2 → 3, where truncation preserves independence from the old latents while the fresh edge latent makes the edge block recoverable.RankSuccessorexposes no pooled carrier, so nothing at this interface could observe whether a proof actually used boundary-crossing permutations; such a check would be vacuous. That property is already formalized by the pooled gate'sPooledRankExtension.map_restrict_embedding, which holds for every sortwise embedding, and each route's intermediate construction is required to consume it.#196 remains open.
cameronfreer commentedon Aug 16, 2026
Acceptance criteria for the two remaining shared regressions, pinned. Both live in a route-independent regression module;
RelRankSuccessorContract.leanstays interface-only.Bipartite, rank 1 → 2. Required witnesses:
RankSuccessortruncation;X_uv = z_u ⊕ z_v;I.i.d. edges, rank 2 → 3. Required witnesses:
X_uvfrom the fresh support-{u,v}latent.The second simultaneously tests staging and recovery.
Neither needs the strongest "no colour is graph-measurable" theorem. A concrete nonindependence identity for bipartite, and nondegeneracy plus fresh-coordinate decoding for i.i.d. edges, are sufficient acceptance tests.
Merge pull request #202 from cameronfreer/r4-successor-contract
wip(#196): rank-two coupling and the three central identities
wip(#196): recovery below rank two, from the pieces already established
wip(#196): the two-point deterministic-block lemma
wip(#196): rank-two screening via the deterministic-block lemma
feat(#196): the bipartite successor witness
feat(#196): the public XOR identity, projected from the block lemma
refactor: relocate uniform01_Iic to SamplerSources (#196)
feat(#196): the XOR event has mass one half
feat(#196): complete the bipartite regression — numerical nonindepend…
docs: list uniform01_Iic in its module header; timeless regression wo…
Merge pull request #203 from cameronfreer/r4-bipartite-regression
cameronfreer commentedon Aug 18, 2026
Bipartite regression merged (#203,
bf468d1); master audit 415.Regression status for the shared battery:
truncation_zero: the truncation equation is automatic at rank zero);1/2against1/4, which a constant edge could not achieve), and both directed coordinates decoding to the same parity;Cbuilt independently with edges nondegenerate and independent of the old latents, a rank-threeDwhose fresh pair latents decode the edges, exact truncation and the decoding identity. It tests staging and recovery together, where the bipartite one tested independence and symmetry;PooledRankExtension.map_restrict_embedding, and each route's intermediate construction must contain a compiled consumer of it (recorded on R4 successor route A (Austin): polling → enriched object → kernel → noise outsourcing (#107) #197 and R4 successor route B (Kallenberg): direct correlated subset latents — independent check (#107) #198).#196 remains open until the i.i.d.-edge regression lands.
wip(#196): both i.i.d.-edge couplings and the truncation gate
feat: cond-indep-from-product lemma for the i.i.d.-edge regression (#196
refactor: generic sortwise-permutation action on rank supports (#196)
feat: equivariance and exchangeability of the i.i.d.-edge law (#196)
feat: rank-two invariance/recovery and the full rank-three clauses (#196
feat: rank-two screening, both representations, and the successor wit…
feat: nondegeneracy, decoding identity, and wiring for the i.i.d.-edg…
docs: correct the forward-transport, definitionality, and nondegenera…
refactor: shared digraph-coordinate support geometry (#196)
refactor: move the digraph support geometry to a bridge module (#196)
Merge pull request #205 from cameronfreer/r4-iid-edge-regression
cameronfreer commentedon Aug 21, 2026
Closing: the shared regression battery for the successor contract is complete and on master.
The battery
truncation_zero: the truncation equation is automatic at rank zero, so the base case imposes nothing beyond the representation axioms.1 → 2witness testing independence and symmetry, with a numerical1/2-vs-1/4nonindependence check.2 → 3witness testing staging and recovery. The two ranks exercise opposite sides oflower_recovers: at rank three a two-point block is decoded from the latent coordinate at its own support, carried by the array because2 < 3, while at rank two those same blocks are not latent-measurable at all. Rank-two screening is a genuine conditional-independence statement — the block reads one coordinate of the edge source and the remainder reads the others plus the whole latent array — and rank-three screening is vacuous for a stated reason: over a binary signature no coordinate reads three vertices.RankSuccessorexposes no pooled carrier, so no check at that interface could observe whether a proof used boundary-crossing permutations. That property is already formalized byPooledRankExtension.map_restrict_embedding, and each route owes a compiled consumer of it instead (recorded on R4 successor route A (Austin): polling → enriched object → kernel → noise outsourcing (#107) #197 and R4 successor route B (Kallenberg): direct correlated subset latents — independent check (#107) #198).What #205 changed about the plan. The pinned route for rank-two screening — prove it at product-source level and transport — was not viable.
restObservation 2 Areads both coordinates, so it is not of the formg ∘ Prod.sndand the product-shaped lemma never applies; and the ambient measure is a pushforward along the thresholding map, which the current API can only transport conditional independence backward through. The obstruction is an API gap, not a mathematical one: for these observables, with conditioning generated by a function, conditional independence is determined by their joint law. The regression instead proves the unconditional independence, which needs no new transport theorem, and applies an abstract conditioning lemma on the coupling.Provisional, awaiting a second consumer (tracked for #160):
condIndepFun_of_indep_of_le— and when it is promoted, the σ-algebra-level theorem should be extracted intoForMathlib/CondIndepSup.leanwith the function version derived from it, rather than promoting the current function-heavy statement;indepFun_of_map; and the threshold-mass computation as a possibleSamplerSourcesgeneralization.Master: build 3408 jobs, audit 426, zero sorries. #107 remains open; #197 and #198 are the next units.