auditCost
plain-language theorem explainer
The definition assigns the natural number 1 to the audit cost. Researchers working on sigma externalization would cite this constant when confirming that the per-output check runs in constant time. It is supplied as a direct definition with no computation or dependencies.
Claim. The audit cost is defined to be the natural number $1$.
background
The Sigma Externalization Audit module implements G-VII-1: an O(1) check per output that determines whether the output increases another agent's J-cost. J-cost denotes the Recognition Science quantity J(x) = (x + x^{-1})/2 - 1. The module imports only Mathlib and contains no sorry statements.
proof idea
The declaration is a direct definition that sets auditCost equal to 1.
why it matters
This definition supplies the constant referenced by the theorem audit_is_O1, which proves auditCost = 1 by reflexivity. It fills the fixed-cost slot in G-VII-1 within the Ethics domain. The constant 1 keeps the audit O(1) independent of output size.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.