SigmaLayer/OnticMarginals: A6 steps 2–3 — ontic reduction maps, and marginal stability

Category: 7-SigmaLayer (Paper C A6 — composite systems).

What this adds

Step 1 (OnticComposite.lean) made non-factorisation a theorem. This file supplies the other half of A6's mathematical content:

• Step 2 — the ontic reduction maps. A composite ray has a density matrix (rayDensity, ray-well-defined, unit trace), and its subsystem marginals are the partial traces (reduceA, reduceB). This is the ontic-level r_S — the map from a point of the composite sector to what a subsystem observer can see of it.
• Step 3 — marginal stability = ontic no-signalling. Under a local unitary on A (the vector action actA, with no Kronecker plumbing):
  • the B-marginal is invariant (reduceB_pointA_invariant) — acting on A changes nothing B can see, at the level of the single ontic point;
  • the A-marginal evolves by conjugation (reduceA_pointA_conj) — the Heisenberg transformation law. Instantiated at the Schrödinger unitaries (reduceB_local_flow_invariant): the local flow of any A-Hamiltonian leaves the B-marginal fixed at every time. That is A6's "marginal stability", and it is the ontic-flow form of the corpus's operational tensorSector_no_signalling.

⚠️ Scope

• These are kinematic identities about the reduction maps under local unitaries; they are exactly what A6's marginal-stability clause asserts, and nothing here claims a new dynamics.
• Step 4 of the plan — dynamical no-signalling through the v0.7.0 measurement layer (a protocol acting on A's register leaves the unconditioned B-marginal unchanged) — is not in this file.
• The maps are defined at the projective level (the base of Σ); the torus fibre plays no role in reduction, so the KSigma form is the composition with Prod.fst and is not separately stated.

References

SigmaLayer/OnticComposite.lean (step 1); Mathlib/LinearAlgebra/Matrix/PartialTrace.lean (traceRight, traceLeft); LF4/ProjectedDynamics.lean (schrodingerUnitary); LF3/Projectors/TensorModel.lean, SigmaLayer/TensorSector.lean (the operational no-signalling this is the ontic form of); specs/reconstruction-status.md §2 (the A6 row).

Step 2: the ray density and its marginals

noncomputable def CSD.RecordLayer.rayDensity {nA nB : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : Matrix (Fin nA × Fin nB) (Fin nA × Fin nB) ℂ

The density matrix of a composite ray: ρ(x,y) = v(x)·conj(v(y))/‖v‖² at the canonical representative. Ray-well-defined (rayDensity_mk), unit trace (rayDensity_trace).

Equations

• CSD.RecordLayer.rayDensity p = Matrix.of fun (x y : Fin nA × Fin nB) => p.rep.ofLp x * star (p.rep.ofLp y) / ↑(‖p.rep‖ ^ 2)

theorem CSD.RecordLayer.rayDensity_ratio_smul {nA nB : ℕ} (c : ℂ) (hc : c ≠ 0) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (x y : Fin nA × Fin nB) : (c • v).ofLp x * star ((c • v).ofLp y) / ↑(‖c • v‖ ^ 2) = v.ofLp x * star (v.ofLp y) / ↑(‖v‖ ^ 2)

The scale-invariance computation behind ray-well-definedness.

theorem CSD.RecordLayer.rayDensity_mk {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (hv : v ≠ 0) : rayDensity (Projectivization.mk ℂ v hv) = Matrix.of fun (x y : Fin nA × Fin nB) => v.ofLp x * star (v.ofLp y) / ↑(‖v‖ ^ 2)

The density is well-defined on rays.

theorem CSD.RecordLayer.normSq_eq_sum_mul_star {ι : Type u_1} [Fintype ι] (w : EuclideanSpace ℂ ι) : ↑(‖w‖ ^ 2) = ∑ x : ι, w.ofLp x * star (w.ofLp x)

‖w‖² as the diagonal sum ∑ₓ w(x)·conj(w(x)) — the casting workhorse for the marginal computations.

theorem CSD.RecordLayer.rayDensity_trace {nA nB : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : (rayDensity p).trace = 1

The ray density has unit trace — it is a genuine state.

noncomputable def CSD.RecordLayer.reduceA {nA nB : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : Matrix (Fin nA) (Fin nA) ℂ

The A-marginal of a composite ray: trace out B.

Equations

• CSD.RecordLayer.reduceA p = (CSD.RecordLayer.rayDensity p).traceRight

noncomputable def CSD.RecordLayer.reduceB {nA nB : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : Matrix (Fin nB) (Fin nB) ℂ

The B-marginal of a composite ray: trace out A.

Equations

• CSD.RecordLayer.reduceB p = (CSD.RecordLayer.rayDensity p).traceLeft

Step 3: local unitaries, and marginal stability

noncomputable def CSD.RecordLayer.actA {nA nB : ℕ} (U : Matrix (Fin nA) (Fin nA) ℂ) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : EuclideanSpace ℂ (Fin nA × Fin nB)

The local A-action on composite vectors: (actA U v)(j,k) = ∑ₐ U j a · v(a,k) — the vector form of U ⊗ 1, with no Kronecker plumbing.

Equations

• CSD.RecordLayer.actA U v = WithLp.toLp 2 fun (jk : Fin nA × Fin nB) => ∑ a : Fin nA, U jk.1 a * v.ofLp (a, jk.2)

@[simp]

theorem CSD.RecordLayer.actA_apply {nA nB : ℕ} (U : Matrix (Fin nA) (Fin nA) ℂ) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (j : Fin nA) (k : Fin nB) : (actA U v).ofLp (j, k) = ∑ a : Fin nA, U j a * v.ofLp (a, k)

theorem CSD.RecordLayer.actA_actA {nA nB : ℕ} (U W : Matrix (Fin nA) (Fin nA) ℂ) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : actA U (actA W v) = actA (U * W) v

theorem CSD.RecordLayer.actA_one {nA nB : ℕ} (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : actA 1 v = v

theorem CSD.RecordLayer.actA_zero {nA nB : ℕ} (U : Matrix (Fin nA) (Fin nA) ℂ) : actA U 0 = 0

theorem CSD.RecordLayer.actA_ne_zero {nA nB : ℕ} {U : Matrix (Fin nA) (Fin nA) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin nA) ℂ) {v : EuclideanSpace ℂ (Fin nA × Fin nB)} (hv : v ≠ 0) : actA U v ≠ 0

theorem CSD.RecordLayer.actA_column_sums {nA nB : ℕ} {U : Matrix (Fin nA) (Fin nA) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin nA) ℂ) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (k k' : Fin nB) : ∑ j : Fin nA, (actA U v).ofLp (j, k) * star ((actA U v).ofLp (j, k')) = ∑ a : Fin nA, v.ofLp (a, k) * star (v.ofLp (a, k'))

★ The workhorse: local sums against a unitary collapse. For UᴴU = 1,

∑ⱼ (actA U v)(j,k) · conj((actA U v)(j,k')) = ∑ₐ v(a,k) · conj(v(a,k'))

for every pair of B-indices — the invariance computation behind both the norm and the B-marginal.

theorem CSD.RecordLayer.actA_row_sums {nA nB : ℕ} (U : Matrix (Fin nA) (Fin nA) ℂ) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) (j j' : Fin nA) : ∑ k : Fin nB, (actA U v).ofLp (j, k) * star ((actA U v).ofLp (j', k)) = ∑ a : Fin nA, ∑ b : Fin nA, U j a * star (U j' b) * ∑ k : Fin nB, v.ofLp (a, k) * star (v.ofLp (b, k))

The bilinear expansion of a row sum — no unitarity needed.

theorem CSD.RecordLayer.norm_actA {nA nB : ℕ} {U : Matrix (Fin nA) (Fin nA) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin nA) ℂ) (v : EuclideanSpace ℂ (Fin nA × Fin nB)) : ‖actA U v‖ = ‖v‖

Local unitaries preserve the composite norm.

noncomputable def CSD.RecordLayer.pointA {nA nB : ℕ} {U : Matrix (Fin nA) (Fin nA) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin nA) ℂ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))

The local action on composite rays.

Equations

• CSD.RecordLayer.pointA hU p = Projectivization.mk ℂ (CSD.RecordLayer.actA U p.rep) ⋯

theorem CSD.RecordLayer.reduceB_pointA_invariant {nA nB : ℕ} {U : Matrix (Fin nA) (Fin nA) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin nA) ℂ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : reduceB (pointA hU p) = reduceB p

★★ Marginal stability = ontic no-signalling. A local unitary on A leaves the B-marginal of the composite ray unchanged: acting on A changes nothing B can see, at the level of the single ontic point. This is Paper C A6's marginal-stability clause, and the ontic form of the corpus's operational tensorSector_no_signalling.

theorem CSD.RecordLayer.reduceA_pointA_conj {nA nB : ℕ} {U : Matrix (Fin nA) (Fin nA) ℂ} (hU : U ∈ Matrix.unitaryGroup (Fin nA) ℂ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : reduceA (pointA hU p) = U * reduceA p * star U

The A-marginal evolves by conjugation — the Heisenberg transformation law for the reduction map.

theorem CSD.RecordLayer.reduceB_local_flow_invariant {nA nB : ℕ} [NeZero nA] {HA : Matrix (Fin nA) (Fin nA) ℂ} (hHA : HA.IsHermitian) (t : ℝ) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin nA × Fin nB))) : reduceB (pointA ⋯ p) = reduceB p

★★ Marginal stability under local flows. The Schrödinger flow of any A-Hamiltonian leaves the B-marginal fixed at every time — A6's marginal-stability clause in flow form, the ontic no-signalling statement.