PlanetStrataCert
plain-language theorem explainer
PlanetStrataCert records four cardinality statements that certify a planet decomposes into three independent five-element strata stacks whose direct sum totals fifteen. Recognition Science modelers cite it when assembling the planetary density or wave-speed profile from the three orthogonal axes. The structure is a record type populated downstream by explicit layer counts and the disjoint-sum identity on the weight-one vectors of F2Power 3.
Claim. Let $A$ be the set of atmospheric layers, $E$ the set of Earth layers, and $O$ the set of ocean layers. The structure asserts $|A|=5$, $|E|=5$, $|O|=5$, $|A|+|E|+|O|=15$, and the cardinality of the direct sum of the three F2Power-3 axes equals 15.
background
The module establishes the planetary 15-stratum direct sum as three independent five-element stacks (atmosphere, solid Earth, ocean) whose cardinalities add rather than tensor. AtmosphericLayer is the inductive type with five constructors (troposphere through exosphere); EarthLayer has five (innerCore through crust); OceanLayer has five (surface through abyssal). Each derives Fintype, so Fintype.card is well-defined. The three axes are the weight-one vectors of F2Power 3: axis1 = (true,false,false), axis2 = (false,true,false), axis3 = (false,false,true). The local setting is the C2 claim that the planet carries an RS disjoint sum, not a tensor product, and that the finite structural claim alone is proved here.
proof idea
PlanetStrataCert is a structure definition whose fields are the four cardinality equalities. No tactics or lemmas are applied inside the declaration itself; the downstream constructor planetStrataCert supplies the concrete values atmosphericLayerCount, earthLayerCount, oceanLayerCount, planet_strata_total_15, and planet_strata_disjoint_sum_15.
why it matters
The declaration supplies the finite structural claim required by the C2 module and is instantiated by planetStrataCert. It aligns with the three spatial dimensions (T8) via the three F2Power axes and with the eight-tick octave through the factor of five per stack. The module explicitly leaves the wave-speed phi-ratio prediction as empirical; this structure closes only the cardinality bookkeeping that later steps in the planetary stratification chain rely upon.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.