Vec3
plain-language theorem explainer
Vec3 is the type alias for ordered triples of real numbers used as the basic representation of thrust and acceleration vectors. Flight layer developers cite it when building observables or experimental traces such as those in Falsifiers.Trace. The declaration is a direct abbreviation requiring no lemmas or reduction steps.
Claim. Define $V := {Vec3} := {R} times {R} times {R}$ as the space of three-component real vectors for thrust observables.
background
The Flight Thrust module supplies a minimal interface for thrust observables. It introduces a vector type, a placeholder observable, and hypothesis interfaces that can later be strengthened to pressure-gradient or control-volume forms. No full continuum derivation is attempted at this stage.
proof idea
Direct abbreviation that equates Vec3 to the Cartesian product of three copies of the reals. No lemmas from upstream results are invoked.
why it matters
Vec3 anchors the thrust interface and is used by netThrust for summation over tick windows and by thrustVector as the return type of the placeholder observable. It also appears in Trace structures for experimental falsification. The module keeps the definition minimal to allow later connection to pressure forms and gradient operators from upstream modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.