EBBA_of_cost_finiteness
plain-language theorem explainer
Cost finiteness across all defect sensors implies the Euler boundary bridge assumption in the unified RH architecture. Researchers closing the Recognition Science link between bounded annular cost and realizable ledger transport cite this step. The argument reduces the finiteness hypothesis via the cost-RH equivalence, then applies the already-proved RH-implies-EBBA theorem.
Claim. If the annular cost remains bounded for every defect sensor (i.e., no sensor satisfies CostDivergent), then the Euler boundary bridge assumption holds: for every sensor the collapse boundary transport is satisfied once the Euler physically realizable ledger is instantiated.
background
The module replaces an earlier total-cost bound with a three-component architecture: CostDivergent (annular cost grows unbounded for nonzero charge under uniform winding), EulerTraceAdmissible (convergent carrier with bounded log derivative), and PhysicallyRealizableLedger (T1 defect uniformly bounded for the Euler carrier). EulerBoundaryBridgeAssumption is the remaining transport claim: collapse of the realized defect family must force boundary approach for the bounded Euler proxy. Upstream, cost_finiteness_iff_rh states that universal non-divergence is equivalent to the Riemann hypothesis (no nonzero-charge sensors). EBBA_of_rh states that the Riemann hypothesis implies the boundary assumption vacuously.
proof idea
Term proof that applies cost_finiteness_iff_rh.mp to the universal non-divergence hypothesis, recovering the no-nonzero-charge condition, then feeds the result directly into EBBA_of_rh.
why it matters
The declaration supplies the forward direction from the RS cost-finiteness principle to the Euler boundary bridge assumption inside the T1-bounded realizability architecture. It composes cost_finiteness_iff_rh with EBBA_of_rh, thereby placing the cost model on equal footing with RH for the purpose of ledger transport. The step supports the module's proof chain that moves from admissible Euler trace to boundary approach only when divergence is absent. It leaves open the concrete status of cost finiteness, which remains equivalent to RH.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.