`planetStrataSum`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.PlanetStrataC2
domain: Physics
line: 52 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.PlanetStrataC2 on GitHub at line 52.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  71structure PlanetStrataCert where
  72  atmospheric_count : Fintype.card AtmosphericLayer = 5
  73  earth_count : Fintype.card EarthLayer = 5
  74  ocean_count : Fintype.card OceanLayer = 5
  75  total_15 : Fintype.card AtmosphericLayer + Fintype.card EarthLayer +
  76    Fintype.card OceanLayer = 15
  77  rs_sum_15 :
  78    @Fintype.card planetStrataSum.axis1.Ix planetStrataSum.axis1.finite +
  79      @Fintype.card planetStrataSum.axis2.Ix planetStrataSum.axis2.finite +
  80      @Fintype.card planetStrataSum.axis3.Ix planetStrataSum.axis3.finite = 15
  81
  82def planetStrataCert : PlanetStrataCert where

papers checked against this theorem

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