`earthCount`

proved

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.PlanetStratification
domain: CrossDomain
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.PlanetStratification on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  35  deriving DecidableEq, Repr, BEq, Fintype
  36
  37theorem atmoCount : Fintype.card AtmosphericLayer = 5 := by decide
  38theorem earthCount : Fintype.card EarthLayer = 5 := by decide
  39theorem oceanCount : Fintype.card OceanLayer = 5 := by decide
  40
  41abbrev PlanetStratum : Type := AtmosphericLayer ⊕ EarthLayer ⊕ OceanLayer
  42
  43theorem planetStratumCount : Fintype.card PlanetStratum = 15 := by
  44  simp only [PlanetStratum, Fintype.card_sum, atmoCount, earthCount, oceanCount]
  45
  46/-- The three injections are not surjective: each covers only 5 of 15. -/
  47theorem atmo_is_proper_subset :
  48    Fintype.card PlanetStratum > Fintype.card AtmosphericLayer := by
  49  rw [planetStratumCount, atmoCount]; decide
  50
  51theorem earth_is_proper_subset :
  52    Fintype.card PlanetStratum > Fintype.card EarthLayer := by
  53  rw [planetStratumCount, earthCount]; decide
  54
  55theorem ocean_is_proper_subset :
  56    Fintype.card PlanetStratum > Fintype.card OceanLayer := by
  57  rw [planetStratumCount, oceanCount]; decide
  58
  59/-- 15 = 3 × D (where D = 5). -/
  60theorem planetStratum_three_D : 15 = 3 * 5 := by decide
  61
  62structure PlanetStratificationCert where
  63  stratum_count : Fintype.card PlanetStratum = 15
  64  three_D : 15 = 3 * 5
  65  atmo_sub : Fintype.card PlanetStratum > Fintype.card AtmosphericLayer
  66  earth_sub : Fintype.card PlanetStratum > Fintype.card EarthLayer
  67  ocean_sub : Fintype.card PlanetStratum > Fintype.card OceanLayer
  68

papers checked against this theorem

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