geophysicalObservableCount
plain-language theorem explainer
The theorem asserts that the finite type of geophysical observables has exactly five elements in the Recognition Science Earth model. Geophysicists using the RS framework for layered Earth certification would cite this cardinality when populating the observables field. The proof is a one-line decision procedure that exhausts the five constructors of the GeophysicalObservable inductive type.
Claim. The finite type of geophysical observables has cardinality five: $Fintype.card(GeophysicalObservable) = 5$, where the observables are the cases seismicity, gravimetry, geomagnetism, heat flow, and GPS geodesy.
background
The module models Earth as nested recognition spheres with five canonical layers and five observables, both equal to configDim D. GeophysicalObservable is the inductive type whose constructors are seismicity, gravimetry, geomagnetism, heatFlow, and gpsGeodesy; it derives DecidableEq, Repr, BEq, and Fintype so that cardinality is computable. This setup follows the upstream convention that five observables match the five Earth layers in the RS-native description.
proof idea
The proof applies the decide tactic directly to the goal Fintype.card GeophysicalObservable = 5. The tactic enumerates the five constructors of the inductive type GeophysicalObservable and confirms the cardinality by decidability of finite types.
why it matters
This supplies the five_observables field inside the geophysicsCert definition, which pairs it with earthLayerCount to certify the full RS Earth model. It instantiates the configDim D = 5 landmark for observables, closing the enumeration step that links the five-layer structure to the five measurable quantities without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.