def definition def or abbrev

`PhysicallyExists`

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

formal statement (Lean)

 921def PhysicallyExists (sensor : DefectSensor) : Prop :=

proof body

Definition body.

 922  ∃ K : ℝ, ∀ N : ℕ,
 923    IndisputableMonolith.Foundation.LawOfExistence.defect
 924      (eulerLedgerScalarState sensor N) ≤ K
 925
 926/-- `ontological_dichotomy` restated: charge = 0 ↔ physically exists. -/

used by (22)

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

physicallyExists_of_ProxyPhysicalizationBridge in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
ProxyPhysicalizationBridge in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
proxyPhysicalizationBridge_iff_physicallyExists in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
proxyPhysicalizationBridge_of_charge_zero in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
rh_from_ZeroInducedProxyPhysicalizationBridge in IndisputableMonolith.NumberTheory.ProxyPhysicalizationBridge decl_use
nonzero_charge_impossible in IndisputableMonolith.NumberTheory.RH_Certificate decl_use
unit_sensor_not_physical_cert in IndisputableMonolith.NumberTheory.RH_Certificate decl_use
nonzero_charge_not_physical in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
rh_from_rs_thesis in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
rh_right_half_certificate in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
RSPhysicalThesis in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
strip_zero_gives_nonphysical_sensor in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
unit_sensor_not_physical in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
witnessed_physical_contradiction in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
witnessed_sensor_not_physical in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
zetaDefectSensor_charge_ne_zero in IndisputableMonolith.NumberTheory.ZetaLedgerBridge decl_use
all_physicallyExist_of_rh in IndisputableMonolith.Unification.UnifiedRH decl_use
charge_zero_iff_physicallyExists in IndisputableMonolith.Unification.UnifiedRH decl_use
ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use
PhysicalSensor in IndisputableMonolith.Unification.UnifiedRH decl_use
rh_from_ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use
rh_iff_all_physical in IndisputableMonolith.Unification.UnifiedRH decl_use

depends on (6)

Lean names referenced from this declaration's body.

K in IndisputableMonolith.Constants decl_use
K in IndisputableMonolith.Constants.LambdaRecDerivation decl_use
defect in IndisputableMonolith.Foundation.LawOfExistence decl_use
DefectSensor in IndisputableMonolith.NumberTheory.CostCoveringBridge decl_use
eulerLedgerScalarState in IndisputableMonolith.Unification.UnifiedRH decl_use
ontological_dichotomy in IndisputableMonolith.Unification.UnifiedRH decl_use