bridge_contradiction_core
plain-language theorem explainer
The theorem shows that no physically realizable ledger can satisfy the boundary-approaching condition on its scalar proxy states. Researchers closing the unification bridge for nonzero charge in Recognition Science cite it to obtain the final contradiction. The proof is a one-line term application of the lemma that T1 defect bounds forbid boundary approach.
Claim. Let $sensor$ be a defect sensor equipped with a physically realizable ledger, so that its scalar proxy states $x_N$ satisfy $x_N > 0$ and possess a uniform T1 defect bound. If the ledger is boundary-approaching, meaning that for every $ε > 0$ there exists $N$ with $x_N < ε$, then a contradiction follows.
background
The module replaces an earlier total-cost bound with a three-component T1-bounded realizability architecture. CostDivergent records that nonzero charge forces annular cost to diverge. EulerTraceAdmissible supplies a convergent Euler carrier with bounded logarithmic derivative. PhysicallyRealizableLedger packages these into a sensor-indexed class whose scalarState $N$ is positive and whose T1 defect remains uniformly bounded. BoundaryApproaching is the auxiliary definition that the scalar states can be driven arbitrarily close to zero. The module's proof chain runs from Euler admissibility through the realizable-ledger instance to the external bridge hypothesis that would force boundary approach, which T1 then forbids.
proof idea
The proof is a direct term application of the lemma physicallyRealizableLedger_not_boundaryApproaching to the given sensor and the boundary-approaching hypothesis. That lemma encodes the T1 prohibition: a uniform defect bound on the scalar states contradicts the requirement that nothing can exist at the boundary.
why it matters
The declaration isolates the logical core of the bridge contradiction for nonzero charge, as stated in the module doc-comment. It completes the chain from proved EulerTraceAdmissible and PhysicallyRealizableLedger instances to the T1 boundary prohibition, thereby discharging the final step in the T1-bounded realizability architecture. No downstream uses are recorded yet; the result remains internal to the unification bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.