LF4 §14.2 multi-region spectral carving (N-arc partition of the fibre)

Category: 3-Local (LF4 §14.2 ontic-side multi-region carving — the infrastructure to lift the Hilbert-side spectral expansion ⟨ψ, A ψ⟩ = ∑ᵢ λᵢ · ‖⟨uᵢ, ψ⟩‖² (proved in SpectralExpansion.lean) to a full ontic ↔ Hilbert observable correspondence for any Hermitian observable of any finite dimension).

The existing fibreArc ℓ = (0, ℓ] primitive (SingletKahler.lean) is anchored at zero: distinct fibreArc w₁, fibreArc w₂ are nested, not disjoint. The existing Hardy four-region setup is "disjoint" only because three of its four arcs are vacuous (zero-length). For a genuine N-arc partition with weights summing to one we need a shifted primitive, plus cumulative-sum index arithmetic.

Module contents

• Phase A — fibreShiftedArc c ℓ := (0,1]⁻¹ preimage of (c, c+ℓ]. Measurability, volume = ENNReal.ofReal ℓ when [c, c+ℓ] ⊆ [0,1], and pairwise disjointness when the underlying ℝ-intervals are disjoint.

• Phase B — cumulative-sum prefixes cumWeights w : Fin (N+1) → ℝ with cumWeights w 0 = 0, `cumWeights w i.succ = cumWeights w i.castSucc

  • w i, monotone for nonnegative w, and the bound cumWeights w i.castSucc + w i ≤ ∑ w. Built on a ℕ-recursive cumWeightsAux` for a clean inductive structure.

• Phase C — N-region spectral carving on the existing Kähler instance KSigma M: spectralRegion w i := univ ×ˢ (fibreShiftedArc (cumWeights w i.castSucc) (w i) ×ˢ univ). Measurability, the carving identity (Dirac p₀ ⊗ vol_T²) (spectralRegion w i) = ENNReal.ofReal (w i) (for w nonnegative with ∑ w ≤ 1), and pairwise disjointness.

Tier-2 posture (unchanged)

The fibre arcs are carved to the Born values by construction (the shifted-arc length equals the prescribed weight). What's new is that the resulting N-arc partition is genuinely disjoint, and the per-region carving identity composes through Finset.sum to give an ontic spectral observable whose integral against the preparation measure equals the Hilbert expectation value.

Axiom posture

Foundational triple only.

Phase A — shifted fibre arc primitive

noncomputable def CSD.LF4.fibreShiftedArc (c ℓ : ℝ) : Set (AddCircle 1)

The shifted fibre arc (c, c+ℓ] on AddCircle 1, the preimage of the ℝ-interval Ioc c (c+ℓ) under the chart equivIoc 1 0 : AddCircle 1 ≃ Ioc 0 1. Concretely a subset of the unit circle of arc length ℓ shifted to start at parameter c.

Equations

• CSD.LF4.fibreShiftedArc c ℓ = ⇑(AddCircle.equivIoc 1 0) ⁻¹' Subtype.val ⁻¹' Set.Ioc c (c + ℓ)

theorem CSD.LF4.fibreShiftedArc_measurable (c ℓ : ℝ) : MeasurableSet (fibreShiftedArc c ℓ)

theorem CSD.LF4.fibreShiftedArc_volume {c ℓ : ℝ} (hc : 0 ≤ c) (hcℓ : c + ℓ ≤ 1) : MeasureTheory.volume (fibreShiftedArc c ℓ) = ENNReal.ofReal ℓ

The shifted fibre arc has Haar volume ℓ when [c, c+ℓ] ⊆ [0, 1].

theorem CSD.LF4.fibreShiftedArc_disjoint {c₁ ℓ₁ c₂ ℓ₂ : ℝ} (h : c₁ + ℓ₁ ≤ c₂) : Disjoint (fibreShiftedArc c₁ ℓ₁) (fibreShiftedArc c₂ ℓ₂)

Two shifted arcs whose ℝ-intervals satisfy c₁ + ℓ₁ ≤ c₂ are disjoint as subsets of AddCircle 1.

Phase B — cumulative weights (Finset.filter form)

noncomputable def CSD.LF4.cumWeights {N : ℕ} (w : Fin N → ℝ) (k : Fin (N + 1)) : ℝ

Cumulative-sum prefixes of a weight vector w : Fin N → ℝ, indexed by Fin (N+1). cumWeights w k = ∑_{j.val < k.val} w j. The Finset.filter form gives clean direct proofs of the key lemmas (succ-castSucc step, monotonicity, last-index sum) via Finset.sum_insert / Finset.sum_le_sum_of_subset_of_nonneg.

Equations

• CSD.LF4.cumWeights w k = ∑ j : Fin N with ↑j < ↑k, w j

theorem CSD.LF4.cumWeights_zero {N : ℕ} (w : Fin N → ℝ) : cumWeights w 0 = 0

theorem CSD.LF4.cumWeights_succ_castSucc {N : ℕ} (w : Fin N → ℝ) (i : Fin N) : cumWeights w i.succ = cumWeights w i.castSucc + w i

theorem CSD.LF4.cumWeights_last {N : ℕ} (w : Fin N → ℝ) : cumWeights w (Fin.last N) = ∑ j : Fin N, w j

theorem CSD.LF4.cumWeights_mono {N : ℕ} {w : Fin N → ℝ} (hw : ∀ (i : Fin N), 0 ≤ w i) : Monotone (cumWeights w)

theorem CSD.LF4.cumWeights_nonneg {N : ℕ} {w : Fin N → ℝ} (hw : ∀ (i : Fin N), 0 ≤ w i) (i : Fin (N + 1)) : 0 ≤ cumWeights w i

theorem CSD.LF4.cumWeights_succ_le_sum {N : ℕ} {w : Fin N → ℝ} (hw : ∀ (i : Fin N), 0 ≤ w i) (hsum : ∑ j : Fin N, w j ≤ 1) (i : Fin N) : cumWeights w i.castSucc + w i ≤ 1

Phase C — N-region spectral carving on KSigma M

noncomputable def CSD.LF4.spectralRegion {N M : ℕ} (w : Fin N → ℝ) (i : Fin N) : Set (KSigma M)

Multi-region fibre carving: the i-th spectral region on KSigma M, indexed by Fin N, with weights w : Fin N → ℝ. The fibre arc spans (cumWeights w i.castSucc, cumWeights w i.succ] (length w i by cumWeights_succ_castSucc). Independent of the base preparation.

Equations

• CSD.LF4.spectralRegion w i = Set.univ ×ˢ CSD.LF4.fibreShiftedArc (CSD.LF4.cumWeights w i.castSucc) (w i) ×ˢ Set.univ

theorem CSD.LF4.spectralRegion_measurable {N M : ℕ} (w : Fin N → ℝ) (i : Fin N) : MeasurableSet (spectralRegion w i)

theorem CSD.LF4.diracProd_spectralRegion {N M : ℕ} (p₀ : CPN M) {w : Fin N → ℝ} (hw : ∀ (i : Fin N), 0 ≤ w i) (hsum : ∑ j : Fin N, w j ≤ 1) (i : Fin N) : ((MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume) (spectralRegion w i) = ENNReal.ofReal (w i)

The N-arc spectral carving identity on any Dirac-on-base × T² preparation: the i-th region has measure w i, for nonnegative w with ∑ w ≤ 1.

theorem CSD.LF4.spectralRegion_pairwise_disjoint {N M : ℕ} {w : Fin N → ℝ} (hw : ∀ (i : Fin N), 0 ≤ w i) : Pairwise (Function.onFun Disjoint (spectralRegion w))

Pairwise disjointness of the N-arc spectral regions.

Phase D — Born weights, spectral observable, and integration identity

noncomputable def CSD.LF4.bornWeights {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : Fin N → ℝ

Born weights of a Hermitian matrix A on a state ψ: the squared moduli ‖⟨uᵢ, ψ⟩‖² of the projections onto the eigenvectors of A. These sum to ‖ψ‖² (Parseval / OrthonormalBasis.sum_sq_norm_inner_right).

Equations

• CSD.LF4.bornWeights hA ψ i = ‖inner ℂ (hA.eigenvectorBasis i) ψ‖ ^ 2

theorem CSD.LF4.bornWeights_nonneg {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : 0 ≤ bornWeights hA ψ i

theorem CSD.LF4.bornWeights_sum_eq_norm_sq {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : ∑ i : Fin N, bornWeights hA ψ i = ‖ψ‖ ^ 2

theorem CSD.LF4.bornWeights_sum_eq_one {N : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) : ∑ i : Fin N, bornWeights hA ψ i = 1

noncomputable def CSD.LF4.spectralOntic {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : KSigma M → ℝ

Ontic spectral observable: the eigenvalue-weighted indicator sum over the N spectral outcome regions. Each region spectralRegion (bornWeights hA ψ) i has fibre measure ‖⟨uᵢ, ψ⟩‖² under the Dirac × T² preparation, and the indicator-weighted sum represents the ontic counterpart of A.

Equations

• CSD.LF4.spectralOntic hA ψ σ = ∑ i : Fin N, hA.eigenvalues i * (CSD.LF4.spectralRegion (CSD.LF4.bornWeights hA ψ) i).indicator (fun (x : CSD.LF4.KSigma M) => 1) σ

theorem CSD.LF4.spectralOntic_measurable {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) : Measurable (spectralOntic hA ψ)

theorem CSD.LF4.spectralOntic_integrable {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) (ψ : EuclideanSpace ℂ (Fin N)) (p₀ : CPN M) : MeasureTheory.Integrable (spectralOntic hA ψ) ((MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume)

theorem CSD.LF4.integral_spectralOntic_eq_inner_re {N M : ℕ} {A : Matrix (Fin N) (Fin N) ℂ} (hA : A.IsHermitian) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ‖ψ‖ = 1) (p₀ : CPN M) : ∫ (σ : CPN M × KTorus), spectralOntic hA ψ σ ∂(MeasureTheory.Measure.dirac p₀).prod MeasureTheory.volume = RCLike.re (inner ℂ ψ ((Matrix.toEuclideanLin A) ψ))

§14.2 ontic-Hilbert observable correspondence at the integration level: for any Hermitian A : Matrix (Fin N) (Fin N) ℂ and unit state ψ : EuclideanSpace ℂ (Fin N), on any Kähler instance KSigma M with preparation (Dirac p₀) × vol_T², the ontic spectral observable integrates to the real part of the Hilbert expectation value. Composes the Phase C multi-region carving identity (diracProd_spectralRegion) with the SpectralExpansion.hermitian_inner_spectral_expansion_re identity.