PhysicallyExists
plain-language theorem explainer
A defect sensor physically exists when its Euler ledger scalar state has T1 defect bounded by some real constant K for all natural numbers N. Researchers deriving the Riemann Hypothesis from Recognition Science cite this definition as the formal existence criterion in the T1-bounded realizability architecture. The definition directly encodes the bounded-defect condition on the ledger state via the defect functional.
Claim. Let $s$ be a defect sensor with charge and real-part data. Then $s$ physically exists if there exists $K : ℝ$ such that for all $N : ℕ$, the defect $J$ of the Euler ledger scalar state of $s$ at step $N$ satisfies $J(s_N) ≤ K$.
background
The Unified RH module replaces an earlier total-cost ledger with a three-component T1-bounded realizability architecture: cost divergence for nonzero charge, Euler trace admissibility, and physically realizable ledgers whose scalar proxy keeps T1 defect uniformly bounded. The DefectSensor structure records the multiplicity (charge) of a zeta zero and its real part. The defect functional equals J, the Recognition Science cost map. The eulerLedgerScalarState returns the constant 1 when charge is zero and the realized collapse scalar otherwise.
proof idea
This is a direct definition that encodes the bounded T1 defect condition. It applies the defect functional from LawOfExistence to the eulerLedgerScalarState for each N and asserts existence of a uniform real bound K.
why it matters
This definition is the target conclusion of the proxy physicalization bridge and feeds theorems such as proxyPhysicalizationBridge_iff_physicallyExists and rh_from_ZeroInducedProxyPhysicalizationBridge that recover the Riemann Hypothesis once the bridge holds for zero-charge sensors. It completes the physically realizable ledger component of the Unified RH architecture and links directly to the ontological dichotomy theorem, which equates charge zero with bounded T1 defect.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.