def
definition
def or abbrev
realizedDefectCollapseScalar
show as:
view Lean formalization →
formal statement (Lean)
305noncomputable def realizedDefectCollapseScalar
306 (sensor : DefectSensor) (hm : sensor.charge ≠ 0) (N : ℕ) : ℝ :=
proof body
Definition body.
307 1 / (1 + annularCost ((canonicalDefectSampledFamily sensor hm).mesh N))
308
309/-- The realized defect collapse scalar is always positive. -/
used by (12)
-
defect_realizedDefectCollapseScalar -
direct_t1_exclusion -
eulerLedgerScalarState -
eulerLedgerScalarState_eq_collapse -
not_realizedDefectCollapseScalar_t1_bounded -
obstruction_structural_asymmetry -
ontological_dichotomy -
RealizedCollapseBoundaryApproaching -
realizedDefectCollapseBoundaryApproaching_of_nonzero_charge -
realizedDefectCollapseScalar_defect_unbounded -
realizedDefectCollapseScalar_pos -
single_scalar_obstruction