oceanAxis
plain-language theorem explainer
oceanAxis supplies the ocean component of the planetary 15-stratum decomposition in Recognition Science. It indexes the five layers from surface to abyssal and tags them with the sigma-charge primitive. The definition is a direct instantiation of the CoupledAxis structure that references the oceanLayerCount theorem for cardinality.
Claim. The ocean axis is the coupled axis of length 5 whose index set is the five-element type of ocean layers (surface, thermocline, intermediate, deep, abyssal) and which is tagged by the sigma-charge primitive.
background
A CoupledAxis n is a structure consisting of an index type Ix, a Fintype instance on Ix, a proof that the cardinality of Ix equals n, and an RSPrimitive tag that labels the physical meaning of the axis. OceanLayer is the inductive type whose constructors are surface, thermocline, intermediate, deep, and abyssal. The theorem oceanLayerCount states that Fintype.card OceanLayer equals 5. RSPrimitive.sigmaCharge is the chosen tag among the five available primitives.
proof idea
The definition populates the four fields of CoupledAxis directly: the index type is set to OceanLayer, the finite instance is inferred from the deriving clause, the card_eq field is assigned the theorem oceanLayerCount, and the primitive field is assigned RSPrimitive.sigmaCharge.
why it matters
This definition is referenced by planetStrataSum, which assembles the three axes into an RSDisjointSum3. It supplies the ocean slot in the module claim that the planet comprises three independent five-stratum stacks whose direct sum yields fifteen strata. Within the Recognition Science framework it contributes to the structural decomposition that precedes the eight-tick octave and the derivation of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.