theorem proved term proof

`cube_volume_surface`

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

formal statement (Lean)

  53theorem cube_volume_surface (L : ℕ) (hL : 0 < L) :
  54    (6 * L ^ 2 : ℕ) > 0 ∧ (L ^ 3 : ℕ) > 0 := by

proof body

Term-mode proof.

  55  constructor
  56  · positivity
  57  · positivity
  58
  59/-- The surface-to-volume ratio of a cube: 6L²/L³ = 6/L.
  60    This decreases with L, confirming surface < volume scaling. -/

depends on (8)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers 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
volume in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use