Pith. sign in
module module high

IndisputableMonolith.Foundation.RSCoupledAxis

show as:
view Lean formalization →

This module defines the five RS primitives for tagging domain axes together with supporting structures such as CoupledAxis and RSIndependentTriple. Modelers of multi-layer physical systems, including planetary strata, cite these definitions to label independent axes. The module contains only definitions and cardinality lemmas with no theorems to prove.

claimThe module introduces the base type $\text{RSPrimitive}$ for axis tags, the structure $\text{CoupledAxis}$ for paired primitives, the type $\text{RSIndependentTriple}$ for three mutually independent axes, and the associated cardinality functions $\text{tripleProductCard}$ and $\text{disjoint_sum_card}$.

background

Recognition Science tags physical domains with discrete primitives that label independent axes. The module supplies the five primitives and the algebraic constructions (independent triples, disjoint sums) needed to combine them while preserving independence. These objects appear directly in the downstream construction of three 5-stratum stacks for atmosphere, solid Earth, and ocean.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed the direct-sum construction of the planetary 15-stratum model in PlanetStrataC2, where three independent 5-strata stacks are assembled from the primitives supplied here. The module therefore supplies the axis-tagging layer required by the C2 planetary-strata proposition.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

declarations in this module (11)