no_cost_divergent_sensor_of_boundary_transport
plain-language theorem explainer
Boundary transport certificates make cost-divergent Euler sensors impossible. Researchers deriving the Riemann hypothesis from the Recognition Composition Law would cite this to confirm that realized defects cannot produce unbounded annular costs under T1 boundary conditions. The proof obtains the physically realizable ledger instance and the divergence-witness class from the certificate then applies ontological exclusion to the admissible trace.
Claim. Let $c$ be a boundary transport certificate and $s$ a defect sensor. Then $s$ is not cost-divergent: its annular cost remains bounded under uniform-charge sampling at every refinement depth.
background
The Boundary Transport module supplies the remaining physical bridge in the RH-from-RCL route. UnifiedRH already shows that nonzero-charge realized defect families possess a concrete collapse scalar approaching zero; the open content is whether this collapse transports to the T1-bounded Euler ledger. A BoundaryTransportCert is the structure carrying an EulerBoundaryBridgeAssumption that encodes exactly this transport. A DefectSensor records the integer charge (multiplicity of the zeta zero) together with its real part. CostDivergent asserts that the annular cost exceeds every bound when the mesh winding equals the sensor charge. Upstream, DivergenceWitnessesBoundary is the class stating that cost divergence forces the ledger state toward the T1 boundary, and euler_boundary_bridge supplies the explicit instance of that class.
proof idea
The proof is a term-mode one-liner. It first obtains the PhysicallyRealizableLedger instance for the sensor via euler_physically_realizable. It next constructs the DivergenceWitnessesBoundary instance by applying euler_boundary_bridge to the certificate's bridge field and the sensor. It then feeds the admissible Euler trace (from euler_trace_admissible) into ontological_exclusion_of_realizable to conclude the negation of CostDivergent.
why it matters
This theorem is invoked inside no_strip_zeros_of_decomposed_data to rule out every right-half-strip zero of the zeta function. It completes the boundary transport step that links the concrete collapse scalar of UnifiedRH to the Euler ledger, thereby closing the physical realizability gap in the RH-from-RCL derivation. Within the Recognition Science framework it reinforces the prohibition of divergent costs for realizable sensors, consistent with J-uniqueness and the eight-tick octave. It touches the remaining open question of whether the full boundary transport certificate can be discharged from the RCL alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.