defect_one_div_one_add
plain-language theorem explainer
The theorem supplies the closed-form T1 defect for the reciprocal-affine proxy 1/(1+t) under the defect functional. Modelers of bounded scalar proxies in Euler carriers cite the identity when deriving uniform T1 bounds from the gap parameter. The proof is a direct algebraic reduction: unfold defect and J, clear the denominator, then normalize the polynomial identity.
Claim. For every real number $t$ with $t ≥ 0$, the T1 defect of $1/(1+t)$ equals $t^2 / (2(1+t))$, where the defect functional is the map $x ↦ J(x)$ from the Law of Existence.
background
The Unified RH module constructs a T1-bounded realizability architecture that separates cost divergence from Euler trace admissibility. The defect functional is defined by defect(x) := J(x) for positive x, where J satisfies the Recognition Composition Law and vanishes at unity. This supplies the explicit value on the form appearing in the Euler scalar proxy construction used to realize the ledger.
proof idea
Unfold the definitions of defect and J. Introduce the auxiliary fact that 1+t ≠ 0 via linarith. Apply field_simp to clear the denominator, then finish with ring to confirm the resulting polynomial identity.
why it matters
The identity is invoked inside eulerScalarProxy_defect_bounded to obtain the uniform bound K = (eulerScalarGap sensor)^2 / 2 and inside defect_realizedDefectCollapseScalar for the realized collapse scalar. It closes the step from euler_trace_admissible to PhysicallyRealizableLedger in the module's proof chain. In the Recognition framework it supports T1 control needed to keep scalar proxies away from the Berry creation threshold phi^{-1} while preserving the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.