Map
plain-language theorem explainer
The Map structure defines a minimal scaffold for continuous-time measurement, consisting of a positive real period T together with a function that converts state trajectories into observations. Researchers building measurement layers or CQ scores cite it when connecting discrete eight-tick streams to continuous observation models. As a bare structure definition it carries no proof obligations and simply declares the three fields.
Claim. A measurement map from state space $State$ to observation space $Obs$ is given by a pair $(T, meas)$ where $T > 0$ is a real number and $meas : (ℝ → State) → ℝ → Obs$ assigns an observation to each trajectory and time.
background
The Measurement module re-exports eight-tick stream invariants and supplies a lightweight continuous-time measurement scaffold. Map depends on four upstream state and period definitions: the discrete 2D Galerkin state (CPM2D.State), the fundamental period abbreviation T (Breath1024.T), the triangular-number function T (Gap45.SyncMinimization.T), and the finite discrete vorticity field (NavierStokes.DiscreteVorticity.State). These supply the concrete State type that trajectories map from ℝ into.
proof idea
This is a structure definition; the Lean compiler accepts the three fields T, T_pos, and meas with no further obligations or lemmas applied.
why it matters
Map supplies the continuous-time interface used by fourteen downstream declarations, including SuperconductorFamily classification, the ClayBridge structure that projects RS complexity onto Turing models, multiplication on LogicInt and LogicRat, torsion8 on words, and the MockThetaPhantomCorrespondence hypothesis. It realizes the measurement scaffold that complements the eight-tick octave (T7) and feeds the RSNative.Core map and Measurement constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.