SigmaLayer/OnticComposite: A6 step 1 — the Segre embedding, and non-factorisation as a theorem #
Category: 7-SigmaLayer (Paper C A6 — composite systems).
What A6's "non-factorising composite" means, made sharp #
Paper C A6 says the composite ontic sector is not the product of the subsystem sectors — that is where entanglement lives. The sharp Lean form: the Segre embedding
segre : ℙ(ℂ^{n_A}) × ℙ(ℂ^{n_B}) → ℙ(ℂ^{n_A × n_B}), ([u], [v]) ↦ [u ⊗ v]
is injective but not surjective whenever both factors have dimension ≥ 2. Injectivity says the product-state manifold sits faithfully inside the composite sector; non-surjectivity — witnessed by a Bell-type vector — says the composite sector strictly exceeds it:
Σ_AB ⊋ image (Σ_A × Σ_B).
That is A6's non-factorisation claim as a machine-checked theorem rather than an architectural remark.
⚠️ Honest scope #
- This is the witness-level A6 content. The corpus constructs the composite sector from the
composite Hilbert space; A6-as-philosophy ("
Σ_ABis primitive, not built from anything") is not a formalisation target and is not claimed. - Steps 2–3 of the A6 plan — ontic reduction maps via
partialTrace, and marginal stability under local flows (ontic no-signalling) — are not in this file. Measure statements are not attemptedSUPERSEDED 2026-08-21 (Q28 item 2): the topological half is now here — ★segre_range_isClosed(the product rays are a closed, hence measurable, set), the reusable minor criterionnot_mem_range_segre, and ★exists_entangled_mem_nhds(entangled rays in every open neighbourhood of every product ray). The measure half — the Fubini–Study weight of the entangled complement is positive, globally and in every open neighbourhood of a product ray — isRecordLayer/EntangledMeasure.lean. What is still NOT proved is the μ_FS-NULL strengthening ("almost every composite state is entangled"): that is research-gated on Mathlib-scale inputs (MATHLIB-GAPS.md, polynomial zero sets).
References #
Mathlib/QuantumInfo/JointRegister.lean (tensorState and its API — the product vector u ⊗ v,
tensorState_ne_zero, tensorState_smul_smul, tensorState_continuous — which this file's Segre
embedding is built from); LF3/Projectors/TensorModel.lean, LF6/GisinTheorem.lean (the corpus's
operational entanglement); specs/reconstruction-status.md §2 (the A6 row this addresses);
specs/BACKLOG.md.
The Segre embedding #
The Segre embedding: the pair of subsystem rays ([u], [v]) goes to the composite ray
[u ⊗ v]. Defined through representatives; segre_mk is the working form.
Equations
- CSD.RecordLayer.segre p = Projectivization.mk ℂ (QuantumInfo.tensorState p.1.rep p.2.rep) ⋯
Instances For
The Segre embedding on representatives.
The Segre embedding is injective: product rays remember their factors.
Non-surjectivity: the Bell-type witness #
The Bell-type vector e₀⊗e₀ + e₁⊗e₁ (unnormalised), defined whenever both factors have
dimension ≥ 2.
Equations
Instances For
★ The Segre embedding is NOT surjective: the Bell ray is not a product ray.
If u ⊗ v = c • bell with c ≠ 0, the four corner coordinates give u₀v₀ = c, u₁v₁ = c,
u₀v₁ = 0, u₁v₀ = 0 — and (u₀v₀)(u₁v₁) = c² ≠ 0 = (u₀v₁)(u₁v₀) is a contradiction. So
Σ_AB ⊋ image (Σ_A × Σ_B)
whenever both factors have dimension ≥ 2: the composite sector strictly exceeds the product of the subsystem sectors. Paper C A6's non-factorisation, as a theorem.
Topology of the Segre image (Q28 item 2a) #
The Segre embedding is continuous — descended through the open quotient maps
mk' on both factors — so its range, the continuous image of a compact space,
is closed. That measurability-grade fact is what the measure tier
(RecordLayer/EntangledMeasure.lean) consumes.
The Segre embedding is continuous. Continuity descends through the open
quotient maps mk' on both factors (IsOpenQuotientMap.prodMap), where the
composite is mk' of the continuous nonvanishing QuantumInfo.tensorState.
★ The Segre image is closed (Q28 item 2a): the continuous image of the compact product of projective spaces, in a Hausdorff target. In particular the set of product rays is measurable and its complement — the entangled rays — is open.
The minor criterion (the reusable rank obstruction) #
A ray is a product ray only if its coefficient matrix w (j, k) has all 2×2
minors equal — the rank-one condition. The contrapositive is the reusable
entanglement witness: one unequal minor puts a ray outside the Segre image.
segre_not_surjective's Bell computation is the special case
(j,k,j',k') = (0,0,1,1).
Membership in the Segre image forces every 2×2 minor of the coefficient
matrix to balance: w (j,k) · w (j',k') = w (j,k') · w (j',k).
The entanglement witness, reusable form: one unbalanced 2×2 minor
puts a ray outside the Segre image.
Entangled rays are dense near every product ray (Q28 item 2b) #
The path t ↦ [a ⊗ b + t · e_{(j₁,k₁)}] is continuous, lands on the product
ray at t = 0, and for t ≠ 0 fails the minor criterion at the corner
(j₀, j₁, k₀, k₁) — a single standard-basis perturbation, no orthogonal
complements needed.
★ Entangled rays in every neighbourhood of every product ray (Q28 item 2b, topological form): whenever both factors have dimension ≥ 2, every open set containing a product ray also contains a ray outside the Segre image.