Defect
plain-language theorem explainer
Defect supplies a binary natural-number indicator for source strings in the CPM LNAL bridge. It returns zero precisely when the string satisfies the Structured predicate and one otherwise. Cost-algebra authors cite it to seed the defect distance d(x,y) = J(x/y). The definition is a direct conditional that delegates the check to the sibling Structured predicate.
Claim. For a source string $src$, define the defect as $0$ if $src$ is structured (its parsed program passes static checks) and $1$ otherwise.
background
The CPM module implements a minimal surrogate for structured sets: programs appear as strings that must survive static checks. The sibling Structured definition parses the input via parseProgram and then runs staticChecks, returning true only when the resulting representation is valid. Defect then maps this Boolean outcome to a Nat cost of zero or one. The module setting is therefore a lightweight bridge between LNAL compiler output and the J-cost algebra.
proof idea
The definition is a direct conditional expression that evaluates Structured src and returns 0 or 1 accordingly. No lemmas or tactics are invoked; it is a primitive one-line definition.
why it matters
Defect feeds the binary deviation indicator into defectDist and its derived properties (non-negativity, symmetry, self-distance zero) inside CostAlgebra. Those properties in turn support the defect pseudometric used for J-cost calculations that appear in the phi-ladder mass formulas and the T5–T8 forcing chain. It therefore closes the LNAL-to-algebra link required for the Recognition framework’s cost accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.