eulerScalarProxy_defect_bounded
plain-language theorem explainer
The Euler scalar proxy state derived from an admissible Euler trace carries T1 defect bounded above by a constant independent of refinement depth N. Researchers modeling physically realizable ledgers in Recognition Science cite this result to confirm that admissible trajectories remain outside the infinite-cost regime. The proof supplies the explicit quadratic bound (scalar gap)^2 / 2 and chains two monotonicity comparisons on the rewritten defect expression.
Claim. There exists a real constant $K$ such that for every natural number $N$, the T1 defect of the Euler scalar proxy state at depth $N$ satisfies defect$(x_N) ≤ K$.
background
The Unified RH module organizes realizability into cost divergence, Euler trace admissibility, and physically realizable ledgers. A DefectSensor indexes hypothetical locations; the Euler scalar proxy supplies the positive scalar state $x_N$ at each refinement depth $N$. The defect functional is the T1 cost from the Law of Existence, which diverges as the state approaches the boundary value zero. Upstream arithmetic lemmas establish ordering on natural numbers and reals, while the scalar gap supplies the uniform distance from zero guaranteed by the admissible Euler carrier.
proof idea
The tactic proof refines the existential quantifier to the concrete bound (eulerScalarGap sensor)^2 / 2. For fixed $N$ it defines $t$ as the gap divided by $N+1$, confirms nonnegativity, rewrites the defect via the one-over-one-plus identity, then applies two comparison lemmas: the defect is at most $t^2/2$ by denominator enlargement, and $t^2/2$ is at most the target bound by monotonicity of squaring. The steps invoke nlinarith on the quadratic inequalities and le_trans to chain the results.
why it matters
This theorem supplies the scalarDefectBounded field of the eulerPhysicallyRealizableLedger instance, completing the proof that the Euler carrier yields a T1-bounded realizable ledger. It occupies the realizability slot in the three-component architecture of UnifiedRH and supports the claim that admissible physical states cannot approach the T1 boundary. The result is consistent with the Law of Existence forbidding zero states and closes one link in the chain from Euler instantiation to physically realizable ledgers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.