isSafeOutput
plain-language theorem explainer
This definition declares an output safe precisely when its absolute impact on another agent's J-cost lies below a supplied epsilon. It would be invoked in any O(1) externalization audit to certify that a candidate output does not raise recognition cost for other agents. The predicate is introduced by direct abbreviation with no lemmas or reductions.
Claim. An output is safe when its absolute impact satisfies $|impact| < epsilon$, where impact denotes the change in J-cost inflicted on another agent.
background
Module G-VII-1 defines the Sigma Externalization Audit as an O(1) per-output test that checks whether the output increases another agent's J-cost. J-cost is the recognition cost function fixed by T5 of the forcing chain: J(x) = (x + x^{-1})/2 - 1. The present definition supplies the safety predicate used by the sibling functions sigmaImpact, safe_when_small and auditCost.
proof idea
Direct definition that equates the safety predicate to the absolute-value inequality on the two real parameters. No tactics or upstream lemmas are invoked.
why it matters
The definition supplies the core predicate for G-VII-1 in the ethics module. It anchors the O(1) audit to the J-cost already fixed by T5 of the Unified Forcing Chain and thereby closes the externalization check inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.