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 #
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.
Product vectors #
The product (Kronecker) vector u ⊗ v: coordinates (u ⊗ v)(j,k) = u j · v k.
Equations
- CSD.RecordLayer.prodVec u v = WithLp.toLp 2 fun (jk : Fin nA × Fin nB) => u.ofLp jk.1 * v.ofLp jk.2
Instances For
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 ℂ (CSD.RecordLayer.prodVec 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 product-vector map is (jointly) continuous.
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 prodVec.
★ 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.