theorem proved term proof

`costFamily_unit`

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

formal statement (Lean)

 123theorem costFamily_unit (κ : ℝ) : costFamily κ 1 = 0 := by

Term-mode proof.

 124  unfold costFamily
 125  simp
 126
 127/-- The order-preserving power map on positive reals, written paper-style as
 128    `x ↦ x^α`. -/

Lean names referenced from this declaration's body.

costFamily in IndisputableMonolith.Algebra.RecognitionCategory decl_use
power in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
map in IndisputableMonolith.Measurement.RSNative.Core decl_use