safe_when_small
The declaration states that for real numbers impact and eps, the absolute value of impact being less than eps follows immediately from the assumption. It would be cited in O(1) safety verifications within the Sigma Externalization Audit when confirming that small perturbations leave another agent's J-cost unchanged. The proof reduces to a direct return of the hypothesis without lemmas or calculation.
claimIf $|impact| < eps$, then $|impact| < eps$.
background
The module implements G-VII-1: Sigma Externalization Audit, an O(1) check per output to determine whether it increases another agent's J-cost. J-cost is the Recognition Science function J(x) = (x + x^{-1})/2 - 1, also written cosh(log x) - 1. This theorem supplies a basic inequality preservation step inside that audit process. The local setting assumes real-valued impacts and tolerances with no further structure imposed on eps.
proof idea
The proof is a one-line wrapper that applies the hypothesis h directly as the conclusion.
why it matters in Recognition Science
It supplies a trivial bound check that supports the O(1) audit mechanism for J-cost increases in the ethics module. The declaration aligns with the Recognition Science forcing chain (T0-T8) by preserving small-defect conditions on the phi-ladder. No parent theorems or downstream uses are recorded, leaving its integration into isSafeOutput or auditCost as an open extension point.
formal statement (Lean)
23theorem safe_when_small (impact eps : ℝ) (h : |impact| < eps) :
24 |impact| < eps := h
proof body
25