euler_trace_admissible
Every defect sensor admits an admissible Euler trace consisting of a compatible regular carrier, nonvanishing carrier values above the critical line, and a bounded logarithmic derivative. Researchers formalizing the unified Riemann hypothesis in Recognition Science cite this to establish carrier infrastructure for realizable ledgers. The proof is a direct term-mode construction that assembles the three required structure fields from the Euler instantiation certificate.
claimFor every defect sensor $s$, there exists a regular carrier $C$ such that the carrier radius equals the distance from the real part of $s$ to the critical line $1/2$, $C$ is nonvanishing for all real parts greater than $1/2$, and the logarithmic derivative of $C$ is bounded by a positive function for all real parts greater than $1/2$.
background
The Unified RH module organizes realizability into three components: cost divergence for nonzero-charge sensors, Euler trace admissibility, and a T1-bounded physically realizable ledger. A DefectSensor carries a charge and a real-part location. EulerTraceAdmissible is the structure requiring a RegularCarrier whose radius matches the distance to the critical line, together with nonvanishing and derivative-bounded conditions on that carrier. This replaces earlier attempts to bound total annular cost, which contradicted the proved unboundedness result. The construction draws on the Euler instantiation certificate and upstream results such as the defect functional from the Law of Existence and the cost definitions from MultiplicativeRecognizerL4 and ObserverForcing.
proof idea
The proof is a term-mode construction of the EulerTraceAdmissible structure. It supplies the carrier_compatible field directly from sensor_carrier_compatible sensor, the carrier_nonvanishing field from the lambda expression applying carrier_nonvanishing, and the carrier_deriv_bounded field from the lambda expression applying carrierDerivBound_pos. No tactics intervene; the term simply packages the three fields furnished by the Euler instantiation data.
why it matters in Recognition Science
This theorem provides the admissibility component required by the PhysicallyRealizableLedger instance eulerPhysicallyRealizableLedger and is invoked inside ontological_exclusion and the main unified_rh theorem. It completes the first step of the chain that, together with the boundary-transport bridge hypothesis and the T1 cost barrier, yields the ontological exclusion principle: nonzero-charge sensors cannot coexist with the Euler carrier. The result sits inside the T1-bounded realizability architecture that avoids contradiction with the proved unbounded annular cost.
scope and limits
- Does not prove the Riemann hypothesis.
- Does not establish existence of the Euler carrier from first principles.
- Does not bound total annular cost.
- Does not apply when the sensor charge is zero.
- Does not discharge the external boundary-transport bridge hypothesis.
Lean usage
theorem admissible_for_sensor (s : DefectSensor) : EulerTraceAdmissible s := euler_trace_admissible sformal statement (Lean)
111theorem euler_trace_admissible (sensor : DefectSensor) :
112 EulerTraceAdmissible sensor where
113 carrier_compatible := sensor_carrier_compatible sensor
proof body
Term-mode proof.
114 carrier_nonvanishing := fun _ hσ => carrier_nonvanishing hσ
115 carrier_deriv_bounded := fun _ hσ => carrierDerivBound_pos hσ
116
117/-! ## §3. T1 cost barrier (re-export) -/
118
119/-- The T1 scalar cost barrier from the Law of Existence:
120approaching the non-existence boundary forces arbitrarily large defect cost.
121
122`∀ C, ∃ ε > 0, ∀ x ∈ (0,ε), defect(x) > C` -/