defect_one_div_one_add
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove existence or convergence of the Euler scalar proxy.
- Does not derive the gap bound eulerScalarGap itself.
- Does not control annular costs or total defect divergence.
- Does not extend to negative values of t.
formal statement (Lean)
187private theorem defect_one_div_one_add (t : ℝ) (ht : 0 ≤ t) :
188 IndisputableMonolith.Foundation.LawOfExistence.defect (1 / (1 + t)) =
189 t ^ 2 / (2 * (1 + t)) := by
proof body
Tactic-mode proof.
190 unfold IndisputableMonolith.Foundation.LawOfExistence.defect
191 IndisputableMonolith.Foundation.LawOfExistence.J
192 have hden : (1 + t : ℝ) ≠ 0 := by linarith
193 field_simp [hden]
194 ring
195
196/-- The Euler scalar proxy has uniformly bounded T1 defect. -/