theorem proved term proof

`posting_one`

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

formal statement (Lean)

  63theorem posting_one : PostingPotential 1 = 1 := by

Term-mode proof.

  64  unfold PostingPotential Jcost
  65  simp [inv_one]
  66
  67/-- Π(x) > 0 for all x > 0. -/

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
PostingPotential in IndisputableMonolith.Foundation.PostingExtensivity decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use