aerodynamicForceCount
plain-language theorem explainer
The declaration proves that the finite type of aerodynamic forces has cardinality five. Recognition Science modelers of fluid dynamics would cite this count when enumerating forces in the J-cost balance for flight. The proof is a one-line decision procedure that evaluates the Fintype instance derived from the five constructors.
Claim. The set of aerodynamic forces has cardinality five: $|$lift, drag, thrust, weight, moment$| = 5$.
background
The AerodynamicsFromRS module treats flight as recognition cost balance at J = 0, where equilibrium lift equals drag and the J-cost landscape is minimized at cruise angle of attack. It introduces the inductive type with constructors lift, drag, thrust, weight and moment, which derives a Fintype instance to support cardinality computation. This realizes configDim D = 5 for the force enumeration in the RS framework. The upstream equilibrium result states that at equilibrium Jcost 1 = 0.
proof idea
The proof is a term-mode one-liner that applies the decide tactic. The tactic directly computes the cardinality from the Fintype instance automatically generated by the five constructors of the inductive type.
why it matters
This supplies the five_forces field in the downstream aerodynamicsCert definition, which bundles the force count with the cruise equilibrium condition. It realizes the five-force enumeration for B11 Fluids / Engineering in the Recognition Science chain and links to the J = 0 equilibrium from the nonlinear dynamics module. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.