geophysicsCert
plain-language theorem explainer
GeophysicsCert packages the five-layer Earth model with five canonical observables into one structure to certify configDim D equals 5. Researchers deriving Earth properties from nested recognition spheres cite it to fix the layer and observable counts in RS derivations. The definition is assembled by direct field assignment from the two decidable cardinality theorems.
Claim. The structure GeophysicsCert consists of the assertions that the cardinality of EarthLayer is 5 and the cardinality of GeophysicalObservable is 5.
background
Recognition Science models Earth as nested recognition spheres whose five canonical layers (inner core, outer core, lower mantle, upper mantle, crust) realize configDim D = 5. The module pairs this with five geophysical observables: seismicity, gravimetry, geomagnetism, heat flow, and GPS geodesy. Both counts are encoded as finite-type cardinalities in Lean.
proof idea
The definition is a direct one-line wrapper that substitutes the theorem earthLayerCount into the five_layers field and geophysicalObservableCount into the five_observables field of the GeophysicsCert structure.
why it matters
This definition supplies the concrete certificate that anchors the Earth model inside the Geophysics from RS module and realizes configDim D = 5 for nested spheres. It closes the Lean encoding of the five-layer and five-observable counts with zero sorry or axiom. No downstream uses are recorded, leaving open the question of how the certificate feeds into explicit RS derivations of magnetic or seismic observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.