SigmaLayer/ShearWitness: a concrete de-isolating interaction (item 3)

Category: 7-SigmaLayer (the record layer — the dynamical witness).

What this is

The first concrete measurement witness: an explicit propagator on Σ_sel × T²_R that takes an apparatus-ready pointer into a pointer displaying the outcome the hidden selector had already fixed. It discharges both standing hypotheses of the interface — CorrelatesOn and PointerInvariantOn — so neither is assumed here.

The physics: the von Neumann shear

Couple the selector's outcome-index observable ι to the pointer momentum,

H_int(t) = g(t) · (ι(x_sel) + 1) · δ · p_R

Hamilton's equations give q̇_R = g(t)(ι+1)δ, ṗ_R = 0, and — the point — ẋ_sel ∝ ∇ι = 0 almost everywhere, because ι is locally constant off the seams between selector sectors. So the coupling translates the pointer at an outcome-dependent rate and does not disturb the selector, except exactly on the measure-zero seam.

★ That is where no_everywhere_correlation said the exceptional set had to live. The constraint predicted the location of the singularity before the construction existed, and the construction puts it there. Two independent routes agreeing is the reason to believe this is the right shape.

Design choices, and why each is forced

• Shifts of (i+1)·δ, not i·δ. With i·δ the outcome-0 region would be the ready region, breaking ready_disjoint_pointer and letting "no record" masquerade as a record. The +1 is what keeps readout_ready_eq_none true.
• g switched off after T_M. This is why the interface uses a two-time propagator rather than a one-parameter group: after readout the propagator is the identity, so PointerInvariantOn is proved, not assumed. A group could not express the switch-off.
• ε = δ/2 with δ = 1/(K+1). Keeps the K pointer arcs and the ready arc pairwise disjoint inside one turn, and — separately — keeps every shifted ready state below 1, so no wraparound occurs and rep is additive on the states that matter (rep_pshift_of_mem).

What is proved

• shearProtocol — a genuine MeasurementProtocol on Σ_sel × T²_R: propagator laws, measurability, disjoint pointer regions, and a ready region disjoint from all of them.
• shear_correlates — CorrelatesOn discharged. Sᵢ × R₀ lands in Bᵢ.
• shear_pointerInvariant — PointerInvariantOn discharged, because the interaction is off.
• shear_measurePreserving — the propagator preserves the Liouville measure. What makes this a dynamics rather than an arbitrary relabelling, and the hypothesis every necessary condition in MeasurementConstraints.lean assumes. A skew product: selector held fixed, each fibre translated by a Haar-preserving shift.
• shear_readout_ready, shear_readout_after — the non-triviality pair: no record before, a unique record after.

⚠️ Honest scope — what this is NOT

1. The Hamiltonian generation is stated, not formalised. The propagator is constructed explicitly and every required property is proved of it. That it is the time-T_M flow of the H_int above is a calculation in symplectic geometry, and Mathlib has no manifold symplectic / Hamiltonian-flow API (reconstruction-status.md §2a, the permanently scoped row). So the plan's "an explicit propagator proved to arise from that Hamiltonian" is half done: explicit propagator yes, proof of Hamiltonian origin no. Do not cite this as a formalised H_int.
2. It is a witness, not a derivation. The coupling is engineered to work. That is what constructing a witness means, and it is the same standard the rest of the corpus's witness models meet — but it does not show that a physically natural interaction must do this.
3. ι is the outcome index. One may object that the apparatus is "coupled to the answer". That objection applies verbatim to the textbook von Neumann coupling H ∝ Â ⊗ p̂, which this is the ontic analogue of. Recorded so the reader can weigh it rather than discover it.
4. Σ_sel is abstract here. The witness needs only a measurable index function, so it is proved at that generality; instantiating ι from globalBasin is a separate step and is not done here.
5. Measure preservation is not proved. RESOLVED — shear_measurePreserving. (An earlier draft of this docstring listed the theorem before it existed; the claim was withdrawn and is now restored because the proof is in.) The witness is therefore known to satisfy the standing hypothesis of every necessary condition in MeasurementConstraints.lean.
6. Not connected to the Born weights. measure_outcomeSector_eq_of_correlates would turn shear_correlates into a dynamical Born statement, but that needs the selector sectors to be globalBasin's and their measures to be the Born weights. Now unblocked by (5), and the remaining work is the instantiation, not a missing ingredient.

References

SigmaLayer/MeasurementProtocol.lean (MeasurementProtocol, CorrelatesOn); SigmaLayer/RecordPersistence.lean (PointerInvariantOn); SigmaLayer/MeasurementConstraints.lean (no_everywhere_correlation — which predicted the seam); SigmaLayer/CircleFibre.lean (rep); LF4/KahlerInstance.lean (KTorus).

Translating the pointer

noncomputable def CSD.RecordLayer.pshift (a : ℝ) (x : LF4.KTorus) : LF4.KTorus

Translate the first torus coordinate by a real amount. The pointer's q; the second coordinate is its symplectic partner and is untouched.

Equations

• CSD.RecordLayer.pshift a x = (x.1 + ↑a, x.2)

@[simp]

theorem CSD.RecordLayer.pshift_zero (x : LF4.KTorus) : pshift 0 x = x

theorem CSD.RecordLayer.pshift_add (a b : ℝ) (x : LF4.KTorus) : pshift a (pshift b x) = pshift (a + b) x

theorem CSD.RecordLayer.continuous_pshift_uncurry : Continuous fun (ar : ℝ × LF4.KTorus) => pshift ar.1 ar.2

theorem CSD.RecordLayer.rep_pshift_of_mem (x : LF4.KTorus) (a : ℝ) (h : rep x.1 + a ∈ Set.Ioc 0 1) : rep (pshift a x).1 = rep x.1 + a

rep is additive under a shift that does not wrap around the circle. The whole reason the region arithmetic below stays on the real line.

Arc measures

volume_circleCell computes the measure of a CDF cell. The witness needs the same fact for arcs specified by arbitrary endpoints, so the general statement is extracted here.

theorem CSD.RecordLayer.volume_repPreimage {a b : ℝ} (h0 : 0 ≤ a) (_hab : a ≤ b) (hb : b ≤ 1) : MeasureTheory.volume (rep ⁻¹' Set.Ioc a b) = ENNReal.ofReal (b - a)

The Haar measure of a circle arc, for endpoints within one turn.

The witness

noncomputable def CSD.RecordLayer.shearWidth (K : ℕ) : ℝ

The arc width ε.

Equations

• CSD.RecordLayer.shearWidth K = 1 / (2 * (↑K + 1))

noncomputable def CSD.RecordLayer.shearGap (K : ℕ) : ℝ

The arc spacing δ.

Equations

• CSD.RecordLayer.shearGap K = 1 / (↑K + 1)

noncomputable def CSD.RecordLayer.shearAmt (K : ℕ) (i : Fin K) : ℝ

The total shift applied to the pointer when the selector reads outcome i.

Equations

• CSD.RecordLayer.shearAmt K i = (↑↑i + 1) * CSD.RecordLayer.shearGap K

noncomputable def CSD.RecordLayer.elapsed (u : ℝ) : ℝ

How much of the interaction has run by time u: the coupling is switched on over [0,1] and off thereafter. This is what makes the propagator two-time rather than a group.

Equations

• CSD.RecordLayer.elapsed u = max 0 (min u 1)

theorem CSD.RecordLayer.elapsed_zero : elapsed 0 = 0

theorem CSD.RecordLayer.elapsed_one : elapsed 1 = 1

theorem CSD.RecordLayer.elapsed_of_one_le {u : ℝ} (hu : 1 ≤ u) : elapsed u = 1

noncomputable def CSD.RecordLayer.readyArc (K : ℕ) : Set LF4.KTorus

The apparatus-ready arc: rep ∈ (0, ε].

Equations

• CSD.RecordLayer.readyArc K = {x : CSD.LF4.KTorus | CSD.RecordLayer.rep x.1 ∈ Set.Ioc 0 (CSD.RecordLayer.shearWidth K)}

noncomputable def CSD.RecordLayer.pointerArc (K : ℕ) (i : Fin K) : Set LF4.KTorus

The pointer arc displaying outcome i.

Equations

• CSD.RecordLayer.pointerArc K i = {x : CSD.LF4.KTorus | CSD.RecordLayer.rep x.1 ∈ Set.Ioc (CSD.RecordLayer.shearAmt K i) (CSD.RecordLayer.shearAmt K i + CSD.RecordLayer.shearWidth K)}

theorem CSD.RecordLayer.measurableSet_readyArc {K : ℕ} : MeasurableSet (readyArc K)

theorem CSD.RecordLayer.measurableSet_pointerArc {K : ℕ} (i : Fin K) : MeasurableSet (pointerArc K i)

Arithmetic of the arcs

theorem CSD.RecordLayer.shearWidth_pos {K : ℕ} : 0 < shearWidth K

theorem CSD.RecordLayer.shearGap_pos {K : ℕ} : 0 < shearGap K

theorem CSD.RecordLayer.shearWidth_lt_gap {K : ℕ} : shearWidth K < shearGap K

theorem CSD.RecordLayer.shearAmt_pos {K : ℕ} (i : Fin K) : 0 < shearAmt K i

theorem CSD.RecordLayer.shearAmt_add_width_le_one {K : ℕ} (i : Fin K) : shearAmt K i + shearWidth K ≤ 1

Every shifted ready state stays below 1: no wraparound.

theorem CSD.RecordLayer.shearAmt_strictMono {K : ℕ} {i j : Fin K} (h : ↑i < ↑j) : shearAmt K i + shearWidth K < shearAmt K j

theorem CSD.RecordLayer.volume_readyArc {K : ℕ} : MeasureTheory.volume (readyArc K) = ENNReal.ofReal (shearWidth K)

The ready arc has positive Haar measure, so conditioning on it is legitimate.

theorem CSD.RecordLayer.volume_readyArc_ne_zero {K : ℕ} : MeasureTheory.volume (readyArc K) ≠ 0

The propagator

noncomputable def CSD.RecordLayer.shearEvolve {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t : SigmaLayer.OnticTime) : Xsel × LF4.KTorus → Xsel × LF4.KTorus

The shear propagator. Over [s,t] the pointer is translated by (elapsed t - elapsed s) · (ι+1)δ; the selector is untouched.

Equations

• CSD.RecordLayer.shearEvolve idx s t x = (x.1, CSD.RecordLayer.pshift ((CSD.RecordLayer.elapsed t - CSD.RecordLayer.elapsed s) * CSD.RecordLayer.shearAmt K (idx x.1)) x.2)

theorem CSD.RecordLayer.shearEvolve_comp' {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (s t u : SigmaLayer.OnticTime) : shearEvolve idx t u ∘ shearEvolve idx s t = shearEvolve idx s u

The shear composes across time, standalone form (also a field of shearProtocol).

theorem CSD.RecordLayer.shearEvolve_frozen {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) {s t : SigmaLayer.OnticTime} (hs : 1 ≤ s) (ht : 1 ≤ t) : shearEvolve idx s t = id

Right of the readout time the shear is frozen: the propagator is the identity.

noncomputable def CSD.RecordLayer.shearProtocol {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) : MeasurementProtocol (Xsel × LF4.KTorus) K

The measurement witness as a MeasurementProtocol.

Equations

• One or more equations did not get rendered due to their size.

Measure preservation

instance CSD.RecordLayer.instIsAddLeftInvariantKTorus : MeasureTheory.volume.IsAddLeftInvariant

Haar measure on the register is translation invariant. Not found by instance search: volume on a product is definitionally the product measure but the invariance instance does not fire through the MeasureSpace instance, so it is supplied here.

theorem CSD.RecordLayer.measurePreserving_pshift (a : ℝ) : MeasureTheory.MeasurePreserving (pshift a) MeasureTheory.volume MeasureTheory.volume

Translating the pointer preserves Haar measure on the register — translation invariance of Haar on the compact group T².

theorem CSD.RecordLayer.shear_measurePreserving {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (μ : MeasureTheory.Measure Xsel) [MeasureTheory.SFinite μ] (s t : SigmaLayer.OnticTime) : MeasureTheory.MeasurePreserving (shearEvolve idx s t) (μ.prod MeasureTheory.volume) (μ.prod MeasureTheory.volume)

★ The shear propagator preserves the Liouville measure.

This is what makes the witness a dynamics rather than an arbitrary relabelling of states, and it is the hypothesis every necessary condition in MeasurementConstraints.lean assumes. A skew product: the selector is held fixed and each fibre is translated by a Haar-preserving shift.

⚠️ The system state does not collapse

theorem CSD.RecordLayer.shear_base_marginal_unchanged {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (μ : MeasureTheory.Measure (Xsel × LF4.KTorus)) (i : Fin K) : MeasureTheory.Measure.map Prod.fst ((shearProtocol idx hidx).postMeasure μ i) = MeasureTheory.Measure.map Prod.fst ((shearProtocol idx hidx).selectedMeasure μ i)

★ The interaction does not change the system's marginal.

Prod.fst ∘ evolve = Prod.fst — the shear moves only the pointer — so the base marginal of the post-measurement ensemble is the base marginal of the selected ensemble. Nothing about the system has moved.

⚠️ This is a genuine limitation of the witness, and it is worth stating rather than burying. It means the shear gives repeatability (re-reading the same observable returns the same outcome — readout_persists_on_interval) but it does not implement the Lüders update: after outcome i the system is still at [ψ], not at [eᵢ]. A subsequent incompatible measurement would therefore see the original preparation, which is not what quantum mechanics predicts.

★ And the tension is structural, not an oversight: the property that makes this witness work — ẋ_sel ∝ ∇ι = 0, no back-reaction on the selector — is exactly the property that prevents collapse. A witness that reproduces Lüders must disturb the selector, and then the clean correlation argument has to be redone. So item 6's Lüders half is not merely unbuilt here; this witness cannot supply it, and a different coupling is required.

def CSD.RecordLayer.selReady {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (i : Fin K) : Set (Xsel × LF4.KTorus)

The selector-and-ready sector for outcome i.

Equations

• CSD.RecordLayer.selReady idx i = {p : Xsel × CSD.LF4.KTorus | idx p.1 = i ∧ p.2 ∈ CSD.RecordLayer.readyArc K}

theorem CSD.RecordLayer.selReady_eq_prod {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) (i : Fin K) : selReady idx i = (idx ⁻¹' {i}) ×ˢ readyArc K

The selector-and-ready sector factors as a product: selector fibre × ready arc.

theorem CSD.RecordLayer.measurableSet_selReady {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (i : Fin K) : MeasurableSet (selReady idx i)

theorem CSD.RecordLayer.selReady_pairwiseDisjoint {Xsel : Type u_1} {K : ℕ} (idx : Xsel → Fin K) : Pairwise (Function.onFun Disjoint (selReady idx))

Distinct selector-and-ready sectors are disjoint: the selector reads one index.

theorem CSD.RecordLayer.shear_correlates {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) : (shearProtocol idx hidx).CorrelatesOn (selReady idx)

★ CorrelatesOn DISCHARGED. The interaction carries a ready pointer, over a selector reading i, into the pointer arc displaying i. This is the correlation theorem the Paper D obligation asks for — here proved of an explicit propagator rather than assumed.

theorem CSD.RecordLayer.shear_pointerInvariant {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) : (shearProtocol idx hidx).PointerInvariantOn

★ PointerInvariantOn DISCHARGED — and for a reason that is physics, not bookkeeping: after the readout time the coupling is switched off, so the propagator is the identity and the record cannot move. A one-parameter group could not have expressed the switch-off; this is what the two-time propagator was for.

theorem CSD.RecordLayer.shear_readout_ready {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) {x : Xsel × LF4.KTorus} (hx : x.2 ∈ readyArc K) : (shearProtocol idx hidx).readout x = none

★ The non-triviality pair. Before the interaction the apparatus reads nothing; after it, it reads exactly the outcome the hidden selector had fixed. Together these rule out an identity flow or a pre-existing label being presented as a created record.

theorem CSD.RecordLayer.shear_readout_after {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) {i : Fin K} {x : Xsel × LF4.KTorus} (hx : x ∈ selReady idx i) : (shearProtocol idx hidx).readout ((shearProtocol idx hidx).evolve 0 1 x) = some i

Externality: the before/after pair

The record-network programme's necessary condition — externality, the outcome information having left the measured system — has a before/after pair on this witness. ⚠️ The "after" half is structurally vacuous here and is recorded as such rather than re-landed as content: the readout reads the register factor only, so the displayed record is invariant under every system-side map by rfl (readout_system_invariant); that is architecture, not physics. The standalone content is the "before" half: prior to the stroke, a system-only transformation changes which outcome gets recorded (outcome_system_dependent_before) — the outcome information is still in the system, and the stroke is what exports it to the register.

theorem CSD.RecordLayer.outcome_system_dependent_before {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) {i j : Fin K} (hij : i ≠ j) {s s' : Xsel} (hs : idx s = i) (hs' : idx s' = j) {q : LF4.KTorus} (hq : q ∈ readyArc K) : (shearProtocol idx hidx).readout ((shearProtocol idx hidx).evolve 0 1 (s, q)) ≠ (shearProtocol idx hidx).readout ((shearProtocol idx hidx).evolve 0 1 (s', q))

★ Before the stroke, the outcome is system-dependent. A system-only change moving the selector across basins changes the record the propagator will create: the outcome information has not yet left the system. The contentful half of the externality pair.

theorem CSD.RecordLayer.readout_system_invariant {Xsel : Type u_1} [MeasurableSpace Xsel] {K : ℕ} (idx : Xsel → Fin K) (hidx : Measurable idx) (f : Xsel → Xsel) (x : Xsel × LF4.KTorus) : (shearProtocol idx hidx).readout (f x.1, x.2) = (shearProtocol idx hidx).readout x

⚠️ The "after" half, vacuous by architecture and recorded so it is not re-landed as content: the readout reads the register factor only, so the displayed record is invariant under every system-side map, definitionally. Externality of a displayed record is a property of the arena's product structure here, not a theorem with content; the contentful half is outcome_system_dependent_before.