The entropy ledger: carrier erosion prices coarse entropy production

(§Q Q4)

Category: 6-Empirical-CSD (the CSD reading of stroboscopic dynamics; specs/BACKLOG.md §Q Q4, the H7 follow-up).

Fine-grained entropy is constant — measure preservation is the floor everywhere in this corpus. So whatever "entropy production" accompanies record erosion must be coarse: an artefact of reading the record register through a partition. This module makes that ledger precise and prices it, framed strictly as retrodiction reliability — every quantity is a present-tense measure of a present-tense set.

The three quantities and how they chain

• retrodictionSuccess Φ ρ n — the set where reading the register now (period n) and asserting "this was the formation value" is correct. Reliability is its measure. It contains recordIntact n (a register that never moved certainly retrodicts), so the §H half-life bound prices it: ★ measure_retrodictionSuccess_compl_le — retrodiction fails on measure at most n · ε, with ε the per-step coupling μ (recordFlip Φ ρ).
• erosionFraction μ Φ ρ n — the eroded fraction μ (recordIntact n)ᶜ as a real number. It starts at 0 (erosionFraction_zero), never decreases (erosionFraction_monotone — the ledger's substrate is one-way, the second-law shape at the register), and is priced linearly (erosionFraction_le).
• ledgerEntropy μ Φ ρ n — the coarse entropy of the two-cell register partition {intact, eroded}: binEntropy (erosionFraction n). It opens at 0 (ledgerEntropy_zero: record formation starts a clean ledger) and ★★ ledgerEntropy_le prices it by the same coupling knob: below the half-filling point, ledgerEntropy n ≤ binEntropy (n · ε). One ε, three readings — reliability, erosion, entropy.

The link to the corpus's entropy

★ vonNeumannEntropy_ledgerState identifies the ledger with the von Neumann entropy of the register's two-cell diagonal state ledgerState e = diag(1 − e, e): the measure-side ledger is the quantity governed by the pinch H-theorem (vonNeumannEntropy_le_pinching, TH2 in Thermo/SecondLaw.lean — cited, not imported). Density credentials are supplied (ledgerState_posSemidef, ledgerState_trace).

The derived instantiation (Q1/Q2 chain closed onto Q4)

For the qubit phase flip, Q2's Duistermaat–Heckman law computed the coupling exactly (deficitKick_phaseFlip_coupling: ε = 1 − δ/2), so both sides land with no free parameter: deficitKick_phaseFlip_reliability (retrodiction fails on at most n·(1 − δ/2)) and deficitKick_phaseFlip_ledger (the ledger fills at most to binEntropy (n·(1 − δ/2))).

Honest scope

No Fano-type converse is claimed (a lower bound on retrodiction error in terms of conditional entropy needs joint-distribution machinery this module does not build), and the two-cell ledger is the register's coarse-graining, not a thermodynamic entropy of anything larger. Note also that retrodictionSuccess may transiently exceed recordIntact (a readout can flip back); the inequalities are stated in the honest direction.

Cross-references: specs/future-work.md, specs/BACKLOG.md §Q (Q4); recordIntact_compl_measure_le (§H), carrier_persistence_window (H7), recordEvent_measure_invariant (the event side that does NOT erode), entropy_production_nonneg (TH2's matrix-side companion).

Retrodiction: read the register now, assert the formation value

def CSD.Empirical.QuantumChaos.retrodictionSuccess {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) (n : ℕ) : Set A

The retrodiction-success set: points where the period-n readout still equals the formation readout, so reading the register now and asserting "this was the recorded value" is correct. Present-tense checkable: membership is a condition on the current state.

Equations

• CSD.Empirical.QuantumChaos.retrodictionSuccess Φ ρ n = {a : A | ρ (Φ^[n] a) = ρ a}

@[simp]

theorem CSD.Empirical.QuantumChaos.retrodictionSuccess_zero {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) : retrodictionSuccess Φ ρ 0 = Set.univ

At formation (n = 0) retrodiction is certain.

theorem CSD.Empirical.QuantumChaos.recordIntact_subset_retrodictionSuccess {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) (n : ℕ) : recordIntact Φ ρ n ⊆ retrodictionSuccess Φ ρ n

An intact carrier certainly retrodicts: recordIntact demands the readout never moved through period n, which in particular pins period n itself.

theorem CSD.Empirical.QuantumChaos.recordIntact_zero {A : Type u_1} {V : Type u_2} (Φ : A → A) (ρ : A → V) : recordIntact Φ ρ 0 = Set.univ

At formation nothing is eroded: recordIntact 0 is everything.

theorem CSD.Empirical.QuantumChaos.measure_retrodictionSuccess_compl_le {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} {Φ : A → A} {ρ : A → V} (hΦ : MeasureTheory.MeasurePreserving Φ μ μ) (hD : MeasurableSet (recordFlip Φ ρ)) (n : ℕ) : μ (retrodictionSuccess Φ ρ n)ᶜ ≤ n • μ (recordFlip Φ ρ)

★ Retrodiction reliability is priced by the coupling: under a measure-preserving step, reading the register at period n retrodicts the formation value except on measure at most n · ε, where ε is the per-step record-sector coupling. The half-life bound (recordIntact_compl_measure_le), rerouted through recordIntact_subset_retrodictionSuccess.

The erosion fraction: the ledger's one-way substrate

noncomputable def CSD.Empirical.QuantumChaos.erosionFraction {A : Type u_1} {V : Type u_2} [MeasurableSpace A] (μ : MeasureTheory.Measure A) (Φ : A → A) (ρ : A → V) (n : ℕ) : ℝ

The erosion fraction: the measure of the eroded set (recordIntact n)ᶜ, as a real number. The scalar the ledger is a function of.

Equations

• CSD.Empirical.QuantumChaos.erosionFraction μ Φ ρ n = (μ (CSD.Empirical.QuantumChaos.recordIntact Φ ρ n)ᶜ).toReal

@[simp]

theorem CSD.Empirical.QuantumChaos.erosionFraction_zero {A : Type u_1} {V : Type u_2} [MeasurableSpace A] (μ : MeasureTheory.Measure A) (Φ : A → A) (ρ : A → V) : erosionFraction μ Φ ρ 0 = 0

The ledger opens empty: erosionFraction 0 = 0.

theorem CSD.Empirical.QuantumChaos.erosionFraction_nonneg {A : Type u_1} {V : Type u_2} [MeasurableSpace A] (μ : MeasureTheory.Measure A) (Φ : A → A) (ρ : A → V) (n : ℕ) : 0 ≤ erosionFraction μ Φ ρ n

The erosion fraction is nonnegative.

theorem CSD.Empirical.QuantumChaos.erosionFraction_le_one {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} [MeasureTheory.IsProbabilityMeasure μ] (Φ : A → A) (ρ : A → V) (n : ℕ) : erosionFraction μ Φ ρ n ≤ 1

For a probability measure the erosion fraction is at most one.

theorem CSD.Empirical.QuantumChaos.erosionFraction_monotone {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} [MeasureTheory.IsFiniteMeasure μ] (Φ : A → A) (ρ : A → V) : Monotone (erosionFraction μ Φ ρ)

★ Erosion is one-way: the eroded fraction never decreases — the second-law shape at the record register, from carrier antitonicity alone (recordIntact_antitone; no dynamics hypothesis beyond finiteness of the measure). Contrast the event side, which does not erode at all (recordEvent_measure_invariant).

theorem CSD.Empirical.QuantumChaos.erosionFraction_le {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} [MeasureTheory.IsFiniteMeasure μ] {Φ : A → A} {ρ : A → V} (hΦ : MeasureTheory.MeasurePreserving Φ μ μ) (hD : MeasurableSet (recordFlip Φ ρ)) (n : ℕ) : erosionFraction μ Φ ρ n ≤ ↑n * (μ (recordFlip Φ ρ)).toReal

Erosion is priced linearly by the per-step coupling: the real-number form of the half-life bound.

The ledger: two-cell coarse entropy, priced by the same knob

noncomputable def CSD.Empirical.QuantumChaos.ledgerEntropy {A : Type u_1} {V : Type u_2} [MeasurableSpace A] (μ : MeasureTheory.Measure A) (Φ : A → A) (ρ : A → V) (n : ℕ) : ℝ

The entropy ledger: the coarse (Shannon) entropy of the two-cell register partition {intact, eroded} at period n. All entropy here is coarse — the fine-grained entropy is constant because the dynamics preserves the measure.

Equations

• CSD.Empirical.QuantumChaos.ledgerEntropy μ Φ ρ n = Real.binEntropy (CSD.Empirical.QuantumChaos.erosionFraction μ Φ ρ n)

@[simp]

theorem CSD.Empirical.QuantumChaos.ledgerEntropy_zero {A : Type u_1} {V : Type u_2} [MeasurableSpace A] (μ : MeasureTheory.Measure A) (Φ : A → A) (ρ : A → V) : ledgerEntropy μ Φ ρ 0 = 0

Record formation opens a clean ledger: ledgerEntropy 0 = 0.

theorem CSD.Empirical.QuantumChaos.ledgerEntropy_nonneg {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} [MeasureTheory.IsProbabilityMeasure μ] (Φ : A → A) (ρ : A → V) (n : ℕ) : 0 ≤ ledgerEntropy μ Φ ρ n

The ledger is nonnegative (the erosion fraction lies in [0, 1] for a probability measure).

theorem CSD.Empirical.QuantumChaos.ledgerEntropy_le {A : Type u_1} {V : Type u_2} [MeasurableSpace A] {μ : MeasureTheory.Measure A} [MeasureTheory.IsProbabilityMeasure μ] {Φ : A → A} {ρ : A → V} (hΦ : MeasureTheory.MeasurePreserving Φ μ μ) (hD : MeasurableSet (recordFlip Φ ρ)) {n : ℕ} (hn : ↑n * (μ (recordFlip Φ ρ)).toReal ≤ 2⁻¹) : ledgerEntropy μ Φ ρ n ≤ Real.binEntropy (↑n * (μ (recordFlip Φ ρ)).toReal)

★★ The ledger is priced by the same coupling knob: below the half-filling point (n · ε ≤ 1/2), the coarse entropy of the register partition after n periods is at most binEntropy (n · ε) — the same per-step coupling ε that prices retrodiction reliability (measure_retrodictionSuccess_compl_le) bounds how far the entropy ledger can fill. One knob, three readings: reliability, erosion, entropy.

The register's coarse state: the ledger is a von Neumann entropy

noncomputable def CSD.Empirical.QuantumChaos.ledgerState (e : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The register's two-cell coarse state: the diagonal density with weights (1 − e, e) — kept mass on the intact cell, eroded mass on its complement.

Equations

• CSD.Empirical.QuantumChaos.ledgerState e = Matrix.diagonal fun (i : Fin 2) => ↑(![1 - e, e] i)

theorem CSD.Empirical.QuantumChaos.ledgerState_isHermitian (e : ℝ) : (ledgerState e).IsHermitian

The register state is Hermitian (real diagonal).

theorem CSD.Empirical.QuantumChaos.ledgerState_trace (e : ℝ) : (ledgerState e).trace = 1

The register state has unit trace.

theorem CSD.Empirical.QuantumChaos.ledgerState_posSemidef {e : ℝ} (h0 : 0 ≤ e) (h1 : e ≤ 1) : (ledgerState e).PosSemidef

The register state is positive semidefinite for e ∈ [0, 1].

theorem CSD.Empirical.QuantumChaos.vonNeumannEntropy_ledgerState (e : ℝ) : QuantumInfo.vonNeumannEntropy ⋯ = Real.binEntropy e

★ The ledger is a von Neumann entropy: the two-cell coarse entropy equals S(diag(1 − e, e)) — the measure-side ledger is exactly the quantity the pinch H-theorem (vonNeumannEntropy_le_pinching, TH2) governs on the matrix side.

The derived instantiation: the phase flip, with no free parameter

instance CSD.Empirical.QuantumChaos.instIsProbabilityMeasureRecordCircleVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

The unit circle's volume is a probability measure (RecordCircle is AddCircle 1, total mass 1).

theorem CSD.Empirical.QuantumChaos.deficitKick_phaseFlip_reliability (V : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) (p₀ : LF4.CPN 2) {δ : ℝ} (hδ0 : 0 < δ) {kick : RecordCircle} (hkick : kick ≠ 0) (n : ℕ) : ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀).prod MeasureTheory.volume) (retrodictionSuccess (deficitTriggeredKick V phaseFlipW δ kick) Prod.snd n)ᶜ ≤ n • ENNReal.ofReal (1 - δ / 2)

★ Derived retrodiction reliability (qubit, phase flip): with the coupling computed exactly by the Duistermaat–Heckman law (deficitKick_phaseFlip_coupling), retrodiction from the present register fails on measure at most n · (1 − δ/2) — no free parameter.

theorem CSD.Empirical.QuantumChaos.deficitKick_phaseFlip_ledger (V : ↥(Matrix.unitaryGroup (Fin 2) ℂ)) (p₀ : LF4.CPN 2) {δ : ℝ} (hδ0 : 0 < δ) (hδ2 : δ ≤ 2) {kick : RecordCircle} (hkick : kick ≠ 0) {n : ℕ} (hn : ↑n * (1 - δ / 2) ≤ 2⁻¹) : ledgerEntropy ((Matrix.UnitaryGroup.fubiniStudyMeasure p₀).prod MeasureTheory.volume) (deficitTriggeredKick V phaseFlipW δ kick) Prod.snd n ≤ Real.binEntropy (↑n * (1 - δ / 2))

★ The derived ledger (qubit, phase flip): below half-filling the entropy ledger is at most binEntropy (n · (1 − δ/2)) — erosion, reliability, and entropy production all priced by the single coupling the DH law computed. Closes the Q1 → Q2 → Q4 chain with no free parameter.