Q28 item 2: entangled rays carry positive Fubini–Study weight #
Category: 7-SigmaLayer (Paper C A6, the measure tier; BACKLOG Q28,
specs/c2-support-plan.md item 2 — the C2-blocking item).
OnticComposite.lean delivers the topology: the Segre image (the product rays)
is closed, and entangled rays exist in every open neighbourhood of every
product ray. This module adds the measure conclusions the C2 argument runs on:
compositeFubiniStudy— the Fubini–Study measure read on the composite indexFin nA × Fin nB: the pushforward offubiniStudyMeasurealong the canonical index reindexing (finProdFinEquiv, as a linear isometry of Euclidean spaces descended to rays). A probability measure; positive on nonempty opens (compositeFubiniStudy_pos_of_isOpen).- ★★
compositeFubiniStudy_entangled_pos_global— the entangled rays carry positive preparation weight: the complement of the Segre image is open (2a) and nonempty (segre_not_surjective), hence has nonzero measure. - ★★
compositeFubiniStudy_entangled_pos— the local form C2's contradiction runs on: every open neighbourhood of a product ray meets the entangled complement in a set of positive measure. A product-supported law assigns that set measure zero, so no product law reproduces the composite preparation weights — and the discrepancy set is defined without reference to any coordinatisation.
⚠️ Scope: the statements are TOPOLOGICAL-neighbourhood forms — ℙ carries no
metric in Mathlib or in this corpus, so "every ε-ball" is not statable today
(MATHLIB-GAPS.md, Fubini–Study metric row). The μ_FS-NULL strengthening
("almost every composite ray is entangled") is research-gated on Mathlib-scale
inputs (MATHLIB-GAPS.md, polynomial zero sets); the positive form here
carries the C2 argument.
References #
specs/c2-support-plan.md (Q28 scoping, item 2);
RecordLayer/OnticComposite.lean (segre, segre_range_isClosed,
exists_entangled_mem_nhds, not_mem_range_segre);
LF4/TypicalityForcing.lean (fubiniStudyMeasure_pos_of_isOpen);
Mathlib/LinearAlgebra/Projectivization/FubiniStudy.lean
(fubiniStudyMeasure); specs/BACKLOG.md (Q28); specs/future-work.md.
The index reindexing, descended to rays #
The canonical index reindexing Fin nA × Fin nB ≃ Fin (nA * nB) as a
linear isometry equivalence of Euclidean spaces.
Equations
Instances For
Composite rays, read on the flat Fin (nA * nB) index.
Equations
Instances For
Flat-index rays, read back on the composite Fin nA × Fin nB index.
Equations
Instances For
Reading a composite ray flat and back is the identity.
The flat-to-composite reading is surjective.
The composite Fubini–Study measure #
The Fubini–Study measure on the composite index: the pushforward of
fubiniStudyMeasure at p₀ along the flat-to-composite ray reading. The
composite ray space is the flat ℂℙ^{nA·nB−1} up to the canonical index
bijection, and this is THE Fubini–Study measure carried across it.
Equations
Instances For
The composite Fubini–Study measure has full support: every nonempty
open set has positive measure. Transports
fubiniStudyMeasure_pos_of_isOpen along the reindexing (preimages of opens
are open by continuity, and nonempty by surjectivity).
The entangled rays carry positive weight (Q28 items 2c₀ and 2c) #
The Segre image is a measurable set (it is closed).
★★ Entangled rays carry positive preparation weight (the global form):
whenever both factors have dimension ≥ 2, the complement of the Segre image —
the entangled rays — has nonzero composite Fubini–Study measure. Open by
segre_range_isClosed, nonempty by segre_not_surjective.
★★ The local form C2's contradiction runs on: every open neighbourhood of a product ray meets the entangled complement in a set of positive composite Fubini–Study measure. A product-supported law gives this set measure zero, so no product law reproduces the composite preparation weights.
★★ Almost every composite state is entangled (MG-2, 2026-08-22) #
The positive-measure statements above say the entangled rays are not negligible. This upgrades
them to the sharp form: the PRODUCT rays are null, so a Fubini–Study-typical composite state is
entangled. The route is Matrix.UnitaryGroup.fubiniStudyMeasure_null_of_cone
(Mathlib/LinearAlgebra/Projectivization/FubiniStudyLebesgue.lean): Fubini–Study is the
projectivization of a Lebesgue-absolutely-continuous measure, so a ray set whose vector cone is
Lebesgue-null is Fubini–Study-null. The Segre cone sits inside the zero set of ONE coordinate
quadratic — the 2×2 minor segre_minor_eq at the corner (j₀,j₁,k₀,k₁), read through the
index bijection — and that zero set is null by Fubini slicing (pi_quadratic_null'). No
polynomial-zero-set theory is needed.
★★ The product rays are null: for factors of dimension ≥ 2, the Segre image has
composite Fubini–Study measure zero. With compositeFubiniStudy_entangled_pos_global this is
the sharp statement — entanglement is not merely non-negligible but generic.
★★ Almost every composite state is entangled — the a.e. form of
compositeFubiniStudy_range_segre_null. The C2 headline, upgraded from "the entangled set has
positive measure" to "the product set is null".