ST-3: the macroscopic-coordinate projection as a structure

Category: 7-SigmaLayer (the record layer — Paper C A7). BACKLOG #99, the structure half of ST-3.

Paper D says spacetime arises "after further coarse-graining" through "additional projections", and neither paper nor charter says which projection. That is a decision, not a lemma, and specs/records-to-spacetime-scoping.md §8 records it as one; specs/BACKLOG.md #38 lists the five candidates. This module builds the frame every candidate has to fit, and nothing else:

• MacroProjection X M — a measurable map from the ontic space to a finite structure. That is all π' is, as a structure;
• FactorsThrough π B — the record event B is a union of fibres, with ★ factorsThrough_iff: it cannot distinguish two microstates with the same macroscopic coordinate. This is the form in which a candidate is checked, and it is closed under complement, union and indexed union;
• ★★ measure_eq_map_of_factorsThrough — the engine: an event that factors has the same probability in the macroscopic law (the pushforward μ.map π') as in the microscopic one. Every identity between probabilities of factoring events therefore transports verbatim, which is what "the record statistics factor through π'" has to mean;
• patternMap, patternProjection — the membership pattern of a finite record family, a MacroProjection onto Fin k → Bool (★ factorsThrough_patternMap), with the universal property ★★ patternMap_eq_of_factorsThrough: it is the coarsest coordinate the family factors through, so any other such coordinate refines it. "The statistics factor through π'" always has a canonical minimal solution;
• ★★★ noSignalling_map_iff — no-signalling survives the projection, in both directions: for a two-party family of factoring events, the macroscopic law satisfies no-signalling exactly when the microscopic law does;
• ★★★ nstep_born_map — the chain law survives the projection: csd_nstep_born's product of record weights along a chain of contexts is the chain rate, and when each step's basin factors, the same product computed with pushforward measures of coordinate sets is the same number.

Those last two are the two theorems the scoping note asks of any instance.

Honest scope

⚠️ This is a frame, not a projection. Nothing here names π', constructs a macrostate, or shows that a projection with any further property exists. The instance is BACKLOG #102 and waits on the author's choice among #38's five candidates; patternProjection is not that choice — it is the tautological coarsest solution for a family of events already in hand, which is why it carries no physics.

⚠️ The two transport theorems are conservative on purpose. They say nothing is lost and nothing is gained: a factoring projection neither destroys no-signalling nor creates it, and the same for the chain law. That is the content the note asked for — a constraint every candidate satisfies — and it must not be read as evidence for any candidate.

⚠️ NoSignalling here is a statement about measures of record events, the form that transports. The corpus's dynamical no-signalling (CV/CompositeArena.lean's composite_no_signalling) is an observable-level statement about kicks; the bridge between the two is the record-weight construction of RecordLayer/, not this file.

⚠️ M is finite with measurable singletons, which is what "a finite structure" means here and what makes every coordinate set measurable. No topology, order or geometry on M is assumed — a macroscopic geometry would be further structure on M that nothing here provides.

References: records-to-spacetime-scoping.md ST-3 and §8; RecordLayer/NStepChain.lean (csd_nstep_born), RecordLayer/GlobalBasin.lean (globalBasin, epistemicMeasure); specs/BACKLOG.md #99, #38, #102.

Factoring through a coordinate

def CSD.RecordLayer.FactorsThrough {X : Type u_1} {M : Type u_2} (π : X → M) (B : Set X) : Prop

A record event factors through the coordinates: it is a union of fibres, i.e. membership is decided by the macroscopic coordinate alone.

Equations

• CSD.RecordLayer.FactorsThrough π B = ∃ (S : Set M), B = π ⁻¹' S

theorem CSD.RecordLayer.factorsThrough_iff {X : Type u_1} {M : Type u_2} {π : X → M} {B : Set X} : FactorsThrough π B ↔ ∀ (x y : X), π x = π y → (x ∈ B ↔ y ∈ B)

★ The pointwise characterisation: an event factors through the coordinates exactly when it cannot distinguish two microstates with the same coordinate. This is the form in which the candidates of #38 are checked.

theorem CSD.RecordLayer.factorsThrough_compl {X : Type u_1} {M : Type u_2} {π : X → M} {B : Set X} (h : FactorsThrough π B) : FactorsThrough π Bᶜ

theorem CSD.RecordLayer.factorsThrough_union {X : Type u_1} {M : Type u_2} {π : X → M} {B C : Set X} (hB : FactorsThrough π B) (hC : FactorsThrough π C) : FactorsThrough π (B ∪ C)

theorem CSD.RecordLayer.factorsThrough_iUnion {X : Type u_1} {M : Type u_2} {ι : Type u_3} {π : X → M} {B : ι → Set X} (h : ∀ (i : ι), FactorsThrough π (B i)) : FactorsThrough π (⋃ (i : ι), B i)

noncomputable def CSD.RecordLayer.patternMap {X : Type u_1} {k : ℕ} (B : Fin k → Set X) (x : X) : Fin k → Bool

The membership pattern of a finite family of record events: the coarsest macroscopic coordinate from which the family can be read off.

Equations

• CSD.RecordLayer.patternMap B x i = if x ∈ B i then true else false

theorem CSD.RecordLayer.factorsThrough_patternMap {X : Type u_1} {k : ℕ} (B : Fin k → Set X) (i : Fin k) : FactorsThrough (patternMap B) (B i)

★ Every event of a finite family factors through the family's own pattern.

theorem CSD.RecordLayer.patternMap_eq_of_factorsThrough {X : Type u_1} {M : Type u_2} {k : ℕ} {B : Fin k → Set X} {π : X → M} (h : ∀ (i : Fin k), FactorsThrough π (B i)) {x y : X} (hxy : π x = π y) : patternMap B x = patternMap B y

★★ The universal property: the pattern map is the coarsest macroscopic coordinate through which a finite record family factors — any other such coordinate refines it, in the sense that two microstates it identifies have the same pattern. So "the statistics factor through π'" always has a canonical minimal solution, and a candidate of #38 is a coarsening of this one.

The structure

structure CSD.RecordLayer.MacroProjection (X : Type u_3) [MeasurableSpace X] (M : Type u_4) [MeasurableSpace M] : Type (max u_3 u_4)

A macroscopic-coordinate projection: a measurable map from the ontic space to a finite structure. Paper D's π', as a structure and nothing more — which candidate map it is, is the decision specs/BACKLOG.md #38 records and this file does not make.

• toFun : X → M

  The coordinate map.

• measurable_toFun : Measurable self.toFun

  It is measurable, so it pushes measures forward.

@[instance_reducible]

instance CSD.RecordLayer.instCoeFunMacroProjectionForall {X : Type u_1} [MeasurableSpace X] {M : Type u_2} [MeasurableSpace M] : CoeFun (MacroProjection X M) fun (x : MacroProjection X M) => X → M

Equations

• CSD.RecordLayer.instCoeFunMacroProjectionForall = { coe := CSD.RecordLayer.MacroProjection.toFun }

theorem CSD.RecordLayer.measurableSet_of_fintype {M : Type u_2} [MeasurableSpace M] [Fintype M] [MeasurableSingletonClass M] (S : Set M) : MeasurableSet S

theorem CSD.RecordLayer.measure_eq_map_of_factorsThrough {X : Type u_1} [MeasurableSpace X] {M : Type u_2} [MeasurableSpace M] [Fintype M] [MeasurableSingletonClass M] (π : MacroProjection X M) (μ : MeasureTheory.Measure X) {B : Set X} {S : Set M} (hB : B = π.toFun ⁻¹' S) : μ B = (MeasureTheory.Measure.map π.toFun μ) S

★★ The engine of ST-3: an event that factors through the coordinates has the same probability in the macroscopic law — the pushforward — as in the microscopic one. Every identity between probabilities of factoring events therefore transports verbatim, which is what "the record statistics factor through π'" has to mean.

noncomputable def CSD.RecordLayer.patternProjection {X : Type u_1} [MeasurableSpace X] {k : ℕ} (B : Fin k → Set X) (hB : ∀ (i : Fin k), MeasurableSet (B i)) : MacroProjection X (Fin k → Bool)

The pattern map of a measurable family is a MacroProjection onto a finite structure.

Equations

• CSD.RecordLayer.patternProjection B hB = { toFun := CSD.RecordLayer.patternMap B, measurable_toFun := ⋯ }

The two theorems any instance must satisfy

def CSD.RecordLayer.NoSignalling {X : Type u_1} [MeasurableSpace X] {C₁ : Type u_3} {O₁ : Type u_4} {C₂ : Type u_5} {O₂ : Type u_6} (μ : MeasureTheory.Measure X) (B : C₁ → O₁ → C₂ → O₂ → Set X) : Prop

No-signalling for a record-event family: the first party's record weights do not depend on the second party's context. Stated as an identity between probabilities, which is the form that transports.

Equations

• CSD.RecordLayer.NoSignalling μ B = ∀ (c₁ : C₁) (o₁ : O₁) (c₂ c₂' : C₂), μ (⋃ (o₂ : O₂), B c₁ o₁ c₂ o₂) = μ (⋃ (o₂ : O₂), B c₁ o₁ c₂' o₂)

theorem CSD.RecordLayer.noSignalling_map_iff {X : Type u_1} [MeasurableSpace X] {M : Type u_2} [MeasurableSpace M] [Fintype M] [MeasurableSingletonClass M] {C₁ : Type u_3} {O₁ : Type u_4} {C₂ : Type u_5} {O₂ : Type u_6} (π : MacroProjection X M) (μ : MeasureTheory.Measure X) {B : C₁ → O₁ → C₂ → O₂ → Set X} {S : C₁ → O₁ → C₂ → O₂ → Set M} (hB : ∀ (c₁ : C₁) (o₁ : O₁) (c₂ : C₂) (o₂ : O₂), B c₁ o₁ c₂ o₂ = π.toFun ⁻¹' S c₁ o₁ c₂ o₂) : NoSignalling μ B ↔ ∀ (c₁ : C₁) (o₁ : O₁) (c₂ c₂' : C₂), (MeasureTheory.Measure.map π.toFun μ) (⋃ (o₂ : O₂), S c₁ o₁ c₂ o₂) = (MeasureTheory.Measure.map π.toFun μ) (⋃ (o₂ : O₂), S c₁ o₁ c₂' o₂)

★★★ No-signalling survives the projection, in both directions: if every record event of a two-party family factors through the macroscopic coordinates, the macroscopic law — the pushforward — satisfies no-signalling exactly when the microscopic law does. Nothing is lost and nothing is gained, which is the first of the two theorems ST-3 asks of any candidate π'.

theorem CSD.RecordLayer.nstep_born_map {M : Type u_2} [MeasurableSpace M] [Fintype M] [MeasurableSingletonClass M] {N : ℕ} (π : ℕ → MacroProjection (LF4.KSigma N) M) (p : LF4.CPN N) (c : ℕ → ContextField N) (i : ℕ → Fin N) (n : ℕ) (S : ℕ → Set M) (hfac : ∀ (k : ℕ), globalBasin (c k) (i k) = (π k).toFun ⁻¹' S k) : ∏ k ∈ Finset.range n, (MeasureTheory.Measure.map (π k).toFun (epistemicMeasure (chainState p i k))) (S k) = ENNReal.ofReal (chainRate p c i n)

★★★ The chain law survives the projection. csd_nstep_born says the product of the record weights along a chain of contexts is the chain rate. If each step's basin factors through the macroscopic coordinates, the same product computed in the macroscopic law — each factor a pushforward measure of a set of coordinates — is the same number. The CSD chain law is therefore a statement about macrostates whenever the basins are macroscopic, which is the second of the two theorems ST-3 asks of any candidate π'.