LF5: the per-microstate pointer-outcome map and the outcome-frequency capstone

Category: 3-Local (LF5 measurement-dynamics layer, outcome-map tranche).

This is LF5-F (LF5 half) of specs/lf5-plan.md: the upgrade of the LF5 capstone from outcome statistics (a sum of per-cell block frequencies, measurement_flow_born_frequency conjunct (5)) to a deterministic per-microstate outcome function, the genuine realisation of the contextual outcome-map slot.

The engine half (CsdLean4/LF4/BornRegionDisjoint.lean) supplies the pairwise-disjointness of the bornRegion cells (so the moment-subdivision is a genuine partition), the per-microstate bornOutcome : CPN (M+1) → Option (Fin (M+1)) (some i on cell i, total off an FS-null set), and the indicator-of-disjoint- union bridge. This module lifts that cell map to the pointer map and lands the single-event outcome-frequency limit.

What is delivered

• vnPointerOutcome — CPN (M+1) → Option (Fin N), the apparatus/pointer index of the microstate's cell: bornOutcome post-composed with the ψ-independent, context-fixed block assignment c ↦ (e.symm c).2 (the second factor of the Fin N × Fin N reindex). The block assignment is the audited tripwire: it does not depend on the preparation, only on the fixed measurement context e.
• vnPointerOutcome_preimage_some — the some i fibre is the pointer-i block union ⋃ n, bornRegion ψ' hψ'0 (e (n, i)).
• measurement_flow_outcome_frequency — the conjunct-(5) upgrade: the frequency of trials whose microstate's outcome is pointer i (a single event per pointer, not a sum of cell frequencies) converges a.s. to the Born weight ‖⟨eᵢ, ψ⟩‖². Conjuncts (1)-(4) of measurement_flow_born_frequency are unchanged; see that theorem for them.
• measurement_flow_outcome_frequency_canonical — the same on the canonical i.i.d. FS trial process (fsTrialMeasure / fsTrial).

The ContextMap slot, now realised

LF3/ContextMap.lean's ContextIndexedOutcomeMaps carries an abstract per-context outcome map F : (ctx) → Domain ctx → Sign × Sign. For the single-system measurement, LF5 now realises that slot both dynamically and definitionally:

• per-context state space = the dilated Σ' = ℂℙ^{N·N−1};
• outcome map = vnPointerOutcome — deterministic (one cell per microstate, by bornRegion_pairwiseDisjoint), total off an FS-null set (bornOutcome_ae_isSome), measurable fibres (bornOutcome_measurable);
• the context enters only through the fixed vN coupling (the flow Φ_vN) plus the ψ-independent block assignment c ↦ (e.symm c).2.

The outcome is fixed by the microstate (deterministic given (ψ, context)), the de-isolation reading required. Honest residue, unchanged from LF5-D/E: the cell shapes (bornRegion ψ') remain ψ'-dependent — the engine's realisation mechanism, with measures forced by the Kähler geometry, not carved; the Born number is from the FS-volume engine; the CSD sector is posited (SO-1); entanglement is deferred (Bell forces a non-local de-isolation map). Single-system projective tier only.

Reference: specs/lf5-plan.md (LF5-F); the owed-since-aeece86 outcome map.

noncomputable def CSD.LF5.vnPointerOutcome {N M : ℕ} (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (e : Fin N × Fin N ≃ Fin (M + 1)) : LF4.CPN (M + 1) → Option (Fin N)

The per-microstate pointer-outcome map. The apparatus/pointer index of the microstate's cell: some ((e.symm c).2) when the microstate lands in cell c, none off the union. The block assignment c ↦ (e.symm c).2 (the second, apparatus, factor of the Fin N × Fin N reindex) is ψ-independent and context-fixed — it depends only on the measurement context e, not on the preparation. Deterministic and total off an FS-null set (inherited from bornOutcome).

Honest A7 caveat (MD-1). The block assignment above is context-fixed, but the outcome cells themselves are the dilated Born regions bornRegion ψ' — so their geometry is preparation-indexed (it depends on the prepared/dilated state ψ'), whereas Paper C's Axiom A7 asks for context-fixed outcome regions Ωᵢ(M) with μ_FS-null boundaries, independent of the preparation. This map is therefore an honest preparation-indexed operational witness, NOT the general Paper C A7 mechanism. Separating the preparation law from context-fixed partitions (and deriving the probabilities by integrating the former over the latter) is the open item MD-1 (specs/BACKLOG.md, specs/reconstruction-status.md §7).

Equations

• CSD.LF5.vnPointerOutcome ψ' hψ'0 e p = Option.map (fun (c : Fin (M + 1)) => (e.symm c).2) (CSD.LF4.bornOutcome ψ' hψ'0 p)

theorem CSD.LF5.vnPointerOutcome_preimage_some {N M : ℕ} (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'0 : ψ' ≠ 0) (e : Fin N × Fin N ≃ Fin (M + 1)) (i : Fin N) : vnPointerOutcome ψ' hψ'0 e ⁻¹' {some i} = ⋃ (n : Fin N), LF4.bornRegion ψ' hψ'0 (e (n, i))

The pointer-i fibre is the pointer-i block union. The set of microstates whose outcome is pointer i is the union over the apparatus index n of the dilated Born cells bornRegion ψ' hψ'0 (e (n, i)). Via bornOutcome_preimage_some and the Option.map fibre algebra + e bijectivity.

theorem CSD.LF5.measurement_flow_outcome_frequency {N M : ℕ} [NeZero N] (_hN : 1 < N) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN (M + 1)) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (j : Fin (M + 1)), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion ψ' hψ'0 j).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin N), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' vnPointerOutcome ψ' hψ'0 e ⁻¹' {some i}).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

LF5-F outcome-frequency capstone: per-microstate pointer outcomes commit the Born frequencies. With the LF5-D/E set-up (unit ψ, dilated state ψ' = piLpCongrLeft e (Vψ)), for i.i.d. FS-typical trials on the dilated ℂℙ^{N·N−1}, almost surely every pointer i has the frequency of trials whose microstate's outcome is pointer i — a single event per pointer, (X k) ⁻¹' (vnPointerOutcome ⁻¹' {some i}), not a sum of per-cell frequencies — converging to the Born weight ‖⟨eᵢ, ψ⟩‖².

This is the conjunct-(5) upgrade of measurement_flow_born_frequency: from outcome statistics (a sum of cell-indicator frequencies) to a deterministic per-microstate outcome function. Conjuncts (1)-(4) (Φ_vN ≠ id, measure-preservation, context-fixedness, committed volume = Born) are unchanged; see measurement_flow_born_frequency for them.

Proof: rewrite the outcome event into the pointer-block union (vnPointerOutcome_preimage_some), turn the union indicator into the block sum (indicator_iUnion_disjoint + pairwise disjointness of the block cells, a sub-family of bornRegion_pairwiseDisjoint), and land on vnDilation_pointer_frequency.

theorem CSD.LF5.measurement_flow_outcome_frequency_canonical {N M : ℕ} [NeZero N] (hN : 1 < N) (e : Fin N × Fin N ≃ Fin (M + 1)) (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ‖ψ‖ = 1) (ψ' : EuclideanSpace ℂ (Fin (M + 1))) (hψ'eq : ψ' = (LinearIsometryEquiv.piLpCongrLeft 2 ℂ ℂ e) ((Matrix.toEuclideanLin (vnDilationV N)) ψ)) (hψ'0 : ψ' ≠ 0) (p₀ : LF4.CPN (M + 1)) : ∀ᵐ (ω : LF4.fsTrialSpace (M + 1)) ∂LF4.fsTrialMeasure p₀, ∀ (i : Fin N), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (LF4.fsTrial (M + 1) k ⁻¹' vnPointerOutcome ψ' hψ'0 e ⁻¹' {some i}).indicator (fun (x : LF4.fsTrialSpace (M + 1)) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2))

LF5-F outcome-frequency capstone on the canonical i.i.d. FS trial process. measurement_flow_outcome_frequency with the trial bundle discharged by the canonical coordinate process (fsTrialMeasure / fsTrial), mirroring measurement_flow_born_frequency_canonical.