atmoCount
The declaration fixes the cardinality of atmospheric layers at exactly five. Cross-domain stratification work in Recognition Science cites this count when assembling the nested planetary total of fifteen strata. The proof is a direct decision on the Fintype instance derived from the five-constructor inductive type.
claim$|AtmosphericLayer| = 5$, where AtmosphericLayer is the finite set whose elements are the five standard atmospheric divisions.
background
AtmosphericLayer is the inductive type with constructors troposphere, stratosphere, mesosphere, thermosphere, exosphere; it derives DecidableEq, Repr, BEq and Fintype. The module treats planetary stratification as the disjoint sum of three such five-element sets, AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer, yielding a total of fifteen strata that occupy distinct radial shells. The upstream inductive definition in both the local module and AtmosphericPhysicsFromRS supplies the Fintype instance used here.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the decidable cardinality computation on the derived Fintype instance of the inductive type.
why it matters in Recognition Science
This cardinality is invoked directly by planetStratumCount to obtain the total of fifteen and by atmo_is_proper_subset to establish that each five-layer injection is proper. It realizes the C2 structural claim that three nested D=5 stratifications sum to fifteen. The result supplies a combinatorial building block for the Recognition Science program of counting strata from the phi-ladder without additional axioms; the module notes that wave-speed ratios remain an open empirical question outside the Lean proof.
scope and limits
- Does not derive the layer count five from the T0-T8 forcing chain or Recognition Composition Law.
- Does not address physical wave propagation or phase velocities inside the layers.
- Does not claim the five-layer division holds for planets other than Earth.
- Does not connect the stratification count to the spatial dimension D=3 of the core framework.
Lean usage
simp only [PlanetStratum, Fintype.card_sum, atmoCount, earthCount, oceanCount]formal statement (Lean)
37theorem atmoCount : Fintype.card AtmosphericLayer = 5 := by decide