Where the overwhelming majority comes from: nearness to a pointer ray

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #105(a), out of #103.

MacrostateStability.lean (#103) proved the majority half of what makes #102's record string macroscopic, but conditionally: ★★ measure_robustBasin_ge_one_sub needs 1 − ε ≤ c.rate p i, and #103 recorded why the hypothesis cannot be dropped — globalBasin_prob makes a cell's measure exactly its Born weight, so no cell is overwhelming unless the weights are. "Overwhelmingly many microstates share the record" is therefore a statement about the preparation and the apparatus, not about the coordinate.

This file supplies the hypothesis for the canonical apparatus, and gives it a geometric reading.

What is proved

• offPointer i ψ — the component of a preparation orthogonal to the i-th pointer ray, with ★ norm_offPointer_sq: ‖offPointer i ψ‖² = ‖ψ‖² − ‖ψ i‖², so the defect is the missing Born weight;
• ★ momentMap_mk_eq_coord_sq — for a unit preparation the canonical context's rate is the squared coordinate, and hence ★★ one_sub_le_momentMap_of_near_pointer: a preparation within √ε of the pointer ray has rate at least 1 − ε there. This is the concentration hypothesis, read as a distance;
• ★★★ measure_robustBasin_ge_of_near_pointer and the distance form ★★★ measure_robustBasin_ge_of_dist_le — near a pointer ray the record macrostate is both overwhelming and robust: the cell of outcome i, restricted to the microstates robust to a record write of size δ, carries all but ε + δ of the epistemic measure. This is #105's statement for the canonical apparatus, obtained by feeding the geometry into #103;
• ★★ measure_globalBasin_ge_of_near_pointer — the same without the robustness margin, and ★★★ measure_map_recordMacro_ge_of_near_pointer — the macroscopic law of #102's record string puts all but ε of its mass on one string, which is the form "almost every microstate records the same outcome" takes in the macroscopic law;
• ★ offPointer_single and ★★ measure_robustBasin_ge_of_pointer — non-vacuity: at the pointer state itself the defect is zero and the robust cell carries 1 − δ, so the hypothesis is satisfiable and the bound is not empty.

Honest scope

⚠️ Nothing here drives the base to a pointer ray. The concentration is a property of where the preparation sits, supplied as a hypothesis with a geometric meaning; no dynamics is shown to produce it, and that — a decoherence or pointer-selection model whose rate field concentrates — is BACKLOG #106 and is the hard half of #105. Reading any statement below as "decoherence gives the macrostate" would be exactly the overclaim this file is written to avoid.

⚠️ It is still not fs_chebyshev_concentration. Thermo/CanonicalTypicality.lean concentrates a base statistic over the projective space with a polynomial rate; this file is about one preparation's weight vector at one base point. The two are different statements about different objects and no theorem joins them.

⚠️ Only the canonical pointer basis. momentContext is the standard-basis context, so "pointer ray" means a coordinate ray of EuclideanSpace ℂ (Fin N). A general apparatus enters by transporting the base point with the corresponding unitary, and that transport is not constructed here: no ContextField built from an arbitrary orthonormal basis appears in the corpus, so nothing below is stated for one.

⚠️ A near-pointer preparation is a special preparation. For a generic superposition no cell is overwhelming, and that is correct physics rather than a gap: the bound degrades exactly as the Born weights spread, and measure_robustBasin_ge_of_dist_le is vacuous once r² + δ ≥ 1. The content is the rate at which macroscopicity is bought with nearness to the pointer, not a claim that record macrostates are generically overwhelming.

⚠️ One context. The statements are about a single context's basin, not about a record string of several contexts; #103's measure_robustBasin_ge_one_sub is per-context and so is everything here. Nothing is claimed about a joint cell of two contexts, where #102's contextuality warning applies.

References: records-to-spacetime-scoping.md ST-3; future-work.md; MacrostateStability.lean (#103), RecordMacrostate.lean (#102), GlobalBasin.lean, LF4/MomentMap.lean; specs/BACKLOG.md #105, #106, #103, #102.

The defect from a pointer ray

noncomputable def CSD.RecordLayer.offPointer {N : ℕ} (i : Fin N) (ψ : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin N)

The component of a preparation orthogonal to the i-th pointer ray. Its norm measures how far the preparation is from being a definite pointer state for the canonical apparatus.

Equations

• CSD.RecordLayer.offPointer i ψ = ψ - ψ.ofLp i • EuclideanSpace.single i 1

theorem CSD.RecordLayer.offPointer_apply {N : ℕ} (i : Fin N) (ψ : EuclideanSpace ℂ (Fin N)) (j : Fin N) : (offPointer i ψ).ofLp j = if j = i then 0 else ψ.ofLp j

theorem CSD.RecordLayer.norm_offPointer_sq {N : ℕ} (i : Fin N) (ψ : EuclideanSpace ℂ (Fin N)) : ‖offPointer i ψ‖ ^ 2 = ‖ψ‖ ^ 2 - ‖ψ.ofLp i‖ ^ 2

★ The defect is exactly the missing Born weight. Parseval in coordinates: removing the pointer component removes ‖ψ i‖² from the squared norm and nothing else.

@[simp]

theorem CSD.RecordLayer.offPointer_single {N : ℕ} (i : Fin N) : offPointer i (EuclideanSpace.single i 1) = 0

Nearness to a pointer ray is the concentration hypothesis

theorem CSD.RecordLayer.momentMap_mk_eq_coord_sq {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) : (Projectivization.mk ℂ ψ hψ0).momentMap i = ‖ψ.ofLp i‖ ^ 2

★ The canonical context's rate at a unit preparation is the squared coordinate.

theorem CSD.RecordLayer.one_sub_le_momentMap_of_near_pointer {N : ℕ} {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) {ε : ℝ} (hnear : ‖offPointer i ψ‖ ^ 2 ≤ ε) : 1 - ε ≤ (Projectivization.mk ℂ ψ hψ0).momentMap i

★★ A preparation within √ε of the pointer ray has rate at least 1 − ε there. This is the concentration hypothesis of #103, with a geometric reading: the weight that is missing from the pointer outcome is exactly the squared distance to its ray.

The macrostate near a pointer ray

theorem CSD.RecordLayer.measure_robustBasin_ge_of_near_pointer {N : ℕ} {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) {δ ε : ℝ} (hδ : 0 ≤ δ) (hnear : ‖offPointer i ψ‖ ^ 2 ≤ ε) : ENNReal.ofReal (1 - ε - δ) ≤ (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) (robustBasin (momentContext N) δ i)

★★★ Near a pointer ray the record macrostate is overwhelming and robust. The cell of outcome i, cut down to the microstates robust to a record write of size δ, carries all but ε + δ of the epistemic measure — where ε bounds the squared distance from the preparation to the pointer ray. This is #105's statement for the canonical apparatus: the two halves of "macroscopic" — many microstates, and stable ones — hold together, with the geometry of the preparation as the only input.

theorem CSD.RecordLayer.measure_robustBasin_ge_of_dist_le {N : ℕ} {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) {δ r : ℝ} (hδ : 0 ≤ δ) (hr : ‖offPointer i ψ‖ ≤ r) : ENNReal.ofReal (1 - r ^ 2 - δ) ≤ (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) (robustBasin (momentContext N) δ i)

★★★ The same, read as a distance. A preparation within r of the pointer ray gives a robust macrostate cell of measure at least 1 − r² − δ. ⚠️ Vacuous once r² + δ ≥ 1: macroscopicity is bought with nearness to the pointer, at this rate and no better.

theorem CSD.RecordLayer.measure_globalBasin_ge_of_near_pointer {N : ℕ} {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) {ε : ℝ} (hnear : ‖offPointer i ψ‖ ^ 2 ≤ ε) : ENNReal.ofReal (1 - ε) ≤ (epistemicMeasure (Projectivization.mk ℂ ψ hψ0)) (globalBasin (momentContext N) i)

★★ Without the robustness margin: the basin of the pointer outcome carries all but ε.

theorem CSD.RecordLayer.measure_map_recordMacro_ge_of_near_pointer {N : ℕ} {ψ : EuclideanSpace ℂ (Fin N)} (hψ0 : ψ ≠ 0) (hψ : ‖ψ‖ = 1) (i : Fin N) {ε : ℝ} (hnear : ‖offPointer i ψ‖ ^ 2 ≤ ε) : ENNReal.ofReal (1 - ε) ≤ (MeasureTheory.Measure.map (recordMacro fun (x : Fin 1) => momentContext N).toFun (epistemicMeasure (Projectivization.mk ℂ ψ hψ0))) {v : Fin 1 → Fin (N + 1) | v 0 = i.succ}

★★★ The macroscopic law puts all but ε of its mass on one record string. #102's recordMacro for the one-context family, read at a near-pointer preparation: almost every microstate records the same outcome, in the macroscopic law rather than microscopically.

theorem CSD.RecordLayer.measure_robustBasin_ge_of_pointer {N : ℕ} (i : Fin N) {δ : ℝ} (hδ : 0 ≤ δ) (hψ0 : EuclideanSpace.single i 1 ≠ 0) : ENNReal.ofReal (1 - δ) ≤ (epistemicMeasure (Projectivization.mk ℂ (EuclideanSpace.single i 1) hψ0)) (robustBasin (momentContext N) δ i)

★★ Non-vacuity: at the pointer state the robust cell carries 1 − δ. The hypothesis of the theorems above is satisfiable with ε = 0, so the bounds are not empty.