def definition def or abbrev

`valueFunctional`

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

formal statement (Lean)

  47def valueFunctional (sigma sigma_max : ℝ) : ℝ :=

Definition body.

  48  1 - Jcost (sigma / sigma_max)
  49

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

consensual_iff_jcost_nondecreasing in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use
ConsentInterfaceCert in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use
IsConsensual in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use
valueFunctional_at_optimum in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use
valueFunctional_nonneg in IndisputableMonolith.Ethics.ConsentInterfaceFromJCost decl_use

Lean names referenced from this declaration's body.

sigma in IndisputableMonolith.Decision.AbileneParadox decl_use
sigma in IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions decl_use