auditCost
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not compute J-cost increases for any output.
- Does not depend on parameters from other modules.
- Does not generalize the cost beyond the constant value 1.
Lean usage
theorem audit_is_O1 : auditCost = 1 := rflformal statement (Lean)
26def auditCost : ℕ := 1
proof body
Definition body.
27