pith. machine review for the scientific record. sign in
def definition def or abbrev high

Defect

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  17def Defect (src : String) : Nat := if Structured src then 0 else 1

proof body

Definition body.

  18
  19end CPM
  20end IndisputableMonolith

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.