R4: the Austin base, its action, and the base-extended bundle (#197 unit 2)

[cameronfreer]

Unit 2 of the Austin route (#197; #107 remains open): the Austin base, its action, and the base-extended bundle with its coherent-basis adapter. Route A only — no Kallenberg machinery, and nothing here asserts the two routes' outputs agree.

The base, and the asymmetry between its two components

AustinBaseSpace = PooledRankLatentSpace × ClusterSpace is the equivariant base over which the enriched kernel will be built, packaged over the existing signature — no synthetic relational signature is introduced, and the pooled real latents stay real rather than being encoded as Boolean relation coordinates.

Its two components differ in kind, and conflating them is a mistake worth naming. The latent component carries no rank-n latent, every pooled index having cardinality < n. The cluster component deliberately does carry rank-n blocks, at supports that are not wholly original. The clusters are correlated structural polling data — which is exactly why conditioning on them is informative, and why a base free of rank-n blocks could not do the job.

The action, proved strict before anything is built on it

Equivariance cannot be repaired downstream, so the action is fixed and proved strict first.

• poolLift acts on the original half and fixes the spare half; its preservation of Sum.isRight is what keeps mixed clusters mixed, all-spare ones included.
• mixedClusterLift with _one and _mul; austinBaseRelabel_one and _mul as exact function equalities.
• The orientation is contravariant: Equiv.trans applies its first argument first, so austinBaseRelabel (σ * τ) = austinBaseRelabel τ ∘ austinBaseRelabel σ. This is stated explicitly in the module so it is not re-derived wrongly.
• enrichedPollingMap_naturality — one square for all four components: structure and pooled latents definitionally, clusters by pollingClusters_relabel (itself rfl), original latents by the split corollary restrictOriginalLatents_sumCongr.
• enrichedPollingLaw_map_enrichedAction — exact invariance, from Measure.map_map, that square, and Q.invariant alone. No almost-everywhere step and no component rewriting inside it.

The dependent cluster fibres are handled by Bool-valued pointwise bridges, with the single required cast isolated in one private lemma. Marking MixedClusterIndex reducible would also have worked and was rejected: unlike the compatibility aliases elsewhere in the repository it is a substantive subtype, and exposing its implementation globally to solve a local elaboration problem is too broad.

The bundle

austinEnrichedObject constructs AustinEnrichedObject from Q and the unit-1 witness as the exact pushforward of enrichedPollingLaw along the compression that drops the original-latent coordinate — redundant because on the image of enrichedPollingMap it is restrictOriginalLatents of the pooled array. So map_original recovers C.P from the pooled component alone, through Q.map_restrict_embedding at the original-vertex embedding, and the #195 gate theorem stays a compiled dependency.

mutualCondIndep is the unit-1 witness moved forward by Austin.iCondIndepFun_of_map, not a second proof. That helper — and Austin.iCondIndepFun_congr_cond alongside it — moved from private into a route-local namespace when this unit became their second consumer. That is not ForMathlib promotion: a second consumer inside the same route is not an independent one, which remains the condition for extraction.

The adapter

Stated for an arbitrary coherent basis, so no Fintype S.Srt enters any signature in the module; selecting a basis via nonempty_coherentBasis is what would introduce it. All four commuting laws are exact:

• boundary projection through the extended lower factor — rfl;
• exact-anchor projection through the layer — rfl;
• map_forget_base — forgetting the base returns the corresponding pushforward of M.law. This asserts no independence: the clusters are correlated structural data, and the identity says only that the structural factor law is recovered once the base is discarded;
• map_recombine — recombining lower and layer through lowerFactorSpaceSuccEquiv.symm returns the rank-(n+1) lower-factor law, an equality of pushed measures with the base forgotten and no a.e. weakening. It is a prerequisite for exact truncation, not that statement: it mentions neither C.P nor rankLatentProjection, so it does not pin RankSuccessor.truncation. Exact truncation will come from map_original together with the assembly unit's source-splitting identity.

The rank-m layer deliberately does not carry the base: the layer is where the fresh rank-m information lives, and the base is the lower-rank data it is read against.

Boundaries held

No condDistrib or kernel equalities — those belong to the kernel unit, where every such identity is almost-everywhere under a named law. No fresh rank-n uniforms, randomization, or RankSuccessor. Countable-only throughout.

Bookkeeping

Audit 433 → 442 in both scripts/axiom_audit.lean and the intended-set literal in scripts/check_census_and_axioms.py. Gates: lake build clean (3410 jobs), census + axiom audit pass, zero sorries, no warnings.