Discharging the abundance hypothesis for Fubini–Study at N ≥ 3 #
SigmaLayer/ContextFixedA7.lean proved the cap — a base-only, U(N)-covariant, non-negative
preparation density g vanishes a.e. below ½ — conditional on an abundance hypothesis:
that two overlap coordinates can jointly take values in any positive-measure set below ½.
This file discharges that hypothesis for the actual Fubini–Study measure, so the cap becomes
unconditional at N ≥ 3.
The mechanism #
The corpus already knows where μ_FS goes under the moment map: fs_volume_eq_dirichlet_inter
says the pushforward is the uniform (Dirichlet) measure on the open simplex,
μ_FS ((ratioN ∘ momentMap) ⁻¹' R) = M! · vol (R ∩ openSimplexFree).
So abundance becomes a question about Lebesgue measure on Fin M → ℝ: does the set where two
chosen coordinates land in T meet the open simplex in positive volume? For M ≥ 2 it does, and
the construction is explicit — put the two chosen coordinates in T and every other coordinate in
a small interval (0, ε).
The one subtlety is that T ⊆ (0, ½) gives tⱼ + tₖ < 1 pointwise but not uniformly, so the
room left for the other coordinates is not bounded below. exists_trunc_of_volume_pos fixes that
by first passing to a positive-measure part of T bounded away from ½.
Why M ≥ 2, i.e. N ≥ 3 #
M = N − 1 is the number of free simplex coordinates. Two distinct free coordinates exist
exactly when M ≥ 2, i.e. N ≥ 3. At N = 2 there is a single free coordinate and the second
Born weight is 1 − s₁ — functionally dependent, which is precisely
CSD.SigmaLayer.joint_degenerate_of_sum_eq_one (SigmaLayer/ContextFixedA7.lean), the qubit's escape route. So the dimension count
that makes this file work is the same one that makes the qubit exempt.
Status #
With fs_joint_abundance the cap is unconditional at N ≥ 3. That is a derived structural
constraint on any base-only A7 construction, replacing the numerical evidence the retracted
"provably dead" row rested on. It is still not the no-go: the generic-ψ requirement and the
harmonic argument remain open (see ContextFixedA7.lean's header and specs/BACKLOG.md).
References #
SigmaLayer/ContextFixedA7.lean (the reduction and the cap);
LF4/BornRegionUncond.lean (fs_volume_eq_dirichlet_inter);
LF4/MomentRatioUniformN.lean (openSimplexFree, ratioN);
LF4/MomentMap.lean (momentMap_sum_eq_one); specs/BACKLOG.md.
Truncating a low set away from ½ #
A positive-measure set below ½ has a positive-measure part bounded away from ½.
Needed because T ⊆ (0,½) bounds tⱼ + tₖ < 1 pointwise but not uniformly, and the product
construction below needs uniform room for the remaining coordinates.
Positivity on the open simplex #
Abundance on the simplex. For M ≥ 2 and a positive-measure T ⊆ (0,½), the set where
coordinates j ≠ k both land in T meets the open simplex in positive volume.
The abundance hypothesis, discharged for Fubini–Study #
The Fubini–Study measure supplies the abundance hypothesis at N ≥ 3.
Two distinct free moment coordinates jointly take values in any positive-measure T ⊆ (0,½) on a
set of positive μ_FS-measure. Via fs_volume_eq_dirichlet_inter this is exactly the simplex
positivity above, and M ≥ 2 — i.e. N ≥ 3 — is what makes two distinct free coordinates
available.
★ The cap, unconditional at N ≥ 3.
A base-only, U(N)-covariant, non-negative preparation density reproducing Born on the
Fubini–Study sector vanishes almost everywhere on overlap values below ½ — no hypothesis
left over. The N = 2 solution 4(2s−1)₊ is supported exactly on (½, 1], so the bound is
sharp and attained.
N = 2 is exempt structurally, and this proof needs nothing to exclude it: the statement
quantifies over distinct j k : Fin M, which is uninhabited unless M ≥ 2, i.e. N = M + 1 ≥ 3.
For why the qubit escapes the cap — the mathematical content, which is not used here — see
CSD.SigmaLayer.joint_degenerate_of_sum_eq_one (SigmaLayer/ContextFixedA7.lean).
Balanced states are not negligible #
vanishes_below_of_balanced needs states whose overlaps are all small — near the barycentre of
the simplex. ∑ᵢ sᵢ = 1 forces maxᵢ sᵢ ≥ 1/n, and every threshold above that is met on a set of
positive measure, witnessed by a box around the barycentre.
The geometry is split from the arithmetic deliberately: box_in_simplex takes the centre b and
half-width d as abstract reals constrained by linear relations plus the single identity
M·b = 1 − b, so every step inside it is linear. The concrete choice b = 1/(M+1),
d = min(b, c−b)/(M+1) is then made once, in volume_balanced_inter_openSimplexFree_pos.