Pith. sign in
module module moderate

IndisputableMonolith.Physics.AerodynamicsFromRS

show as:
view Lean formalization →

AerodynamicsFromRS module translates the Recognition Science J-cost into aerodynamic force expressions and equilibrium statements. It imports the Cost module and defines cruise equilibrium as the condition J equals zero, along with AerodynamicForce, aerodynamicForceCount, AerodynamicsCert and related objects. The module consists entirely of definitions and certificates with no internal proofs.

claimCruise equilibrium is the condition $J=0$, where $J$ denotes the Recognition Science cost function. Aerodynamic force and its count are expressed in terms of this cost, with an associated certificate AerodynamicsCert.

background

The module sits in the physics domain and imports IndisputableMonolith.Cost, the source of the J-cost function used throughout Recognition Science. The supplied doc comment identifies the central object as cruise equilibrium expressed by J = 0. Sibling declarations in the same file supply AerodynamicForce, aerodynamicForceCount, cruise_equilibrium, AerodynamicsCert and aerodynamicsCert.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the aerodynamic layer that applies the J-cost framework to fluid forces and equilibrium. It feeds the AerodynamicsCert object and the broader physics derivations that rest on the Cost module. It addresses the cruise equilibrium step within the T0-T8 forcing chain.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)