theorem proved term proof

`planetStratumCount`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  43theorem planetStratumCount : Fintype.card PlanetStratum = 15 := by

proof body

Term-mode proof.

  44  simp only [PlanetStratum, Fintype.card_sum, atmoCount, earthCount, oceanCount]
  45
  46/-- The three injections are not surjective: each covers only 5 of 15. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

atmo_is_proper_subset in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
earth_is_proper_subset in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
ocean_is_proper_subset in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
planetStratificationCert in IndisputableMonolith.CrossDomain.PlanetStratification decl_use

depends on (9)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
atmoCount in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
earthCount in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
oceanCount in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
PlanetStratum in IndisputableMonolith.CrossDomain.PlanetStratification decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use