RecordLayer/NStepChain: the measurement chain to arbitrary depth

Category: 7-SigmaLayer (the record layer).

The corpus proves one step (globalBasin_prob, csd_sequential_born) and two steps (two_stage_joint). The programme's account of measurement is the chain to arbitrary depth, and until now that was an argument rather than a theorem. This module makes it a theorem, at the level where the argument actually lives: the sequence of record-layer states.

The content, which is self-similarity

After a record i, the state is the vertex vertexPoint i — that is the collapse, and it is what makes the chain repeat. So the state entering step k+1 is a function of the previous record alone, never of the preparation or of the earlier records:

• chainState — chainState p i 0 = p, and chainState p i (k+1) = vertexPoint (i k).
• ★ chainState_succ — the reset, as a lemma rather than an unfolding.

The chain law is then a product of per-step rates read at those states:

• ★★ csd_nstep_born — for every depth n, every sequence of context fields and every sequence of outcomes, the product of the per-step basin measures equals ENNReal.ofReal of the product of the per-step rates. Induction on n; the step is globalBasin_prob at chainState.
• ★ csd_nstep_born_succ — the recursion in the form the programme states it: depth n+1 is the first rate times the depth-n chain at the collapsed vertex.
• ★ csd_twostep_born — the n = 2 instance, so the general theorem is visibly the two-step law the corpus already had.
• ★ csd_nstep_repeatable — non-vacuity with teeth: measuring the same basis repeatedly reproduces the first outcome with probability one at every depth, because the vertex rate is an indicator.

⚠️ What the bank family is doing, and what this does not claim

One measurement consumes one bank, so a depth-n chain is an n-bank construction and the posit is renewed at each step (specs/POSITS.md Posit 5; the external review's Posit 2). That renewal is exactly what chainState encodes: each step is prepared afresh at epistemicMeasure (chainState …), with a fresh register and a fresh bank. The theorem is conditional on the bank family in that sense, and the hypothesis is visible in the statement as the per-step epistemicMeasure rather than hidden in a structure field.

⚠️ This is the chain at the level of record-layer states, not a single-arena factorisation. two_stage_joint (RecordLayer/TwoTimeLuders.lean) does something different and harder for n = 2: it factors the joint probability inside one two-stage arena, with the stage-2 apparatus explicitly adjoined. Generalising that construction to an n-stage arena is a separate and larger piece of work, and it is not done here. What is proved here is the law the chain obeys once each step is granted its own bank; what is not proved is that an n-stage arena assembles to give it.

References

RecordLayer/GlobalBasin.lean (epistemicMeasure, globalBasin, globalBasin_prob, ContextField); RecordLayer/SwapLuders.lean (vertexPoint, momentMap_vertex); RecordLayer/TwoTimeLuders.lean (two_stage_joint, the single-arena two-stage factorisation); Empirical/CSD/SequentialMeasurement.lean (csd_sequential_born, csd_repeatability); specs/POSITS.md (Posit 5, the calibrated bank); specs/future-work.md.

noncomputable def CSD.RecordLayer.chainState {N : ℕ} (p : LF4.CPN N) (i : ℕ → Fin N) : ℕ → LF4.CPN N

The state entering step k of the chain: the preparation at step 0, and thereafter the vertex named by the previous record. This is the collapse, written as data.

Equations

• CSD.RecordLayer.chainState p i 0 = p
• CSD.RecordLayer.chainState p i k.succ = CSD.RecordLayer.vertexPoint (i k)

@[simp]

theorem CSD.RecordLayer.chainState_zero {N : ℕ} (p : LF4.CPN N) (i : ℕ → Fin N) : chainState p i 0 = p

@[simp]

theorem CSD.RecordLayer.chainState_succ {N : ℕ} (p : LF4.CPN N) (i : ℕ → Fin N) (k : ℕ) : chainState p i (k + 1) = vertexPoint (i k)

★ The reset. The state entering step k+1 depends on the previous record alone — not on the preparation, and not on the records before it. This is why the chain repeats.

theorem CSD.RecordLayer.chainState_shift {N : ℕ} (p : LF4.CPN N) (i : ℕ → Fin N) (k : ℕ) : chainState (vertexPoint (i 0)) (fun (m : ℕ) => i (m + 1)) k = chainState p i (k + 1)

★ The tail of a chain is a chain. Re-rooting at the first record's vertex and shifting the outcome sequence reproduces the original states from step one on. This is chainState_succ in the form the induction needs, where the equation sits under a binder and rfl will not reach it.

noncomputable def CSD.RecordLayer.chainRate {N : ℕ} (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) (n : ℕ) : ℝ

The chain rate to depth n: the product of the per-step rates, each read at the state that step actually sees.

Equations

• CSD.RecordLayer.chainRate p c i n = ∏ k ∈ Finset.range n, (c k).rate (CSD.RecordLayer.chainState p i k) (i k)

@[simp]

theorem CSD.RecordLayer.chainRate_zero {N : ℕ} (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) : chainRate p c i 0 = 1

theorem CSD.RecordLayer.chainRate_nonneg {N : ℕ} (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) (n : ℕ) : 0 ≤ chainRate p c i n

theorem CSD.RecordLayer.csd_nstep_born {N : ℕ} (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) (n : ℕ) : ∏ k ∈ Finset.range n, (epistemicMeasure (chainState p i k)) (globalBasin (c k) (i k)) = ENNReal.ofReal (chainRate p c i n)

★★ The measurement chain to arbitrary depth. For every depth, every sequence of context fields and every sequence of outcomes, the product of the per-step basin measures is the product of the per-step rates.

Each factor is globalBasin_prob at the state that step sees, and the states are given by chainState: the preparation first, the collapsed vertex thereafter. The bank family enters as the per-step epistemicMeasure — one measurement, one bank (specs/POSITS.md Posit 5).

theorem CSD.RecordLayer.csd_nstep_born_succ {N : ℕ} (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) (n : ℕ) : chainRate p c i (n + 1) = (c 0).rate p (i 0) * chainRate (vertexPoint (i 0)) (fun (k : ℕ) => c (k + 1)) (fun (k : ℕ) => i (k + 1)) n

★ The recursion, in the form the programme states it. A depth-n+1 chain is the first step's rate times a depth-n chain at the collapsed vertex: the tail of a chain is a chain.

theorem CSD.RecordLayer.csd_twostep_born {N : ℕ} (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) : (epistemicMeasure p) (globalBasin (c 0) (i 0)) * (epistemicMeasure (vertexPoint (i 0))) (globalBasin (c 1) (i 1)) = ENNReal.ofReal ((c 0).rate p (i 0) * (c 1).rate (vertexPoint (i 0)) (i 1))

★ The two-step instance. The general theorem specialised to n = 2, so it is visible that the depth-n law is the two-step law the corpus already had, extended rather than replaced. ⚠️ This is the state-level statement; two_stage_joint proves the harder single-arena factorisation for two steps.

theorem CSD.RecordLayer.csd_nstep_repeatable {N : ℕ} (p : LF4.CPN N) (i₀ : Fin N) (n : ℕ) : chainRate p (fun (x : ℕ) => momentContext N) (fun (x : ℕ) => i₀) (n + 1) = (momentContext N).rate p i₀

★ Repeatability at every depth. Measure the computational basis, record i 0, then measure it again at every later step: the chain reproduces i 0 with probability one, to arbitrary depth.

Non-vacuity with teeth — the vertex rate is an indicator (momentMap_vertex), so the product of the tail rates is 1 and the chain does not decay.