  37  card_eq := atmosphericLayerCount
  38  primitive := RSPrimitive.phiLadder
  39
  40def earthAxis : CoupledAxis 5 where
  41  Ix := EarthLayer
  42  finite := inferInstance
  43  card_eq := earthLayerCount
  44  primitive := RSPrimitive.jCost
  45
  46def oceanAxis : CoupledAxis 5 where
  47  Ix := OceanLayer
  48  finite := inferInstance
  49  card_eq := oceanLayerCount
  50  primitive := RSPrimitive.sigmaCharge
  51
  52def planetStrataSum : RSDisjointSum3 5 where
  53  axis1 := atmosphereAxis
  54  axis2 := earthAxis
  55  axis3 := oceanAxis
  56  indep12 := by simp [independent, atmosphereAxis, earthAxis]
  57  indep13 := by simp [independent, atmosphereAxis, oceanAxis]
  58  indep23 := by simp [independent, earthAxis, oceanAxis]
  59
  60theorem planet_strata_total_15 :
  61    Fintype.card AtmosphericLayer + Fintype.card EarthLayer +
  62      Fintype.card OceanLayer = 15 := by
  63  rw [atmosphericLayerCount, earthLayerCount, oceanLayerCount]
  64
  65theorem planet_strata_disjoint_sum_15 :
  66    @Fintype.card planetStrataSum.axis1.Ix planetStrataSum.axis1.finite +
  67      @Fintype.card planetStrataSum.axis2.Ix planetStrataSum.axis2.finite +
  68      @Fintype.card planetStrataSum.axis3.Ix planetStrataSum.axis3.finite = 15 := by
  69  rw [disjoint_sum_card planetStrataSum]
  70

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.