LF3 SectorSeparation: sector-state decomposition and pointer-leakage bounds

Category: 3-Local (LF3 sector-separated final state, per-wing pointer overlaps, leakage bound).

Paper §4 / §9.6. (Renamed from BranchSeparation in Phase 11, 2026-05-18, to align with the volume-ratios reading: the four (s, t) regions are eigensectors / volume domains, not Everettian branches.)

Defines the sector-separated final state, the per-wing pointer-overlap observables, and the cross-sector readout mass; bundles the per-side leakage parameters as PointerLeakageBounds; proves the sector-decomposition law (definitional under MeasurementUnitary.action) and the operational distinguishability bound.

The amplitude cAmp : Sign → Sign → ℂ is carried as an external parameter; the concrete singlet amplitude is supplied later in Singlet/State.lean so the import direction stays SectorSeparation → Singlet/State.

noncomputable def CSD.LF3.sectorState {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (M : MeasurementUnitary S) (s t : Sign) (φA0 : K_A) (φB0 : K_B) : H_SA

Sector state |B_{st}⟩ = |s, t⟩ ⊗ uA|φ_A⁰⟩ ⊗ uB|φ_B⁰⟩, packaged through the joint eigenstate field of MeasurementUnitary. Each sector labels one of the four spin pointer-eigenspaces (s, t) ∈ Sign × Sign.

Equations

• CSD.LF3.sectorState M s t φA0 φB0 = M.jointEig (s, t) (M.ptrTransA s φA0) (M.ptrTransB t φB0)

noncomputable def CSD.LF3.finalState {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (M : MeasurementUnitary S) (cAmp : Sign → Sign → ℂ) (φA0 : K_A) (φB0 : K_B) : H_SA

Sector-separated final state after the measurement unitary acts on the initial pointer state, with the amplitude cAmp (carrying the detector-setting dependence) supplied externally.

Equations

• CSD.LF3.finalState M cAmp φA0 φB0 = ∑ st : CSD.LF3.Sign × CSD.LF3.Sign, cAmp st.1 st.2 • CSD.LF3.sectorState M st.1 st.2 φA0 φB0

noncomputable def CSD.LF3.pointerOverlapA {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (S : SystemApparatusSetup K_A K_B H_SA) (M : MeasurementUnitary S) (φA0 : K_A) (s' s : Sign) : ℝ

s'-sector Born weight of the A-pointer translated by M.ptrTransA s starting from φA0.

Equations

• CSD.LF3.pointerOverlapA S M φA0 s' s = ‖(S.ptrA.proj s') (M.ptrTransA s φA0)‖ ^ 2

noncomputable def CSD.LF3.pointerOverlapB {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (S : SystemApparatusSetup K_A K_B H_SA) (M : MeasurementUnitary S) (φB0 : K_B) (t' t : Sign) : ℝ

t'-sector Born weight of the B-pointer translated by M.ptrTransB t starting from φB0.

Equations

• CSD.LF3.pointerOverlapB S M φB0 t' t = ‖(S.ptrB.proj t') (M.ptrTransB t φB0)‖ ^ 2

noncomputable def CSD.LF3.crossSectorReadoutMass {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (S : SystemApparatusSetup K_A K_B H_SA) (M : MeasurementUnitary S) (cAmp : Sign → Sign → ℂ) (φA0 : K_A) (φB0 : K_B) : ℝ

Total Born mass landing on a cross-sector readout after measurement: for each spin sector (s, t) with amplitude cAmp s t, the squared amplitude is weighted by the cross-sector overlap mass on each side.

Equations

• One or more equations did not get rendered due to their size.

structure CSD.LF3.PointerLeakageBounds {K_A : Type u_4} {K_B : Type u_5} {H_SA : Type u_6} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] (S : SystemApparatusSetup K_A K_B H_SA) (M : MeasurementUnitary S) (φA0 : K_A) (φB0 : K_B) : Type

Per-side pointer-leakage bounds (paper §4.7). εA, εB upper-bound the wrong-sector pointer overlap on each wing; the _right fields lower-bound the correct-sector overlap. Parameterised over the apparatus S, the measurement unitary M, and the chosen initial pointer states φA0, φB0 (needed to make the overlap predicates well-typed).

• εA : ℝ

  A-wing leakage parameter.

• εB : ℝ

  B-wing leakage parameter.

• εA_nn : 0 ≤ self.εA

  The A-wing leakage parameter is non-negative.

• εB_nn : 0 ≤ self.εB

  The B-wing leakage parameter is non-negative.

• A_wrong (s : Sign) : pointerOverlapA S M φA0 s.neg s ≤ self.εA

  Wrong-sector overlap on the A side is bounded by εA.

• B_wrong (t : Sign) : pointerOverlapB S M φB0 t.neg t ≤ self.εB

  Wrong-sector overlap on the B side is bounded by εB.

• A_right (s : Sign) : 1 - self.εA ≤ pointerOverlapA S M φA0 s s

  Right-sector overlap on the A side is at least 1 - εA.

• B_right (t : Sign) : 1 - self.εB ≤ pointerOverlapB S M φB0 t t

  Right-sector overlap on the B side is at least 1 - εB.

The leakage bounds are non-vacuous (the consumers of A_right / B_right)

A_wrong / B_wrong bound the wrong-sector overlap above; the sector-separation theorems below use only those. On their own they are satisfied by a completely uninformative pointer — set every overlap to 0 and any εA, εB ≥ 0 works. What rules that out is A_right / B_right, the matching bounds below on the right-sector overlap.

Until 2026-07-28 those two fields were carried by every instance and consumed by nothing (scripts/check-vacuity.sh), so the two-sided reading of PointerLeakageBounds was unsupported: nothing in the corpus depended on the pointer registering anything. The lemmas here are their consumers, and they say what the fields are for.

theorem CSD.LF3.pointerOverlapA_pos {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} {M : MeasurementUnitary S} {φA0 : K_A} {φB0 : K_B} (L : PointerLeakageBounds S M φA0 φB0) (h : L.εA < 1) (s : Sign) : 0 < pointerOverlapA S M φA0 s s

The A-wing pointer actually registers: with leakage εA < 1 the right-sector overlap is strictly positive. Consumes A_right.

theorem CSD.LF3.pointerOverlapB_pos {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} {M : MeasurementUnitary S} {φA0 : K_A} {φB0 : K_B} (L : PointerLeakageBounds S M φA0 φB0) (h : L.εB < 1) (t : Sign) : 0 < pointerOverlapB S M φB0 t t

The B-wing pointer actually registers. Consumes B_right.

theorem CSD.LF3.pointerOverlapA_discriminates {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} {M : MeasurementUnitary S} {φA0 : K_A} {φB0 : K_B} (L : PointerLeakageBounds S M φA0 φB0) (h : L.εA < 1 / 2) (s : Sign) : pointerOverlapA S M φA0 s.neg s < pointerOverlapA S M φA0 s s

The A-wing pointer discriminates: below εA = ½ the right-sector overlap strictly exceeds the wrong-sector one, so the pointer carries genuine information about the sector rather than merely failing to leak. Consumes A_right and A_wrong.

theorem CSD.LF3.pointerOverlapB_discriminates {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} {M : MeasurementUnitary S} {φA0 : K_A} {φB0 : K_B} (L : PointerLeakageBounds S M φA0 φB0) (h : L.εB < 1 / 2) (t : Sign) : pointerOverlapB S M φB0 t.neg t < pointerOverlapB S M φB0 t t

The B-wing pointer discriminates. Consumes B_right and B_wrong.

theorem CSD.LF3.pointerLeakage_nonvacuous {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} {M : MeasurementUnitary S} {φA0 : K_A} {φB0 : K_B} (L : PointerLeakageBounds S M φA0 φB0) (hA : L.εA < 1 / 2) (hB : L.εB < 1 / 2) : (∀ (s : Sign), 0 < pointerOverlapA S M φA0 s s) ∧ (∀ (t : Sign), 0 < pointerOverlapB S M φB0 t t) ∧ (∀ (s : Sign), pointerOverlapA S M φA0 s.neg s < pointerOverlapA S M φA0 s s) ∧ ∀ (t : Sign), pointerOverlapB S M φB0 t.neg t < pointerOverlapB S M φB0 t t

Non-vacuity of the leakage bounds, both wings. Small leakage forces the pointers to register and to discriminate — so PointerLeakageBounds is not inhabited by the null model in which nothing is recorded. This is what the A_right/B_right fields buy, and the reason the sector-separation results below are about a real apparatus.

Theorem targets (paper §4.11 / spec §9.6)

theorem CSD.LF3.finalState_sector_decomposition {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (M : MeasurementUnitary S) (cAmp : Sign → Sign → ℂ) (φA0 : K_A) (φB0 : K_B) : finalState M cAmp φA0 φB0 = ∑ st : Sign × Sign, cAmp st.1 st.2 • sectorState M st.1 st.2 φA0 φB0

Sector decomposition of the final state (paper §4.5): the final state is the four-term sum of sector states weighted by cAmp. Definitional unfolding of finalState.

theorem CSD.LF3.sector_separation_leakage_bound {K_A : Type u_1} {K_B : Type u_2} {H_SA : Type u_3} [NormedAddCommGroup K_A] [InnerProductSpace ℂ K_A] [FiniteDimensional ℂ K_A] [NormedAddCommGroup K_B] [InnerProductSpace ℂ K_B] [FiniteDimensional ℂ K_B] [NormedAddCommGroup H_SA] [InnerProductSpace ℂ H_SA] [FiniteDimensional ℂ H_SA] {S : SystemApparatusSetup K_A K_B H_SA} (M : MeasurementUnitary S) (cAmp : Sign → Sign → ℂ) (φA0 : K_A) (φB0 : K_B) (L : PointerLeakageBounds S M φA0 φB0) (hAmp : ∑ st : Sign × Sign, ‖cAmp st.1 st.2‖ ^ 2 ≤ 1) : crossSectorReadoutMass S M cAmp φA0 φB0 ≤ L.εA + L.εB

Cross-sector readout mass is bounded by εA + εB given amplitude normalisation (paper §4.11). The proof sums the per-side leakage bounds weighted by ‖cAmp st‖² and uses ∑ ‖cAmp st‖² ≤ 1.

Disclosure-infrastructure status. This theorem is standalone in the current Lean tree: no LF3 export consumes it. LF3_finite_leakage_theorem routes through the operator-form LeakageCompat.sectorVolume_dev field (in Projectors/SectorVolume.lean) instead, which is structurally a more direct bound on the quantity the chain capstones actually consume. The geometric sector_separation_leakage_bound here is kept as paper-side disclosure infrastructure: it makes the §4.11 inequality formally available even though the operator-form path supersedes it in the v1.00 chain. A v2 refactor connecting the two would replace LeakageCompat.sectorVolume_dev with a derived form using this lemma plus a Cauchy-Schwarz step. Not scheduled for LF4.