Increment 2 (#107): the factor spaces are standard Borel - #152
Merged
Conversation
`CoherentBasis.FactorSpace A` names the Boolean cube over `BasisIndex A`, with a `StandardBorelSpace` instance — available because the index is countable, and the reason for indexing by `BasisIndex A` rather than coding every factor into `ℕ → Bool`: the varying index keeps the inclusions literal without giving up measurable structure. This is the hypothesis the conditional-kernel step of increment 3 will need. Also `measurable_factorMap'` (ambient measurability, from the `fixingAlgebra A` version by `fixingAlgebra_le`), `measurable_factorProjection` (the projections are coordinate restrictions), and a `@[simp]` reading of a factor coordinate as event membership. Scope note: increment 2 is small because most of what "simultaneous factor maps with literal inclusion coherence and finitary relabeling equivariance" asks for already landed — the inclusion coherence is `factorProjection_factorMap` and `factorProjection_comp`, both `rfl` since #149, and the equivariance is `factorMap_basisIndexEquiv` with its two definitional compatibilities from #151. What remained was the measurable-structure packaging, which is what this commit adds. I have not invented a bundled restatement of facts that already exist individually. Audit 184 → 186. Full build 3357 jobs green; census, axiom audit, and documentation drift checks pass.
…valences `CoherentBasis.factorSpaceEquiv σ A : FactorSpace (A.image σ) ≃ᵐ FactorSpace A`, the forward map being precomposition with `basisIndexEquiv σ A`. Both directions are coordinate reindexings, hence measurable. This is the single entry point increment 3 needs: transporting a kernel across a relabeling requires the measurable equivalence, not just the underlying index bijection. `factorMap_comp_relabel` is restated through it — same content as the merged version, but the anonymous `fun f => f ∘ basisIndexEquiv σ A` is replaced by the named equivalence, so the commuting square reads as one. The name is unchanged, so the audit entry still applies. `FactorSpace` moved above the derived factors and now appears in the `factorMap` and `factorProjection` signatures. Being an abbreviation this is proof-neutral, but it makes the public API display the packaging rather than the raw `BasisIndex A → Bool`. No `factorLaw` or projection-consistency statement here — those first become mathematically necessary in increment 3, and belong there. Audit 186 → 187. Full build 3357 jobs green; census, axiom audit, and documentation drift checks pass.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Second structural increment. #107 remains open.
CoherentBasis.FactorSpace Anames the Boolean cube overBasisIndex A, with aStandardBorelSpaceinstance. That instance is available because the index is countable, and it is the concrete reason for indexing byBasisIndex Arather than coding every factor intoℕ → Bool: the varying index keeps the inclusions literal without giving up measurable structure. It is the hypothesis the conditional-kernel step of increment 3 needs.Also:
measurable_factorMap'— ambient measurability, from thefixingAlgebra Aversion viafixingAlgebra_le;measurable_factorProjection— the projections are coordinate restrictions;@[simp]lemma reading a factor coordinate as event membership.Scope note
This increment is small, and deliberately so. Most of what "simultaneous factor maps with literal inclusion coherence and finitary relabeling equivariance" asks for had already landed:
C ⊆ AbasisIndexEmbedding(#149)factorProjection_factorMap(#149)rflfactorProjection_comp(#149)rflfactorMap_basisIndexEquiv(#151)basisIndexEmbedding_basisIndexEquiv,factorProjection_basisIndexEquiv(#151)rflexists_comap_factorMap_ae_eq(#149)What was genuinely missing was the measurable-structure packaging, which is what this adds. I have not invented a bundled restatement of facts that already exist individually — if you would prefer one anyway, as a single named entry point for increment 3 to consume, say so and I will add it.
Gates
Full build 3357 jobs green; zero sorries; audit 184 to 186, new declarations
[propext, Classical.choice, Quot.sound]-clean; documentation drift checks pass.Next
Increment 3: conditional kernels on these coherent factors, then the
uniform01randomization adapter from #140.