Map
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prescribe any concrete form or continuity condition on the meas function.
- Does not relate T or meas to the Recognition Composition Law or phi-ladder.
- Does not incorporate noise, error bounds, or statistical models for observations.
- Does not restrict the type parameters State or Obs to particular upstream instances.
formal statement (Lean)
69structure Map (State Obs : Type) where
70 T : ℝ
71 T_pos : 0 < T
72 meas : (ℝ → State) → ℝ → Obs
73
74/-- Midpoint sampling average (lightweight helper). -/