AerodynamicForce
plain-language theorem explainer
The inductive definition enumerates the five canonical aerodynamic forces as an explicit finite set in the Recognition Science treatment of fluids. Aerodynamic modelers deriving equilibrium conditions from J-cost minimization at cruise would cite this enumeration when establishing the configuration dimension. It is introduced directly as an inductive type with automatic derivation of decidable equality and finite-type instances.
Claim. Let $F$ be the finite set whose elements are the five aerodynamic forces lift, drag, thrust, weight, and moment. Then $|F|=5$, matching the configuration dimension $D=5$ required for the Recognition Science model of flight as J-cost balance at equilibrium.
background
The module treats B11 Fluids / Engineering by positing that flight corresponds to recognition cost balance at J=0, with the J-cost landscape minimized at the cruise angle of attack. Five canonical force types are required to reach configDim D=5. The supplied definition supplies the explicit finite enumeration of those forces.
proof idea
This is a direct inductive definition that enumerates the five constructors and derives the DecidableEq, Repr, BEq, and Fintype instances in one step.
why it matters
The definition supplies the force set required by the downstream cardinality theorem establishing exactly five forces and by the AerodynamicsCert structure that pairs the five-forces field with the cruise equilibrium condition Jcost 1 = 0. It thereby anchors the Recognition Science claim that flight equilibrium occurs at J=0 inside the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.