LF4/HatBox: the Archimedes hat-box for the qubit (context-fixed measurement infra, A7)

Category: 2-LF4 (Kähler / moment-map layer — sphere-measure infrastructure).

The single-axis crux integral for the context-fixed qubit measurement (Paper C A7, specs/record-layer-plan.md §2): the Fubini–Study average over ℂℙ¹ of the Bloch height |λ·n| = |2·momentMap − 1| is ½ — Archimedes' hat-box. This is the piece the qubit context-fixed proof reduces to (via ρ_m = 2(m·λ) + 2|m·λ| and the hemisphere indicator = ½(1 + sign(λ·n))).

It is not raw S² integration (Mathlib lacks that): it reduces to the proved fact that the moment coordinate is Uniform[0,1] (fs_moment_pushforward_uniform, the ℂℙ¹ Duistermaat–Heckman / Archimedes result) plus the elementary 1-D integral ∫_{[0,1]} |2t−1| dt = ½. Foundational-triple, no sorry.

References

LF4/MomentUniform.lean (fs_moment_pushforward_uniform — the moment coordinate is Uniform[0,1]); LF4/MomentMap.lean (momentMap); specs/record-layer-plan.md §2 (the qubit context-fixed crux).

theorem CSD.LF4.integral_abs_two_mul_sub_one : ∫ (t : ℝ) in Set.Icc 0 1, |2 * t - 1| = 1 / 2

The 1-D core of the hat-box: ∫_{[0,1]} |2t − 1| dt = ½.

theorem CSD.LF4.hatBox_moment (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), |2 * momentMap p 0 - 1| ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1 / 2

The Archimedes hat-box (qubit). The Fubini–Study average over ℂℙ¹ of the Bloch height |λ·n| = |2·momentMap p 0 − 1| is ½. Equivalent to the moment coordinate being Uniform[0,1] (fs_moment_pushforward_uniform) plus the 1-D integral (integral_abs_two_mul_sub_one). The single-axis crux for the context-fixed qubit measurement.

theorem CSD.LF4.integral_max_two_mul_sub_one_zero : ∫ (t : ℝ) in Set.Icc 0 1, max (2 * t - 1) 0 = 1 / 4

The 1-D core of the spread-density normalisation: ∫_{[0,1]} max(2t − 1, 0) dt = ¼.

theorem CSD.LF4.spreadDensity_normalized (p₀ : CPN 2) : ∫ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin 2))), 4 * max (2 * momentMap p 0 - 1) 0 ∂Matrix.UnitaryGroup.fubiniStudyMeasure p₀ = 1

The spread density is a probability density. For the reference (e₀) axis, the CSD spread density ρ = 4·max(2·momentMap − 1, 0) (Bloch form 4(m·λ)₊) integrates to 1 against the Fubini–Study measure — the normalisation ∫ ρ dμ_FS = 1 of record-layer-plan.md §2. Via the moment coordinate being Uniform[0,1] (fs_moment_pushforward_uniform) + integral_max_two_mul_sub_one_zero.