SO-1 onramp: where the Fubini–Study typicality measure comes from

Category: 3-Local (where the Fubini–Study typicality measure comes from).

This file isolates the honest content of the CSD sector posit SO-1 (SectorData.(π, G), AXIOMS.md §3.3) at the level of the typicality measure: which measure is the canonical sampling law on the sector Σ = ℂℙ^{N-1}, and by what. SO-1 — deriving the sector (Σ, π, μL) from CSD's primitive deterministic ontology — is the central open CSD goal, not a footnote; this file pins exactly what remains. (SO-1 is distinct from Paper C Axiom A5, which is the quantum-effective / projectability condition on Hamiltonians, not the sector's origin.)

IMPORTANT — what forces typicality (read first)

Typicality is forced by the LAW OF LARGE NUMBERS (LF1, LF1_main_theorem_ae / freq_tendsto_of_iid; papers A & B): over repeated i.i.d. preparations, empirical frequencies converge almost surely to the volume weights of the sampling measure. That is the entire typicality-forcing mechanism — no time-average, no Birkhoff / single-flow-ergodicity hypothesis. The results in THIS file are NOT the typicality-forcing mechanism; they concern a different question — which measure is the canonical sampling law (A), and a negative about the stat-mech single-flow ergodicity route which CSD does not use (B/B′).

The two honest results

(A) The FS typicality MEASURE is singled out by the sector symmetry G = U(N) (a measure-characterisation, NOT the typicality-forcing). fubiniStudy_forced_by_symmetry restates the corpus's axiom-free uniqueness theorem fubiniStudyMeasure_unique (Phase G4, Mathlib/LinearAlgebra/Projectivization/FubiniStudyUnique.lean): any U(N)-invariant probability measure on the sector is the Fubini–Study measure. So FS is the symmetry-canonical sampling measure — the Born = FS-volume measure (the input to the Duistermaat–Heckman cluster fs_born_volume_ratio_N / born_frequency_convergence_N) is singled out by the sector symmetry, the (π, G) sector datum (SO-1), rather than posited as an arbitrary independent law. The LLN then forces frequencies to its volume ratios. This is about the measure CHOICE, via the symmetry group, NOT via any single flow and NOT the convergence mechanism.

(B) A single ontic flow does NOT force FS (the obstruction). obsFlow_not_uniquely_ergodic exhibits, for obsFlow (the diagonal-phase Hamiltonian flow t ↦ exp(i t Â) of LF4/ObservableFlow.lean), two distinct obsFlow-invariant probability measures: the Fubini–Study measure and the Dirac measure δ_{[eⱼ]} at a computational-basis eigenstate ray. Because obsFlow is a diagonal phase flow, every basis ray [eⱼ] is an eigenvector and is a fixed point (obsFlow_fixes_eigenstate), so δ_{[eⱼ]} is invariant (dirac_eigenstate_obsFlow_invariant); and δ_{[eⱼ]} ≠ μFS because FS is U(N)-invariant while δ_{[eⱼ]} is moved by a unitary swapping [eⱼ] ↔ [eₖ]. Hence obsFlow is not uniquely ergodic: a single deterministic flow cannot single out FS. This is why the concrete instances cpSectorDataFlow / kSectorDataFlow (D1c-1/2), whose Φ is one such flow, do not discharge SO-1.

(B′) The obstruction is GENERIC, not accidental: a CONSERVED QUANTITY. obsFlow_continuum_invariant strengthens (B) from "≥ 2" to a continuum (Set.InjOn on [0,1]) of pairwise-distinct obsFlow-invariant probability measures. The structural reason is a constant of motion: the Born coordinates momentMap · i are conserved along obsFlow (momentMap_obsFlow, reused from LF4/ObservableFlow.lean — the diagonal phase e^{itλᵢ} leaves |ψᵢ|² unchanged). The genuine content is the conserved-quantity reweighting principle map_withDensity_of_conserved: if h is obsFlow-invariant (h ∘ obsFlow = h) and μ is obsFlow-invariant, then μ.withDensity (g ∘ h) is again obsFlow-invariant — instantiated at h = momentMap · i by withDensity_momentMap_obsFlow_invariant. So invariant measures are abundant precisely because obsFlow carries a non-trivial conserved quantity; the obstruction to unique ergodicity is structural. (The explicit continuum witness is the convex-combination family s ↦ s·μFS + (1−s)·δ_{[e₀]}, s ∈ [0,1], a clean genuine continuum; the conserved Born coordinates are the why.) This still does not force FS and does not close SO-1 — it sharpens the obstruction.

Honest scope (the whole point — claim NOTHING more)

This tranche does not close SO-1, and does not force typicality (the LLN does that, LF1 / papers A & B — see the note above). It (i) shows the FS typicality measure is singled out by the sector symmetry G = U(N) (a measure-characterisation, reusing the uniqueness theorem — the LLN then forces frequencies to it), (ii) proves no single ontic flow singles out FS via its own dynamics (the obstruction — a negative about the single-flow ergodicity / Birkhoff route, which CSD does NOT use; it reinforces that the LLN/i.i.d. route is the operative one), and (iii) thereby pins the residual SO-1 primitive to G itself: the symmetry group U(N) is the datum the canonical measure follows from, and G-from-dynamics — deriving the U(N)-symmetry of the ontic flow from CSD's deterministic substrate — is exactly D1, the deepest open CSD content (Φ = id in every concrete SectorData, or a single non-ergodic phase flow in D1c). We claim nothing about deriving G, and nothing about typicality-forcing beyond the LLN.

so1_onramp conjoins (A) and (B). Foundational-triple-only (no busch_effect_gleason); invariant_measure_uniqueness_cpn / fubiniStudyMeasure_unique are axiom-free.

Computational-basis eigenstate rays

theorem CSD.LF4.cpBasisVec_ne_zero {N : ℕ} (j : Fin N) : EuclideanSpace.single j 1 ≠ 0

The computational-basis vector eⱼ = single j 1 is nonzero.

noncomputable def CSD.LF4.cpBasisRay {N : ℕ} (j : Fin N) : CPN N

The computational-basis eigenstate ray [eⱼ] ∈ ℂℙ^{N-1}.

Equations

• CSD.LF4.cpBasisRay j = Projectivization.mk ℂ (EuclideanSpace.single j 1) ⋯

theorem CSD.LF4.cpBasisRay_ne {N : ℕ} (j k : Fin N) (hjk : j ≠ k) : cpBasisRay j ≠ cpBasisRay k

Distinct indices give distinct basis rays ([eⱼ] ≠ [eₖ] for j ≠ k): if they were equal, some scalar a would satisfy a • eₖ = eⱼ, impossible at coordinate j (0 = a·0 ≠ 1).

(B) — the eigenstate ray is a fixed point of obsFlow

theorem CSD.LF4.obsFlow_fixes_eigenstate {N : ℕ} [NeZero N] (lam : Fin N → ℝ) (t : ℝ) (j : Fin N) : obsFlow lam t (cpBasisRay j) = cpBasisRay j

The diagonal-phase flow fixes every computational-basis ray. obsFlow λ t [eⱼ] = [eⱼ]: the diagonal obsUnitary λ t scales eⱼ by the unit phase obsPhase λ t j, which is the same projective ray. (This is exactly why the Φ ≠ id witness obsFlow_ne_id must use a superposition ray, never a basis ray.)

theorem CSD.LF4.dirac_eigenstate_obsFlow_invariant {N : ℕ} [NeZero N] (lam : Fin N → ℝ) (t : ℝ) (j : Fin N) : MeasureTheory.Measure.map (obsFlow lam t) (MeasureTheory.Measure.dirac (cpBasisRay j)) = MeasureTheory.Measure.dirac (cpBasisRay j)

The Dirac measure at an eigenstate ray is obsFlow-invariant. Immediate from Measure.map_dirac and the fixed-point obsFlow_fixes_eigenstate.

Dirac injectivity on the (Hausdorff Borel) sector

theorem CSD.LF4.dirac_ne_of_ne {N : ℕ} {p q : CPN N} (h : p ≠ q) : MeasureTheory.Measure.dirac p ≠ MeasureTheory.Measure.dirac q

Distinct points give distinct Dirac measures on ℂℙ^{N-1} (singletons are measurable: Projectivization.instMeasurableSingletonClass).

(A) — the FS typicality MEASURE is singled out by the sector symmetry G = U(N)

theorem CSD.LF4.fubiniStudy_forced_by_symmetry {N : ℕ} [NeZero N] (p₀ : CPN N) (μ : MeasureTheory.Measure (CPN N)) [MeasureTheory.IsProbabilityMeasure μ] (hμ_inv : ∀ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), MeasureTheory.MeasurePreserving (fun (p : CPN N) => U • p) μ μ) : μ = Matrix.UnitaryGroup.fubiniStudyMeasure p₀

(A) The FS typicality measure is singled out by the sector symmetry (a measure-characterisation, NOT the typicality-forcing — typicality is forced by the LLN, LF1 / papers A & B; see the file header). Any U(N)-invariant probability measure on the sector Σ = ℂℙ^{N-1} is the Fubini–Study measure. A restatement of the axiom-free fubiniStudyMeasure_unique (Phase G4): FS is the symmetry-canonical sampling measure — the Born = FS-volume measure consumed downstream is singled out by the (π, G) sector datum (SO-1) rather than posited as an arbitrary law; the LLN then forces frequencies to its volume ratios. The characterisation is via the symmetry group, not via any single flow (contrast (B) below).

(B) — a single ontic flow does not force FS

theorem CSD.LF4.obsFlow_not_uniquely_ergodic {N : ℕ} [NeZero N] (hN : 1 < N) (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : ∃ (μ : MeasureTheory.Measure (CPN N)) (ν : MeasureTheory.Measure (CPN N)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.IsProbabilityMeasure ν ∧ MeasureTheory.Measure.map (obsFlow lam t) μ = μ ∧ MeasureTheory.Measure.map (obsFlow lam t) ν = ν ∧ μ ≠ ν

(B) The honest negative. obsFlow is not uniquely ergodic: it admits at least two distinct invariant probability measures — the Fubini–Study measure μFS (invariant by obsFlow_measurePreserving) and the Dirac measure δ_{[e₀]} at a computational-basis eigenstate ray (invariant by dirac_eigenstate_obsFlow_invariant, since the diagonal phase flow fixes basis rays). They differ: FS is U(N)-invariant while δ_{[e₀]} is moved to δ_{[e₁]} by a unitary swapping the two rays (transitivity of the U(N)-action), and distinct rays give distinct Dirac measures.

So no single deterministic ontic flow forces FS — only the full sector symmetry G = U(N) does (result (A)). This is the obstruction behind the naive "single ergodic flow whose unique invariant measure is μFS" picture, and the reason cpSectorDataFlow / kSectorDataFlow (D1c) do not discharge SO-1.

(B′) — the conserved quantity and the continuum of invariant measures

theorem CSD.LF4.map_withDensity_of_conserved {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {T : α → α} (hT : MeasureTheory.MeasurePreserving T μ μ) {d : α → ENNReal} (hd : Measurable d) (hcons : ∀ (x : α), d (T x) = d x) : MeasureTheory.Measure.map T (μ.withDensity d) = μ.withDensity d

Conserved-quantity reweighting principle (the genuine structural content). If a measure-preserving map T admits a conserved measurable density d (d ∘ T = d), then reweighting an invariant measure μ by d is again T-invariant: map T (μ.withDensity d) = μ.withDensity d. The change of variables uses d ∘ T = d together with map T μ = μ (MeasurePreserving.lintegral_comp). General Mathlib-style lemma (no CSD content); kept local.

theorem CSD.LF4.withDensity_momentMap_obsFlow_invariant {N : ℕ} [NeZero N] (lam : Fin N → ℝ) (t : ℝ) (p₀ : CPN N) (i : Fin N) (g : ℝ → ENNReal) (hg : Measurable g) : MeasureTheory.Measure.map (obsFlow lam t) ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀).withDensity fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => g (momentMap p i)) = (Matrix.UnitaryGroup.fubiniStudyMeasure p₀).withDensity fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => g (momentMap p i)

The Born coordinate is a conserved reweighting of every obsFlow-invariant measure. Instantiating map_withDensity_of_conserved at the conserved Born coordinate momentMap · i (momentMap_obsFlow): for any measurable density profile g, the reweighted Fubini–Study measure μFS.withDensity (g ∘ momentMap · i) is obsFlow-invariant. This is the genuine conserved-quantity mechanism behind the abundance of invariant measures: the Born coordinates being constants of motion lets one reweight the typicality measure freely without breaking invariance. (It does not by itself produce a continuum of probability measures — that needs normalisation, i.e. the Duistermaat–Heckman pushforward law of momentMap; the explicit probability continuum below uses the convex-combination route instead. The conserved coordinate is the structural reason.)

theorem CSD.LF4.obsFlow_continuum_invariant {N : ℕ} [NeZero N] (hN : 1 < N) (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : ∃ (f : ℝ → MeasureTheory.Measure (CPN N)), (∀ s ∈ Set.Icc 0 1, MeasureTheory.IsProbabilityMeasure (f s) ∧ MeasureTheory.Measure.map (obsFlow lam t) (f s) = f s) ∧ Set.InjOn f (Set.Icc 0 1)

(B′) The obstruction is generic: a CONTINUUM of obsFlow-invariant probability measures. Strengthens obsFlow_not_uniquely_ergodic (≥ 2) to an uncountable, pairwise-distinct family (Set.InjOn on [0,1]). The witness is the convex-combination family f s = s · μFS + (1−s) · δ_{[e₀]} of the two invariant probability measures of (B): each is a probability measure (masses sum to one), each is obsFlow-invariant (map is ℝ≥0∞-linear and fixes both summands), and they are pairwise distinct — evaluating on {[e₀]}ᶜ gives f s ({[e₀]}ᶜ) = ofReal s · μFS({[e₀]}ᶜ) with μFS({[e₀]}ᶜ) ∈ (0, ∞) (positivity from μFS({[e₀]}) < 1, which follows from U(N)-invariance: μFS{[e₀]} = μFS{[e₁]} on disjoint singletons, so 2·μFS{[e₀]} ≤ 1), hence s ↦ f s ({[e₀]}ᶜ) is injective.

The structural reason for this abundance is the conserved Born coordinate (momentMap_obsFlow, map_withDensity_of_conserved, withDensity_momentMap_obsFlow_invariant): a deterministic flow with a non-trivial constant of motion cannot be uniquely ergodic. Honest scope: this does not force FS and does not close SO-1, and typicality is forced not by any flow but by the LLN (LF1 / papers A & B). The FS measure is singled out by the full sector symmetry G = U(N) (result (A), fubiniStudy_forced_by_symmetry); this result is a negative about the single-flow ergodicity route (which CSD does not use). The residue is G-from-D1.

(B′′) — obsFlow is not even μFS-ERGODIC (the sharper, FS-specific obstruction)

obsFlow_not_uniquely_ergodic (≥ 2 invariant measures) and obsFlow_continuum_invariant (a continuum) say obsFlow does not uniquely single out μFS. They do not say obsFlow fails to be ergodic with respect to μFS itself: a non-uniquely-ergodic map can still be ergodic for one of its invariant measures. This block proves the sharper statement: obsFlow is not μFS-ergodic, because it has a non-trivial μFS-invariant set ({m₀ ≥ m₁}), of measure strictly between 0 and 1. The structural reason is exactly the conserved Born coordinate momentMap · i (momentMap_obsFlow): a non-constant constant of motion produces a non-trivial invariant set, which is precisely the failure of ergodicity. Framing (LLN, not ergodicity): CSD forces typicality by the LAW OF LARGE NUMBERS over i.i.d. preparations (LF1 / papers A & B), NOT by single-flow time-averaging. So this result is a negative about the stat-mech single-flow ergodicity (Birkhoff) route — a route CSD does not use: it shows one cannot shortcut to μFS through one flow's dynamics, which reinforces that the LLN/i.i.d. route (with the symmetry-canonical measure of (A)) is the operative one. It is NOT an obstruction to CSD's typicality (there is none — the LLN does the forcing).

theorem CSD.LF4.fubiniStudyMeasure_pos_of_isOpen {N : ℕ} [NeZero N] (p₀ : CPN N) {O : Set (CPN N)} (hO : IsOpen O) (hne : O.Nonempty) : (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) O ≠ 0

The Fubini–Study measure has full support. Any nonempty open set O ⊆ ℂℙ^{N-1} has positive μFS mass. μFS = (orbitMap p₀)∗ unitaryHaarProb; the orbit-map preimage of a nonempty open O is open (continuity) and nonempty (U(N)-transitivity), and Haar measure is IsOpenPosMeasure. (General Mathlib-style projective-geometry fact; the witness sets below use it to bound the invariant set away from 0 and 1.)

theorem CSD.LF4.isOpen_momentMap_lt {N : ℕ} (i j : Fin N) : IsOpen {p : CPN N | momentMap p i < momentMap p j}

The strict moment-coordinate comparison {p | momentMap p i < momentMap p j} is open. Pulled back through the open quotient map mk', it is {v ≠ 0 | ‖vᵢ‖²/‖v‖² < ‖vⱼ‖²/‖v‖²}, open as a strict inequality of continuous functions; its image under the open map mk' is the set itself (surjectivity). Uses Projectivization.isOpenMap_mk' / momentMap_mk.

theorem CSD.LF4.momentMap_cpBasisRay {N : ℕ} (q r : Fin N) : momentMap (cpBasisRay r) q = if q = r then 1 else 0

The moment-map coordinate at a computational-basis ray: momentMap [eᵣ] q = δ_{qr}. The non-constancy witness for the conserved Born coordinate.

theorem CSD.LF4.momentMap_obsFlow_nonconstant_conserved {N : ℕ} [NeZero N] (hN : 1 < N) (lam : Fin N → ℝ) (t : ℝ) : (∀ (p : CPN N), momentMap (obsFlow lam t p) (obsIdx0 hN) = momentMap p (obsIdx0 hN)) ∧ (Measurable fun (p : CPN N) => momentMap p (obsIdx0 hN)) ∧ ∃ (p : CPN N) (q : CPN N), momentMap p (obsIdx0 hN) ≠ momentMap q (obsIdx0 hN)

(1) The non-constant conserved observable (the conceptual heart). The Born coordinate momentMap · i is, for obsFlow, simultaneously:

• a constant of motion — momentMap (obsFlow λ t p) i = momentMap p i for every p (momentMap_obsFlow: the diagonal phase e^{itλᵢ} leaves |ψᵢ|² unchanged);
• measurable (momentMap_measurable);
• non-constant — it takes the value 1 at [eᵢ] and 0 at [eⱼ] (j ≠ i) (momentMap_cpBasisRay).

This is exactly a non-constant constant of motion. Its existence is the obstruction to ergodicity (next theorem): an ergodic flow has only a.e.-constant conserved observables.

theorem CSD.LF4.obsFlow_not_ergodic {N : ℕ} [NeZero N] (hN : 1 < N) (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : ¬Ergodic (obsFlow lam t) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

(2) Headline: obsFlow is NOT μFS-ergodic. The set S = {p | momentMap p 1 ≤ momentMap p 0} ({m₀ ≥ m₁}) is an obsFlow-invariant measurable set with 0 < μFS S < 1, contradicting the zero-one law PreErgodic.prob_eq_zero_or_one.

• Invariant (obsFlow ⁻¹' S = S): both coordinates are conserved (momentMap_obsFlow).
• Measurable: measurableSet_le of two momentMap_measurable coordinates.
• μFS S ≠ 0: S ⊇ {m₁ < m₀}, open (isOpen_momentMap_lt) and nonempty ([e₀] has m₁ = 0 < 1 = m₀), so positive by full support (fubiniStudyMeasure_pos_of_isOpen).
• μFS S ≠ 1: Sᶜ = {m₀ < m₁}, open and nonempty ([e₁] has m₀ = 0 < 1 = m₁), so positive; hence μFS S = 1 − μFS Sᶜ < 1.

This is sharper than obsFlow_not_uniquely_ergodic: not merely "≥ 2 invariant measures", but "μFS itself is not an ergodic measure for obsFlow". The two are independent — a non-uniquely-ergodic map can still be ergodic for a particular invariant measure. The obstruction is the non-constant conserved Born coordinate of (1).

Capstone

theorem CSD.LF4.so1_obstruction_capstone {N : ℕ} [NeZero N] (hN : 1 < N) (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : ((∀ (p : CPN N), momentMap (obsFlow lam t p) (obsIdx0 hN) = momentMap p (obsIdx0 hN)) ∧ (Measurable fun (p : CPN N) => momentMap p (obsIdx0 hN)) ∧ ∃ (p : CPN N) (q : CPN N), momentMap p (obsIdx0 hN) ≠ momentMap q (obsIdx0 hN)) ∧ ¬Ergodic (obsFlow lam t) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

SO-1 single-flow obstruction capstone. Packages the obstruction story:

1. momentMap_obsFlow_nonconstant_conserved — a single flow (obsFlow) carries a non-constant conserved observable, the Born coordinate momentMap · 0 (conserved, measurable, takes distinct values at [e₀], [e₁]).
2. obsFlow_not_ergodic — therefore obsFlow is not μFS-ergodic: the non-constant constant of motion produces a non-trivial μFS-invariant set ({m₀ ≥ m₁}, measure in (0,1)).

Honest scope (LLN, not ergodicity). Typicality is forced by the LAW OF LARGE NUMBERS (LF1 / papers A & B), NOT by an ergodic flow. This result CLOSES the single-flow ergodicity (Birkhoff) obstruction story — a route CSD does NOT use: obsFlow, with its conserved Born coordinates, is provably not μFS-ergodic, so one cannot shortcut to μFS through one flow's dynamics. That reinforces the LLN/i.i.d. route rather than exposing a gap. It does not close SO-1: the FS measure is singled out by the full sector symmetry G = U(N) (fubiniStudy_forced_by_symmetry) and the LLN forces frequencies to it; the residue is G-from-D1 — deriving the U(N)-symmetry of the ontic dynamics from CSD's deterministic substrate, which remains open (Φ = id / single non-ergodic phase flow in the concrete SectorData instances).

theorem CSD.LF4.so1_onramp {N : ℕ} [NeZero N] (hN : 1 < N) (p₀ : CPN N) (lam : Fin N → ℝ) (t : ℝ) : (∀ (μ : MeasureTheory.Measure (CPN N)), MeasureTheory.IsProbabilityMeasure μ → (∀ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), MeasureTheory.MeasurePreserving (fun (p : CPN N) => U • p) μ μ) → μ = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) ∧ ∃ (μ : MeasureTheory.Measure (CPN N)) (ν : MeasureTheory.Measure (CPN N)), MeasureTheory.IsProbabilityMeasure μ ∧ MeasureTheory.IsProbabilityMeasure ν ∧ MeasureTheory.Measure.map (obsFlow lam t) μ = μ ∧ MeasureTheory.Measure.map (obsFlow lam t) ν = ν ∧ μ ≠ ν

SO-1 onramp. Conjunction of the two honest results:

• (A) fubiniStudy_forced_by_symmetry: any U(N)-invariant probability measure on the sector ℂℙ^{N-1} is the Fubini–Study measure — so the FS sampling measure is singled out by the sector symmetry G = U(N), not posited as an arbitrary law.
• (B) obsFlow_not_uniquely_ergodic: a single ontic flow (obsFlow) does not single out FS via its dynamics — it has at least two distinct invariant probability measures.

Honest framing (LLN, not ergodicity). Typicality — frequencies converging to the measure's volume weights — is forced by the LAW OF LARGE NUMBERS (LF1 / papers A & B) over i.i.d. preparations, NOT by symmetry and NOT by an ergodic flow. (A) only singles out which measure is canonical (the unique G-invariant one); (B) is a negative about the single-flow ergodicity route CSD does not use. So this does not force typicality (the LLN does) and does not close SO-1; the residual SO-1 primitive is G = U(N) itself, which reduces to D1 (deriving the U(N)-symmetry of the ontic dynamics from CSD's deterministic substrate — not done, the deepest open CSD content). It locates the measure-characterisation in the symmetry and pins the residue.