earthAxis
plain-language theorem explainer
The declaration defines the solid-Earth five-stratum axis as a CoupledAxis instance in the planetary model. A researcher constructing the three-stack direct sum for atmosphere, Earth, and ocean would cite it to complete the 15-element structure. The definition is a direct structure instance that names the EarthLayer type, invokes its Fintype instance, cites the cardinality lemma, and tags the axis with the jCost primitive.
Claim. Let $E$ be the inductive type with five constructors corresponding to inner core, outer core, lower mantle, upper mantle, and crust. The Earth axis is the CoupledAxis structure on $E$ equipped with a Fintype instance, cardinality exactly 5, and tagged by the jCost primitive.
background
The CoupledAxis structure consists of an index type Ix, a Fintype proof for that type, a cardinality equality to the parameter n, and a primitive tag drawn from the RSPrimitive inductive. EarthLayer is the inductive type whose five constructors label the geological layers and carries DecidableEq, Repr, BEq, and Fintype instances. The module establishes the planetary 15-stratum direct sum as three independent five-stratum stacks (atmosphere, solid Earth, ocean) realized as an RS disjoint sum. The upstream earthLayerCount lemma supplies the required cardinality equality of 5.
proof idea
The definition populates the CoupledAxis structure fields directly. It sets Ix to EarthLayer, obtains the finite field via inferInstance, supplies the card_eq field from the earthLayerCount lemma, and sets the primitive field to the jCost constructor of RSPrimitive.
why it matters
This definition supplies the middle axis in the planetStrataSum construction that realizes the RSDisjointSum3 5 for the full planetary strata. It closes the finite structural claim in the C2 module for the three-stack model. The construction uses finite domains tagged by RS primitives such as jCost, consistent with the Recognition Science emphasis on structural axes before dynamical or phi-ladder content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.