feat: the pooled rank extension and cheap constructor — gate 1a stage 2 (#195)

[cameronfreer]

Stage 2 of the pooled-latent extension gate (#195; #107 remains open): the three-field structure and the cheap constructor. Stage-2 boundary respected exactly — mixed-window recovery is left as a named acceptance theorem rather than a field, and screening and route-specific claims stay out.

PooledRankExtension

structure PooledRankExtension (C : M.RankRepresentation n) where
  law : ProbabilityMeasure (RelStructure S (PoolVertex S) × PooledRankLatentSpace S n)
  map_restrictOriginal :
    law.map (Prod.map (restrictOriginal S) (restrictOriginalLatents S n)) = C.P
  invariant : ∀ ρ : ∀ s, Equiv.Perm (PoolVertex S s),
    law.map (Prod.map (RelStructure.relabel ρ) (pooledRankLatentRelabel ρ n)) = law

Three fields, the full mixed action, and no independence field.

The cheap constructor

RankRepresentation.pooledExtension — both laws are map_prodMap_restrict_self (#194) in disguise. Writing pv for poolVertexEquiv and ov for originalVertex, the transport is comap pv on structures and restriction along pv on latents. Then:

• restrictOriginal ∘ transport = comap (pv ∘ ov), and pv ∘ ov is a self-injection of the original carrier — that is map_restrictOriginal;
• relabel ρ ∘ transport = transport ∘ relabel κ for the conjugate κ = pv ∘ ρ ∘ pv⁻¹, a permutation of the original carrier — so invariant, for every mixed ρ, is the same theorem applied to κ, a permutation being in particular an injection.

This is what "full mixed pooled invariance costs no additional mathematics once the self-injection theorem exists" comes to in code: the constructor is two applications of one theorem plus composition and conjugation bookkeeping.

Generic lemmas added, per review

Proved carrier-generically so that instantiating never manipulates Finset.image under a derived DecidableEq:

• latentRestrictOver_latentRelabelOver_conj — the conjugation square for a carrier equivalence, the latent mirror of RelStructure.congrCarrier_relabel, making the two commuting squares visibly parallel;
• latentRestrictOver_toEmbedding — restriction along a permutation-as-embedding is that permutation's action;
• latentRestrictOver_comp / latentIndexEmbed_comp — functoriality of restriction.

Plus the two bridges pinned in review: rankLatentRelabel_eq_latentRelabelOver and rankLatentReindex_eq_latentRestrictOver. Both are genuine equalities rather than rfl, since the rank-indexed and generic constructions choose different Decidable instances under open scoped Classical.

One elaboration change

RankLatentIndex is now marked @[reducible]. It is a compatibility alias for LatentIndexOver S (Vinfinite S), and rw must see through it to match RankLatentSpace S n against LatentSpaceOver S (Vinfinite S) n in the constructor's rewrites. The full build is clean with the attribute, with no other change.

Bookkeeping

• New module Graphon/RelPooledExtension.lean; import and doc bullet in Graphon.lean.
• Audit 379 → 384 in both scripts/axiom_audit.lean and the intended-set literal in scripts/check_census_and_axioms.py; pooledExtension verified #print axioms-clean.
• Gates: lake build clean (3401 jobs), census + axiom audit pass, zero sorries.

Stage 3 — current-rank recovery and screening on mixed pooled supports, plus the joint mixed-window acceptance theorem — is the next unit, after which the gate stops for the route decision.