Physics Geophysics From Rs

Five layers, five observables

Geophysics is the physics of the Earth: how its interior is layered, how its magnetic field arises, and how we measure those things from the surface. The standard model of the Earth's interior names five canonical layers: the inner core, the outer core, the lower mantle, the upper mantle, and the crust. Seismology, the study of earthquake waves, revealed these layers in the early 20th century; the inner core was confirmed in 1936 by Inge Lehmann. The same five-part structure appears in the five geophysical observables that let us study the planet without drilling to its center: seismicity (earthquake waves), gravimetry (gravity variations), geomagnetism (the magnetic field), heat flow (internal heat escaping), and GPS geodesy (crustal movement).

In Recognition Science, the framework models the Earth as a nested set of recognition spheres, and it treats the five layers and the five observables as the same underlying dimension. The framework's machine-checked library of formal theorems contains a module, GeophysicsFromRS, that defines the five layer types and the five observable types as distinct enumerated objects. Two theorems in that module prove, by direct computation, that each set has exactly five members. A certificate structure bundles those two proofs together, and the certificate is constructed without any unproved assumptions.

The module does not derive the existence of the layers or the observables; it takes them as given definitions, matching the empirical consensus of Earth science. What it establishes is that the count is five in both cases, and that this count is consistent with the framework's broader claim that physical structure is forced by the cost of recognition. The number five here is a configuration dimension, not a derived constant like the golden ratio. The empirical check is that the framework's count matches the accepted five-layer and five-observable scheme; the match is a check, not a prediction.

What this means for a reader is that the framework can encode a piece of standard geophysics in a form a computer can verify. The five layers and five observables are not a coincidence in this account; they are the same structural number appearing in two places. The module is a small, clean example of how RS treats a classical science: it takes the established facts, formalizes them, and shows that the count fits the framework's pattern.

theorem earthLayerCount : Fintype.card EarthLayer = 5 := by decide

theorem geophysicalObservableCount : Fintype.card GeophysicalObservable = 5 := by decide

structure GeophysicsCert where
  five_layers : Fintype.card EarthLayer = 5
  five_observables : Fintype.card GeophysicalObservable = 5

def geophysicsCert : GeophysicsCert where
  five_layers := earthLayerCount
  five_observables := geophysicalObservableCount

What this page does not claim

The module does not derive the existence of the five layers or the five observables from first principles. The count five is not derived from the forcing chain that produces the golden ratio or three dimensions. The module does not provide a physical mechanism connecting the layers to the observables.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/GeophysicsFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: