Context-fixed A7 at general N: the support reduction #
Category: SigmaLayer (the Paper C A7 architecture).
Paper C A7 asks for outcome regions Ωᵢ(M) ⊂ ℂℙⁿ⁻¹ fixed by the apparatus context M
alone, together with a preparation law ρ_ψ^ep, such that
P(i ∣ M, ψ) = ∫_{Ωᵢ(M)} ρ_ψ^ep dμ_FS = |⟨eᵢ|ψ⟩|².
Under U(N)-covariance the preparation density collapses to ρ_ψ^ep(φ) = g(|⟨ψ|φ⟩|²) for a
single function g : [0,1] → ℝ≥0, the same for every state and every context. So the whole
question is whether such a g exists. At N = 2 it does — g(s) = 4(2s−1)₊, the CSD spread
density, with {Ωᵢ} the hemispheres (LF4/QubitBorn.lean qubitBorn). At N ≥ 3 the question
is open in both directions (specs/BACKLOG.md; the earlier "provably dead" verdict rested on
numerics plus an informal argument and was retracted 2026-07-28).
What this file contributes #
The support reduction: a hard, elementary constraint on any such g, obtained by evaluating
the A7 requirement at the n basis-vector preparations ψ = eⱼ, where the Born weights are
|⟨eᵢ|eⱼ⟩|² = δᵢⱼ. For i ≠ j the requirement says a non-negative integrand integrates to
zero over Ωᵢ, which forces it to vanish a.e. there. Consequently
overlapSupport_ae_subset— the support ofg ∘ sⱼlies insideΩⱼ(a.e.);overlapSupports_ae_disjoint— thensupports are pairwise a.e. disjoint;sum_measure_overlapSupport_le_one— their measures sum to at most1, so by symmetry each is at most1/n.
Read physically: a base-only preparation density must be concentrated, with the region it
occupies shrinking as 1/n, while still integrating to 1. It has to spike. That is a genuine
structural obstruction — it is what the N = 2 solution 4(2s−1)₊, supported exactly on
(½, 1], is doing — and it sharply narrows the space any N ≥ 3 construction must live in.
Deliberately stated over an abstract measure space #
Nothing here needs projective geometry: it is the measure-theoretic core, so it is proved once,
for a probability space with n overlap functions and n disjoint regions. The intended
instantiation is X := CPN n, μ := fubiniStudyMeasure p₀ (a probability measure), s j :=
momentMap · j (momentMap_mk_eq_inner_sq identifies it with |⟨eⱼ|φ⟩|², and
momentMap_sum_eq_one gives ∑ⱼ sⱼ = 1), Ω j := Ωⱼ(M). Keeping it abstract also means the
result survives a move to a fibred Σ, where the same reduction applies verbatim.
What this does NOT do #
It is not the no-go. It constrains g; it does not refute it. Two things stand between this
and a genuine N ≥ 3 impossibility theorem:
- The generic-
ψrequirement is untouched. Everything here comes from thenbasis-vector preparations. The suspected obstruction lives at genericψ, where the Born value|⟨eᵢ|ψ⟩|²varies continuously and the cap aroundψstraddles several regions. - The harmonic argument is out of reach. The informal reason for pessimism is that
g(|⟨ψ|φ⟩|²)integrated over a fixed region produces, as a function ofψ, components of every degree(k,k), while the target|⟨eᵢ|ψ⟩|²is pure degree(1,1); killing the higher harmonics for all regions and all contexts is what should fail atN ≥ 3. Formalising that needs representation theory / harmonic analysis onℂℙⁿ⁻¹for which Mathlib has no API.
So: this is step one of the no-go, and it is honest about being step one.
References #
LF4/QubitBorn.lean (qubitBorn, the N = 2 case that does work); LF4/MomentMap.lean
(momentMap_mk_eq_inner_sq, momentMap_sum_eq_one); specs/BACKLOG.md (the re-opened
general-N A7 row, and the hpos boundary row — note the DH region machinery cannot express a
vanishing amplitude, a second structural limit at this same spot);
specs/record-layer-plan.md §3; specs/sigma-fibre-contextuality.md.
The set where the preparation density is non-zero at overlap function s: the ontic states
that a preparation with overlap profile s can actually occupy.
Instances For
The reduction #
A non-negative density with a vanishing Born weight vanishes on that region.
This is the whole mechanism, isolated. The A7 requirement at preparation eⱼ and outcome i ≠ j
reads ∫_{Ωᵢ} g(sⱼ) dμ = |⟨eᵢ|eⱼ⟩|² = 0; since g ≥ 0, a zero integral forces the integrand to
vanish almost everywhere on Ωᵢ. Non-negativity of the preparation density is doing all the work
— exactly the hypothesis a signed density would escape.
The support of the density for outcome j lies inside region j (up to a null set).
Given the off-diagonal A7 conditions — the Born weight of outcome i at preparation eⱼ is zero
for i ≠ j — and a covering family of regions, the states where g(sⱼ) ≠ 0 cannot lie in any
region other than Ωⱼ.
The supports are pairwise almost disjoint. Distinct outcomes' preparation supports cannot overlap on a set of positive measure: each is confined to its own region, and the regions are disjoint.
The supports occupy at most the whole space, hence at most 1/n each by symmetry.
The quantitative form of the reduction: a base-only preparation density is confined to n
pairwise-disjoint sets whose measures sum to at most 1. Each must still carry total integral
1, so as n grows the density has to spike on an ever-smaller set.
Step two: the cap — the density is confined above ½ #
The supports are Aᵢ = {φ : sᵢ(φ) ∈ S_g} for S_g = {t | g t ≠ 0}, and step one showed them
pairwise a.e. disjoint. Now push on that.
Suppose S_g contained a positive-measure set T of overlap values below ½. Two
coordinates taking values in T sum to less than 1, so such states are not excluded by
∑ᵢ sᵢ = 1 — and at N ≥ 3 there is a third coordinate free to absorb the remainder, so they
occur with positive measure. Any such state lies in Aⱼ ∩ Aₖ, contradicting disjointness.
Conclusion: g vanishes a.e. below ½. The N = 2 solution 4(2s−1)₊ is supported exactly on
(½, 1], so the bound is sharp and attained.
The state-abundance input is taken as an explicit hypothesis (hjoint) rather than derived,
because deriving it is the Dirichlet pushforward of μ_FS — real work, and orthogonal to the
argument. What makes this worth stating that way is joint_degenerate_of_sum_eq_one below:
the hypothesis fails at N = 2, and that failure is exactly the qubit's escape route.
The cap bound. If two overlap coordinates can jointly take values in any positive-measure
set below ½, then the preparation density vanishes almost everywhere below ½.
Why the qubit escapes. When two overlap coordinates are complementary — sⱼ + sₖ = 1,
which is forced at N = 2 because the two Born weights exhaust the state — they can never both
lie below ½. So the abundance hypothesis of cap_of_joint_nondegenerate fails identically, and
no cap bound follows.
This is not a technicality: it is the structural reason N = 2 admits a base-only density at all.
At N ≥ 3 the coordinates stop being functionally dependent, a third one is free to absorb the
remainder, and the escape closes.
The reduction, assembled. Under the hypotheses of step one plus joint non-degeneracy of two
overlap coordinates, a base-only U(N)-covariant non-negative preparation density is confined to
overlap values ≥ ½ — up to a null set — while still having to integrate to 1.
Together with sum_measure_overlapSupport_le_one this is a genuine squeeze on any N ≥ 3
construction: the density lives on a set of measure ≤ 1/n and only where the overlap exceeds
½. It is not yet a contradiction; see the module header for the two steps that remain.
Step four: orthogonal preparations, and the (n−1)/n support bound #
Steps one to three used only the n basis-vector preparations. The first genuinely
generic-ψ input is the orthogonal one: whenever ψ ⊥ eᵢ the Born weight |⟨eᵢ|ψ⟩|²
is zero, so the same non-negativity argument applies — g ∘ sψ must vanish a.e. on Ωᵢ.
What makes this stronger than the basis-vector case is that there are many such ψ, and the
overlap values they realise at a given φ sweep an entire interval. For unit ψ ⊥ eᵢ, the
overlap |⟨ψ|φ⟩|² is maximised at the normalised projection of φ into eᵢ^⊥, with value
1 − sᵢ(φ); tilting ψ within eᵢ^⊥ scales it continuously down to 0. That tilt needs
dim eᵢ^⊥ ≥ 2, i.e. n ≥ 3 — at n = 2 the orthocomplement is a line, ψ is unique up to
phase, and only the single value 1 − sᵢ(φ) is realised. The same threshold, for the third
independent reason.
So for n ≥ 3: a.e. φ ∈ Ωᵢ forces g ≡ 0 on the whole interval [0, 1 − sᵢ(φ)]. Since the
regions cover, a.e. φ has some i with g ≡ 0 on [0, 1 − sᵢ(φ)], and maxᵢ sᵢ(φ) can be
made arbitrarily close to 1/n on a positive-measure set — so g vanishes below (n−1)/n.
At n = 2 that reads g = 0 below ½, which is exactly where 4(2s−1)₊ is supported. The
bound is sharp at the one dimension where a solution is known.
Orthogonal-preparation confinement. If a family of preparations all give outcome i
zero Born weight, then on Ωᵢ the density vanishes at every overlap value any of them realises.
Only the non-negativity of g and the vanishing of the Born weight are used, so this is the
basis-vector argument of step one applied to a much larger family — the first step that uses
preparations other than the eⱼ.
The interval form. If, at almost every x ∈ Ω, the realised overlap values are dense in
[0, r x] and g is continuous, the vanishing extends from those values to the whole interval.
The density hypothesis is the geometric input: for ψ ranging over the unit sphere of eᵢ^⊥,
the overlaps |⟨ψ|φ⟩|² sweep [0, 1 − sᵢ(φ)] — available exactly when dim eᵢ^⊥ ≥ 2, i.e.
n ≥ 3.
Step five: the (n−1)/n support bound #
Step four gives, for a.e. φ, an outcome i with g ≡ 0 on [0, 1 − sᵢ(φ)]. To make that a
statement about g alone, take φ as balanced as possible: the smaller maxᵢ sᵢ(φ), the
longer the interval. Since ∑ᵢ sᵢ = 1 forces maxᵢ sᵢ ≥ 1/n, the best available interval is
[0, 1 − 1/n], and states arbitrarily close to the barycentre occur with positive measure.
The step is short because step four's conclusion is pointwise in g — g vanishes on a whole
interval, for a.e. φ. g is a fixed function, so one suitable φ suffices; no almost-
everywhere bookkeeping survives into the conclusion.
A positive-measure set meets any almost-everywhere property.
★ The (n−1)/n support bound. A base-only preparation density vanishes on every overlap
value below (n−1)/n.
hvan is what step four delivers (each state lies in some outcome region, and there g dies on
[0, 1 − sᵢ]); hbalanced says states with all overlaps below c are not negligible, for any
c above the forced minimum 1/n.
At n = 2 the bound reads "g vanishes below ½", which is exactly the support of the known
solution 4(2s−1)₊ — sharp at the one dimension where a solution exists.