Pith. sign in
module module moderate

IndisputableMonolith.Physics.GeophysicsFromRS

show as:
view Lean formalization →

The GeophysicsFromRS module supplies the core definitions for modeling planetary geophysics within Recognition Science. It introduces EarthLayer, GeophysicalObservable, and GeophysicsCert to certify RS-derived structures. These feed the PlanetStrataC2 module for assembling the three independent 5-strata stacks. The module contains only definitions and no proofs.

claimThe module defines EarthLayer (planetary strata), GeophysicalObservable (RS-derived measurable quantities), and GeophysicsCert (certification that the structures satisfy the Recognition framework).

background

This module sits in the Physics domain and introduces EarthLayer, earthLayerCount, GeophysicalObservable, geophysicalObservableCount, GeophysicsCert, and geophysicsCert as the basic objects. These rest on the Recognition Science primitives such as the phi-ladder and J-uniqueness from the forcing chain. The local setting treats geophysical quantities as discrete strata whose counts and observables are certified for consistency with RS constants.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module is imported by PlanetStrataC2 to support the C2 claim of a planetary 15-stratum direct sum consisting of atmosphere, solid Earth, and ocean stacks. It supplies the foundational definitions required to apply the Recognition framework to geophysics.

scope and limits

used by (1)

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

declarations in this module (6)