netThrust
plain-language theorem explainer
This definition sums a sequence of per-tick thrust vectors into a single net vector over the interval of N consecutive ticks starting at t0. Discrete flight models in Recognition Science cite it when accumulating external force inputs before any continuum refinement. The definition is realized by three independent Finset.range sums, one per component of the input Vec3.
Claim. Given a map $f:ℕ→ℝ^3$ supplying a thrust vector at each tick, the net thrust over the window $[t_0,t_0+N)$ is the vector whose components are the separate sums of the three coordinates of $f(t_0+k)$ for $k=0,…,N-1$.
background
The Flight Thrust Layer supplies a minimal observable interface for thrust without yet invoking surface integrals or control-volume derivations. Vec3 is introduced as the ordered triple of real numbers that will later carry pressure-gradient information. The module therefore treats the per-tick thrust function as an external black box whose values are simply added component-wise.
proof idea
The definition is a direct component-wise summation: each coordinate of the output Vec3 is obtained by applying Finset.range.sum to the corresponding projection of f(t0+k) for k ranging from 0 to N-1.
why it matters
The definition supplies the basic aggregation step required by any later thrust-to-acceleration conversion inside the flight module. It occupies the placeholder role described in the module header, keeping the interface open for replacement by a pressure-gradient expression while preserving the discrete tick structure already fixed by the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.