Increment 3 step 1 (#107): boundary/exact splitting and the factor laws

[cameronfreer]

Increment 3, step 1: the boundary/exact splitting and the factor laws. #107 remains open.

The decomposition

The factor at A splits by anchor:

• BoundaryIndex A — indices whose anchor is a proper subset of A;
• ExactIndex A — the exact-anchor layer: indices whose anchor is exactly A;
• factorSpaceProdEquiv : FactorSpace A ≃ᵐ BoundarySpace A × ExactSpace A.

Both index types are countable and both spaces standard Borel.

This partitions coordinates by anchor, not information. Anchors are not minimal: a Boolean expression can carry anchor A while naming an event already measurable over a proper subset, since the seeds at A live in fixingAlgebra A ⊇ fixingAlgebra C for every C ⊆ A. So the exact-anchor layer is not "the new information at A", and the splitting alone rules out no redundancy between layers.

This is the shape the recursion needs — one kernel per finite A, conditioned on the whole proper-subset boundary, recursing by |A|. The module docstring records why, rather than the two obvious alternatives:

• Kernels for every pair C ⊆ A are redundant, and would force compatibility conditions between different versions of conditional distributions, each only defined a.e.
• A linear chain over an enumeration imposes an arbitrary ordering, and lets the value at A depend on sets incomparable to A — breaking the subset-locality of the AHK formula.

Sampling only ExactSpace A, rather than resampling all of FactorSpace A, means the recursion never overwrites coordinate slots already generated at proper subsets — that much is structural, from the coordinate partition. Consistency with lower-anchor events that an exact-anchor coordinate happens to duplicate semantically is a separate matter: an almost-sure/support property of stepKernel, which conditions on the boundary, not something the partition delivers on its own.

The laws

factorLaw, boundaryLaw, exactLaw as pushforwards of M.law, each a probability measure, with boundaryLaw_eq_map and exactLaw_eq_map identifying the latter two as the marginals of the factor law through the product decomposition. Then:

• factorLaw_map_factorProjection — projection consistency, immediate because factorProjection_factorMap is rfl;
• factorLaw_map_factorSpaceEquiv — relabeling invariance. This is the first place in this layer where exchangeability of the law is used; everything before it was law-free.

Note

In the product equivalence the branch condition depends on the index, not the point, so the proofs go through dif_pos/dif_neg plus an explicit function equality. Rewriting with the hypothesis anchor i = A itself also rewrites inside the subtype and breaks the match — recorded in the source.

Not in this PR

stepKernel, and the mutual-independence theorem for same-rank exact layers given the lower-rank boundary. Pairwise conditional independence is not automatically mutual, so that will be an explicit theorem in step 2. Randomization via #140 and the recursion on |A| are step 3.

Gates

Full build 3358 jobs green; zero sorries; audit 187 to 191, new declarations [propext, Classical.choice, Quot.sound]-clean; documentation drift checks pass.