def definition def or abbrev

`eulerLedgerScalarState`

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

formal statement (Lean)

 449noncomputable def eulerLedgerScalarState (sensor : DefectSensor) (N : ℕ) : ℝ :=

proof body

Definition body.

 450  if hzero : sensor.charge = 0 then 1
 451  else realizedDefectCollapseScalar sensor hzero N
 452
 453/-- In the zero-charge sector, the Euler ledger scalar is identically `1`. -/

used by (7)

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

charge_zero_cost_scalar_t1_bounded in IndisputableMonolith.Unification.UnifiedRH decl_use
euler_collapse_boundary_transport in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerLedgerScalarState_eq_collapse in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerLedgerScalarState_eq_one in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerLedgerScalarState_pos in IndisputableMonolith.Unification.UnifiedRH decl_use
ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use
PhysicallyExists in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (6)

Lean names referenced from this declaration's body.

is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
realizedDefectCollapseScalar in IndisputableMonolith.Unification.UnifiedRH decl_use