Map
plain-language theorem explainer
The Map structure defines a minimal scaffold for continuous-time measurements, consisting of a positive real period T and a function that extracts observations from state trajectories over time. Physicists extending eight-tick stream models to continuous sampling would cite this when parameterizing measurement processes in the Recognition layer. As a structure definition it introduces the type with no proof obligations or computational content.
Claim. A measurement map consists of a positive real number $T > 0$ and a function $meas : (ℝ → State) → ℝ → Obs$ that samples an observation from a state trajectory at a given time.
background
The Measurement module re-exports eight-tick stream invariants from Streams and Blocks while adding a lightweight continuous-time scaffold. Upstream State types include the discrete 2D Galerkin state at truncation N from CPM2D and the finite lattice vorticity field from DiscreteVorticity; T aligns with the fundamental period abbrev from Breath1024, here lifted to positive reals for continuous time. The structure therefore supplies a uniform type for maps that convert trajectories (functions ℝ → State) into observations.
proof idea
This is a structure definition that directly declares the three fields T, T_pos, and meas with no lemmas applied and no tactic steps.
why it matters
The definition supplies the basic type used by the map and Measurement declarations in RSNative.Core, and appears in downstream bridges such as SuperconductorFamily classification and ClayBridge compatibility structures. It connects discrete eight-tick invariants (T7) to continuous sampling in the measurement layer, supporting the overall scaffold for CQ scores without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.