GeophysicsCert
plain-language theorem explainer
GeophysicsCert is a structure asserting that the finite set of Earth layers has cardinality 5 and the finite set of geophysical observables has cardinality 5. A researcher building planetary models from Recognition Science would cite it to fix configDim D = 5 in concrete types. The declaration is a bare structure definition that records the two cardinality facts supplied by the derived Fintype instances.
Claim. Let $E$ be the set whose elements are the inner core, outer core, lower mantle, upper mantle and crust. Let $O$ be the set whose elements are seismicity, gravimetry, geomagnetism, heat flow and GPS geodesy. Then GeophysicsCert is the structure whose two fields assert that the cardinality of $E$ equals 5 and the cardinality of $O$ equals 5.
background
The Geophysics from RS module treats Earth as nested recognition spheres whose stratification yields exactly five layers, matching configDim D = 5. The inductive type enumerating inner core, outer core, lower mantle, upper mantle and crust carries a derived Fintype instance, so its cardinality is well-defined. The companion inductive type enumerating seismicity, gravimetry, geomagnetism, heat flow and GPS geodesy likewise carries a Fintype instance. This local setting follows the Recognition Science claim that five canonical layers and five observables both equal configDim D.
proof idea
The declaration is a structure definition with no proof body. It directly introduces the two fields as the statements Fintype.card EarthLayer = 5 and Fintype.card GeophysicalObservable = 5, relying on the Fintype instances that the upstream inductive definitions of EarthLayer and GeophysicalObservable derive automatically.
why it matters
GeophysicsCert supplies the certification structure instantiated by the downstream geophysicsCert definition. It fills the C Earth Science section by anchoring the five-layer and five-observable counts to configDim D = 5, consistent with the eight-tick octave and D = 3 spatial dimensions forced earlier in the chain. The structure therefore supports the broader claim that planetary observables emerge from the J-uniqueness relation without extra parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.