Q1: the derived coupling — operator norm → flip measure #
Category: 3-Local (CSD-ontic record layer; specs/BACKLOG.md §Q Q1, the
H7 residue).
Every record-coupling measure in the §H thread so far was posited (the
fibreTrigger quarter-arc: exactly 1/2). This module derives one: the
trigger is the region where a perturbation W actually moves the state
— the overlap-deficit region — and its measure is bounded by the operator
norm ‖W − 1‖ through Markov's inequality over the typicality measure. The
same ‖W − 1‖ that prices the carrier at the operator level
(CV/CarrierPersistence.lean, carrier_persistence_window) now prices the
ontic flip probability: one knob, both levels.
overlapDeficit W p—1 − Re⟨u, Wu⟩/‖u‖²on the rayp: how farWmoves the state, ray-well-defined (overlapDeficit_mk), continuous (continuous_overlapDeficit— quotient descent, themomentMaproute), valued in[0, ‖W − 1‖](overlapDeficit_nonneg,overlapDeficit_le— the pointwise operator-norm bound, Cauchy–Schwarz).- ★
measure_deficitTrigger_le— the Markov bridge: the trigger region{δ ≤ overlapDeficit W}has typicality measure at most‖W − 1‖/δ(stated multiplicatively inℝ≥0∞). An operator norm has become a measure. deficitTriggeredKick— the record-coupled ontic step: the perturbed drive's projective flow, record kicked exactly on the trigger (triggeredRecordKickinstantiated; measure-preserving by the skew product).- ★★
deficitKick_record_halfLife— the derived half-life bound:δ · μ((intact n)ᶜ) ≤ n · ‖W − 1‖— the §H5 record half-life withεDERIVED from the drive data rather than posited. The H7 residue, discharged. deficitKick_persists_of_id— the sanity anchor: atW = 1the deficit vanishes identically, the trigger is empty, and persistence is almost-sure at every period count — no perturbation, no erosion, derived rather than assumed.
Scope #
Stated on the corpus's Fin-indexed projective sector (CPN M,
fubiniStudyMeasure), where the typicality measure lives; the CV chain's
FieldConfig-indexed drives connect by re-indexing (bookkeeping, not
mathematics — recorded, not done here). The trigger thresholds at a free
δ; the threshold-free sharp version (flip measure = the deficit
distribution itself) would need the distribution's law, not just its
Markov bound — a recorded refinement, not claimed.
The overlap deficit #
The overlap deficit: how far the unitary W moves the ray p,
measured by the normalised expectation gap 1 − Re⟨u, Wu⟩/‖u‖². Zero iff
W fixes the state's expectation; ray-well-defined (overlapDeficit_mk);
at most ‖W − 1‖ (overlapDeficit_le).
Equations
- CSD.Empirical.QuantumChaos.overlapDeficit W p = 1 - RCLike.re (inner ℂ (Projectivization.rep p) ((Matrix.toEuclideanLin ↑W) (Projectivization.rep p))) / ‖Projectivization.rep p‖ ^ 2
Instances For
The deficit computed on any representative.
The deficit descends continuously (the continuous_momentMap route).
The deficit is nonnegative: a unitary cannot raise the normalised expectation above one (Cauchy–Schwarz + norm preservation).
★ The pointwise operator-norm bound: the deficit never exceeds
‖W − 1‖.
The Markov bridge #
The trigger: the region the perturbation genuinely moves.
Equations
Instances For
★ The Markov bridge: the trigger's typicality measure is bounded by
the operator norm — δ · μ_FS(trigger) ≤ ‖W − 1‖. An operator quantity has
become a measure bound.
The record-coupled ontic step, and the derived half-life #
The deficit-triggered kick: the perturbed drive's projective flow on the sector, with the record kicked exactly where the perturbation genuinely moves the state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
★★ The derived half-life bound — the H7 residue, discharged. A
formed record survives n periods of the deficit-triggered dynamics except
on a set whose measure is priced by the operator norm of the
perturbation: δ · μ((intact n)ᶜ) ≤ n · ‖W − 1‖. The same ‖W − 1‖ that
bounds the carrier's operator-level deviation (carrier_persistence_window)
now bounds the ontic flip probability — ε derived, not posited.
The sanity anchor: no perturbation, no erosion #
The identity perturbation has zero deficit everywhere.
No perturbation, no erosion — derived: at W = 1 the trigger is
empty, the coupling is null, and a formed record persists almost surely at
every period count.
The derived coupling bites: the qubit phase flip, exactly #
Generic attainment of the half-life bound is already settled
(HalfLifeAttainment.lean: cyclicKick_halfLife_attained, equality on the
cyclic kick). What remained for the derived coupling was the bite: is the
deficit trigger ever more than null? Here it is computed exactly. For
the qubit phase flip W = diag(−1, 1) the deficit is twice the moment
coordinate (overlapDeficit_phaseFlipW), so the trigger is a moment
super-level set — and the Duistermaat–Heckman law
(fs_moment_pushforward_uniform) evaluates its typicality measure exactly:
1 − δ/2, strictly between 0 and 1 on δ ∈ (0, 2). The exact value
also shows where Markov is loose: ‖W − 1‖ = 2, so the generic Q1 bound
δ·μ ≤ 2 is trivial on this window, while the DH law pins the coupling —
the generic bridge is for drives whose deficit law is unknown; when the law
is available it should be used instead.
The qubit phase flip diag(−1, 1): the observable unitary
exp(iπ·diag(1, 0)).
Equations
- CSD.Empirical.QuantumChaos.phaseFlipW = CSD.LF4.obsUnitary (fun (i : Fin 2) => if i = 0 then 1 else 0) Real.pi
Instances For
The deficit of the phase flip is twice the moment coordinate:
overlapDeficit (diag(−1,1)) p = 2·m₀(p). The perturbation's disturbance is
read off the Kähler moment map.
★ The derived coupling, exactly (qubit, phase flip): the trigger's
typicality measure is 1 − δ/2 — the Duistermaat–Heckman law evaluates
what Markov could only bound.
The derived kick's coupling strength, exactly.
★★ The derived coupling bites: for δ ∈ (0, 2) the flip probability
is strictly between 0 and 1 — the deficit-triggered kick genuinely
couples, and the derived half-life bound below is about a real erosion
channel, not a vacuous one.
The half-life at the exact rate (qubit, phase flip): a formed record
survives n periods except on measure at most n·(1 − δ/2) — the generic
bound instantiated with the coupling the DH law computed, rather than the
Markov estimate.