feat: rank successor decomposition, unit 1 of the transition (#107)

[cameronfreer]

Unit 1 of the rank transition n → n+1, per the design checkpoint on #107. Law-free: index types, equivalences and projections, no measure. #107 remains open.

The layer is a Bool-cube, not a dependent product

This is the load-bearing choice and the reason unit 1 comes first. The obvious definition of the rank-n layer is Π A : RankSupport S n, ExactSpace A. That would force every downstream conditional law to be a kernel into a dependent product, and Mathlib has no countable dependent product of kernels — no Kernel.pi under that or any name; the only Π-valued kernels are the Ionescu–Tulcea trajectory kernels, whose source is the history Π i : Iic a, X i rather than a fixed common parameter.

Since ExactSpace A = ExactIndex A → Bool, the dependent product is already a Bool-cube:

Π A : RankSupport S n, ExactSpace A  ≃  ((Σ A, ExactIndex A) → Bool)

and that sigma index is {i // (anchor i).card = n}. So RankLayerIndex / RankLayerSpace are defined directly as the Bool-cube, with sigmaExactIndexEquiv recording the bridge to the per-support view and rankLayerMap_sigmaExactIndexEquiv identifying each block with exactMap A — by rfl, since both sides evaluate the same basis event at the same point.

Countability and standard Borelness are then the same instances that already serve LowerFactorSpace. Downstream, no product kernel is needed anywhere: a layer conditional law is an ordinary condDistrib into a standard Borel space, and mutual conditional independence supplies exactly the finite products that finite-cylinder extensionality consumes.

Contents

• RankLayerIndex / RankLayerSpace / rankLayerMap, with measurability;
• RelSignature.RankSupport and the bridge sigmaExactIndexEquiv;
• lowerIndexSuccEquiv — LowerIndex (n+1) ≃ LowerIndex n ⊕ RankLayerIndex n, from card < n+1 ↔ card < n ∨ card = n — and lowerFactorSpaceSuccEquiv, the measurable split LowerFactorSpace (n+1) ≃ᵐ LowerFactorSpace n × RankLayerSpace n. fst_lowerFactorSpaceSuccEquiv and lowerFactorSpaceSuccEquiv_lowerFactorMap are both rfl, so the split agrees with the existing rank nesting on the nose;
• lowerToBoundaryProjection — for A.card = n, the rank-n factor reads the boundary at A, with lowerToBoundaryProjection_lowerFactorMap definitional as hoped;
• rankSupportEquiv / rankLayerIndexEquiv / rankLayerSpaceEquiv — the relabeling actions. Like lowerIndexEquiv and unlike basisIndexEquiv, these are automorphisms of one fixed type (the action transports anchors by an injective image map, so it preserves cardinality exactly), so the action laws are honest equalities of equivalences with no dependent transport.

One square is not definitional

lowerIndexSuccEquiv_rankLayerIndexEquiv — the equivariance of the successor split — is not rfl, and the module header says so rather than leaving it looking like an oversight. The split is a case distinction on card < n versus card = n, hence a dite, and the branch conditions on the two sides agree only after transporting anchor cardinality through the image map. Everything else in the file is rfl.

One promotion

RelSignature.sigmaMap_injective was private in RelRankAlgebra; RelLowerFactor already carries a private near-duplicate of it. Rather than add a third copy, this promotes the more general one (raw permutation family) to public. Rank is defined by anchor cardinality, so every rank-indexed construction needs the image map to be injective in order to see that the action preserves rank.

Gates

• lake build — 0 errors.
• scripts/check_census_and_axioms.py — census and axiom audit OK; the eleven new declarations use only propext, Classical.choice, Quot.sound.
• Audit list updated in both scripts: 246 → 257, measured directly on base and head.
• Zero sorry/admit.

Unit 2 (the rank-layer factorization) is next and is where the mathematical content sits; unit 3 stops for review before implementation, as agreed.

[cameronfreer]

Both items addressed in c179a8d.

1. No injectivity wrapper. You were right that nothing needed promoting. Function.injective_id.sigma_map fun s => (σ s).injective is used throughout instead; the promoted sigmaMap_injective is gone from RelRankAlgebra, and so are both private duplicates — the one in RelRankAlgebra and the near-duplicate in RelLowerFactor. Three copies down to none, and the audit entry is removed.

2. Structural API. All six items added, all law-free, and all definitional:

• rankLayerToExactProjection with measurable_rankLayerToExactProjection, and rankLayerToExactProjection_rankLayerMap : rankLayerToExactProjection hA ∘ rankLayerMap n = exactMap A by rfl;
• exactSpaceEquiv_rankLayerToExactProjection — naturality under rankLayerSpaceEquiv/exactSpaceEquiv;
• boundarySpaceEquiv_lowerToBoundaryProjection — naturality of the boundary projection;
• rankSupportEquiv_one/_mul and rankLayerSpaceEquiv_one/_mul (plus rankLayerSpaceEquiv_apply, needed to make the simp proofs of the latter go through, mirroring lowerFactorSpaceEquiv_apply);
• rankLayerIndexEquiv_sigmaExactIndexEquiv — naturality of the bridge;
• lowerFactorSpaceSuccEquiv_lowerFactorSpaceEquiv — the space-level successor square.

One observation worth recording: the space-level successor square is definitional even though the index-level one is not. The space map is built from lowerIndexSuccEquiv.symm, which is a Sum.elim and computes on the constructors, so the forward dite that forces the index-level case split never appears. Units 2 and 3 will be working at the space level, so they inherit a rfl square rather than the two-branch one.

Two incidental cleanups while in there: rankSupportEquiv moved to the RelSignature namespace, since it never mentions the basis; and card_image_sigmaMap extracted as the shared rank-preservation step rather than repeated inline.

3. Header corrected. "Everything else here is rfl" was literally false, as you say. It now states which square is not definitional and names the coordinate and projection compatibility lemmas that are.

Gates re-run on the new head: lake build 0 errors, census + axiom audit OK, standard axioms only. Audit 257 → 265 — the nine new entries less the removed wrapper. Unit 2 stays separate.