def definition def or abbrev

`balanceResidual`

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

formal statement (Lean)

  41noncomputable def balanceResidual (lambda : ℝ) : ℝ :=

Definition body.

  42  J_curv lambda - J_bit_normalized
  43
  44/-- The balance point in RS-native dimensionless units. -/

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

balance_at_lambda_0 in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
balance_determines_lambda in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
balance_unique_positive_root in IndisputableMonolith.Constants.LambdaRecDerivation decl_use

Lean names referenced from this declaration's body.

J_bit_normalized in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
J_curv in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
J_curv in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
lambda in IndisputableMonolith.Physics.RGTransport decl_use