GeophysicalObservable
plain-language theorem explainer
GeophysicalObservable enumerates the five standard Earth-science quantities that Recognition Science identifies with configuration dimension D. Geophysicists and RS modelers cite it when certifying that the theory reproduces the canonical observable set. The declaration is an inductive type with five constructors that automatically supplies Fintype, DecidableEq, Repr, and BEq instances.
Claim. GeophysicalObservable is the inductive type whose five constructors are seismicity, gravimetry, geomagnetism, heat flow, and GPS geodesy, equipped with decidable equality and a Fintype instance.
background
The module treats Earth as five nested recognition spheres (inner core, outer core, lower mantle, upper mantle, crust) so that configDim D equals 5. It identifies the same dimension D with five canonical geophysical observables: seismicity, gravimetry, geomagnetism, heat flow, and GPS geodesy. The inductive definition supplies the Lean encoding of these observables.
proof idea
The declaration is an inductive type with exactly five constructors that derives the Fintype, DecidableEq, Repr, and BEq instances by standard typeclass synthesis.
why it matters
This type is required by the GeophysicsCert structure, which asserts that both EarthLayer and GeophysicalObservable have cardinality 5. It directly implements the module statement that five observables equal configDim D. The construction supplies the concrete data side of the RS geophysics certification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.