`planetStrataCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.PlanetStrataC2
domain: Physics
line: 82 · 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 82.

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

formal source

  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.