pith. sign in
module module moderate

IndisputableMonolith.Physics.GeophysicsFromRS

show as:
view Lean formalization →

This module introduces the core geophysical definitions derived from Recognition Science, including EarthLayer, GeophysicalObservable, and GeophysicsCert. These objects model planetary strata and observables for use in higher-level constructions. The module consists entirely of type definitions and count functions with no theorems or proofs. It is referenced by the planetary stratum direct sum in PlanetStrataC2.

claimThe module defines $EarthLayer$, $earthLayerCount$, $GeophysicalObservable$, $geophysicalObservableCount$, $GeophysicsCert$, and $geophysicsCert$ as the basic objects for RS-derived geophysics.

background

The module sits in the Physics domain and imports only Mathlib. It introduces EarthLayer as the basic unit for planetary stratification, GeophysicalObservable for quantities measurable under the Recognition Composition Law, and GeophysicsCert as the certification object. The count functions earthLayerCount and geophysicalObservableCount enumerate the layers and observables. This provides the setting for the three-stack model of atmosphere, solid Earth, and ocean.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed directly into the C2 planetary 15-stratum direct sum of PlanetStrataC2, which decomposes the planet into three independent 5-strata stacks. It supplies the interface between Recognition Science primitives and geophysical observables, closing one step in the derivation of planetary structure from the forcing chain.

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)