SigmaLayer/OutcomeField: outcome count decoupled from dimension (item 7)

Category: 7-SigmaLayer (the record layer — generalisation).

ContextField N ties the number of outcomes to the Hilbert-space dimension: rate : CPN N → Fin N. That is right for a nondegenerate measurement and wrong for everything else — a degenerate projective measurement has fewer outcomes than dimensions.

OutcomeField N K decouples them.

★ The design constraint this file respects

The plan is explicit on two points, and both are followed:

1. Introduce OutcomeField alongside ContextField, do not replace every use of it. globalBasin and everything downstream still take a ContextField; nothing was refactored. The conversion ContextField.toOutcomeField shows the generalisation is conservative.
2. Do not treat an arbitrary simplex-valued rate field as automatically physical. An OutcomeField is a measurable simplex-valued field and no more — inhabiting it proves nothing about an apparatus. The physical content is in blockField, which derives the field from a measurement's degeneracy structure rather than positing it.

What is proved

• OutcomeField N K — a measurable simplex-valued rate field with K outcomes on ℂℙ^{N-1}.
• ContextField.toOutcomeField — every context field is one, with K = N. Conservativity.
• blockField — ★ degenerate projective measurements. Given a degeneracy map b : Fin N → Fin K grouping basis directions into outcomes, the rate of outcome i is ∑_{b j = i} momentMap p j. Non-negativity, normalisation and measurability all come free from the moment map's, because the field is a finite sum of moment coordinates — the same object, coarse-grained.
• blockField_id — with b = id this is exactly momentContext, so the nondegenerate case is recovered rather than replaced.

The remaining extensions, in the plan's order

blockField covers degenerate projective measurements (step 2). Corrected 2026-08-04 (codebase audit). — steps 1, 3, 4 and 5 have all since landed (measurement_covariance, SigmaLayer/RotatedSwap.lean; mixed_swap_sector_born, MixedSwap.lean, with the conditioned update in MixedLuders.lean; povm_selector_born/povm_instrument, PovmDynamics.lean). What this module does not do is drive them. Formerly: still open, and not attempted here: arbitrary orthonormal bases by unitary covariance (step 1 — the U(N) action on CPN exists, so this should be cheap); mixed preparations by trace linearity (step 3); POVMs through the existing Naimark machinery (step 4); instrument-level updates (step 5).

⚠️ And note what is not connected: globalBasin still consumes a ContextField, so an OutcomeField cannot yet drive the dynamical layer. Generalising globalBasin is the bridge, and it is deliberately not done here — see design constraint 1.

References

SigmaLayer/GlobalBasin.lean (ContextField, momentContext); LF4/MomentMap.lean (momentMap_nonneg, momentMap_sum_eq_one, measurable_momentMap); specs/BACKLOG.md.

structure CSD.RecordLayer.OutcomeField (N K : ℕ) : Type

A measurement's outcome field: a measurable, simplex-valued rate field with K outcomes on the N-dimensional projective base. Unlike ContextField, the outcome count is independent of the dimension, which is what a degenerate measurement needs.

⚠️ Inhabiting this proves nothing about a physical apparatus — it is a measurability-and-simplex condition. See blockField for a field that is derived from a measurement rather than posited.

• rate : LF4.CPN N → Fin K → ℝ

  The rate assigned to each ontic base point.

• measurable_rate (i : Fin K) : Measurable fun (p : LF4.CPN N) => self.rate p i

  Each coordinate is measurable.

• nonneg (p : LF4.CPN N) (i : Fin K) : 0 ≤ self.rate p i

  The rates are non-negative.

• sum_one (p : LF4.CPN N) : ∑ i : Fin K, self.rate p i = 1

  The rates are normalised.

def CSD.RecordLayer.ContextField.toOutcomeField {N : ℕ} (c : ContextField N) : OutcomeField N N

Conservativity: every ContextField is an OutcomeField with K = N. The generalisation adds cases, it does not change the existing ones.

Equations

• c.toOutcomeField = { rate := c.rate, measurable_rate := ⋯, nonneg := ⋯, sum_one := ⋯ }

Degenerate projective measurements

noncomputable def CSD.RecordLayer.blockField {N K : ℕ} (b : Fin N → Fin K) : OutcomeField N K

★ The outcome field of a degenerate projective measurement.

b : Fin N → Fin K is the degeneracy map: it says which outcome each basis direction belongs to. The rate of outcome i is the total moment-map weight of its block,

rate p i = ∑_{j : b j = i} momentMap p j

which is the ontic form of ⟨ψ, Π_i ψ⟩ for the projector Π_i onto that block's eigenspace.

★ Every field condition comes free from the moment map's, because this is a finite sum of moment coordinates — the same object, coarse-grained. Nothing new is posited: the degeneracy structure is the only input, and it is combinatorial.

Equations

• CSD.RecordLayer.blockField b = { rate := fun (p : CSD.LF4.CPN N) (i : Fin K) => ∑ j : Fin N with b j = i, CSD.LF4.momentMap p j, measurable_rate := ⋯, nonneg := ⋯, sum_one := ⋯ }

theorem CSD.RecordLayer.blockField_id {N : ℕ} (p : LF4.CPN N) (i : Fin N) : (blockField id).rate p i = (momentContext N).rate p i

The nondegenerate case is recovered, not replaced. With the identity degeneracy map every block is a single direction, so blockField id is momentContext viewed as an OutcomeField.