pith. machine review for the scientific record. sign in
structure

PlanetStrataCert

definition
show as:
view math explainer →
module
IndisputableMonolith.Physics.PlanetStrataC2
domain
Physics
line
71 · 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 71.

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

  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
  83  atmospheric_count := atmosphericLayerCount
  84  earth_count := earthLayerCount
  85  ocean_count := oceanLayerCount
  86  total_15 := planet_strata_total_15
  87  rs_sum_15 := planet_strata_disjoint_sum_15
  88
  89end PlanetStrataC2
  90end Physics
  91end IndisputableMonolith

papers checked against this theorem

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