Record light cone

Records are safe from distant meddling by theorem: what lies outside the light cone can shift the outcome the arena's fibre wrote by no more than a bound that collapses factorially with distance.

proved in corpus · proved here, no imported axiomsLean record_lightcone

In plain terms

Here is the problem. If measurement outcomes are written into a hidden part of the arena, a skeptic should ask how robust the writing is. Could a distant disturbance -- some operation far from the apparatus -- reach in and rewrite the record? If so, records would be too fragile to ground anything.

The answer is a locality theorem aimed exactly at that worry. Take a record written into the arena's fibre by a local interaction. Take any disturbance supported far away, and let everything evolve. The theorem bounds how much the record cell can move by a quantity that dies factorially in the graph distance -- the same light-cone suppression that governs ordinary observables.

Distant meddling does not slightly corrupt records. It fails to touch them by a margin that shrinks factorially in the distance.

In CSD

This is the record layer and the field track meeting: the fibred arena carries record strokes -- fibre shifts controlled by base observables -- and the Lieb-Robinson machinery transports its cone through the bridge. Disjoint kicks commute with record writing exactly; distant kicks steer the written cell by at most the cone bound.

Scope, stated where it is proved: the stroke shape of fibre activity -- base-dependent fibre shifts, the corpus's own record mechanism -- not arbitrary base-coupled fibre velocities, which nothing in the record layer needs.

Mathematically

record_lightcone: for a record stroke driven by an observable A and a disturbance outside distance d, the displacement of the recorded fibre cell after time t is bounded by the Lipschitz data of the stroke times 2 (2 norm(S) t)^d / d! times norm(A) -- the rigid part of the fibre rotation cancelling between the disturbed and undisturbed histories. Companions: exact commutation of disjoint kicks with record writing, and the arena-level cone the bridge transports.

Module
CsdLean4/CV/FibredArenaBridge.lean
Related
lieb robinson bound, record layer, fibre, field arena

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy