pith. sign in
module module high

IndisputableMonolith.Physics.OceanographyFromRS

show as:
view Lean formalization →

OceanographyFromRS supplies the ocean stack for Recognition Science planetary models by defining discrete layers and a certification object. Researchers building unified derivations of atmosphere-Earth-ocean strata cite it when assembling the full C2 direct sum. The module consists of type definitions and a certification drawn from the RS time quantum, with no complex proofs.

claimOceanLayer as a type for discrete ocean strata; oceanLayerCount : ℕ; OceanographyCert as a certification proposition; oceanographyCert : OceanographyCert.

background

The module imports IndisputableMonolith.Constants, whose sole documented object is the fundamental RS time quantum τ₀ = 1 tick. It introduces OceanLayer, oceanLayerCount, OceanographyCert and oceanographyCert as the ocean-specific objects needed for planetary modeling. The local setting is the Recognition Science derivation of all physics from the J-functional equation, with oceanography treated as one of three independent 5-stratum stacks.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the parent construction in PlanetStrataC2 on the C2 planetary 15-stratum direct sum, which assembles three independent 5-stratum stacks (atmosphere, solid Earth, ocean). It supplies the ocean component required to complete that direct-sum statement.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (4)