def definition def or abbrev

`eulerScalarProxy`

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

formal statement (Lean)

 173noncomputable def eulerScalarProxy (sensor : DefectSensor) (N : ℕ) : ℝ :=

Definition body.

 174  1 / (1 + eulerScalarGap sensor / (N + 1 : ℝ))
 175
 176/-- The concrete Euler scalar proxy stays positive at every refinement depth. -/

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

eulerLedgerScalarState_pos in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerPhysicallyRealizableLedger in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerScalarProxy_defect_bounded in IndisputableMonolith.Unification.UnifiedRH decl_use
eulerScalarProxy_pos in IndisputableMonolith.Unification.UnifiedRH decl_use
physicallyRealizableLedger_not_boundaryApproaching in IndisputableMonolith.Unification.UnifiedRH decl_use

Lean names referenced from this declaration's body.

DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
refinement in IndisputableMonolith.Papers.DraftV1 decl_use
eulerScalarGap in IndisputableMonolith.Unification.UnifiedRH decl_use