euler_trace_admissible
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.