avg
plain-language theorem explainer
The avg definition supplies a midpoint sampling operator that evaluates a continuous function x at t + T/2 for any positive interval length T. Measurement-layer code in Recognition Science cites it when building lightweight continuous-time descriptors from stream data. The implementation is a direct arithmetic reduction that forms the midpoint and returns the sampled value.
Claim. Let $T > 0$, let $x : ℝ → ℝ$, and let $t ∈ ℝ$. Define avg$(T, x, t) := x(t + T/2)$.
background
The Measurement module supplies eight-tick stream invariants together with a continuous-time scaffold built around the coherence quotient. The CQ structure records listensPerSec, opsPerSec and a coherence8 field whose bounds are witnessed as 0 ≤ coherence8 ≤ 1. Upstream, the Breath1024 T abbreviation denotes fundamental periods as natural numbers, while the Gap45 T definition computes the triangular number n(n+1)/2; the sibling CQ abbreviation re-exports the same coherence descriptor for use in cost-model alignment thresholds.
proof idea
The definition is a direct one-line computation: it forms the midpoint t + T/2 and returns the value of the input function x at that point.
why it matters
The helper supports the continuous-time measurement scaffold that supplies coherence scores to the eight-tick octave layer. It sits inside the T7 period-8 construction by providing a uniform sampling rule compatible with block-aligned streams. No downstream theorems are recorded, so the declaration functions as an internal utility rather than a theorem that closes a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.