Structured
plain-language theorem explainer
Structured defines a Boolean predicate on source strings that returns true precisely when parsing succeeds and staticChecks reports ok. LNAL compiler users and CPM bridge developers invoke it to gate inputs before defect evaluation. The definition matches on the parse result, feeds the code or empty array to staticChecks, and projects the ok flag.
Claim. For a program source string $s$, let $p$ be the result of parsing $s$. Then Structured$(s)$ holds if and only if staticChecks applied to $p$ (or to the empty program on parse failure) returns a report whose ok component is true.
background
The CPM.LNALBridge module supplies minimal surrogates that connect LNAL compiler output to the Recognition framework. Structured acts as the validation gate for structured-set membership by testing static well-formedness. It imports parseProgram and staticChecks from LNAL.Compiler together with the core defect and A primitives from Foundation and Masses layers.
proof idea
The definition is a direct one-line computation. It matches the parseProgram result on src, applies staticChecks to the extracted code or to the empty array on error, and returns the ok field of the report.
why it matters
Structured supplies the Boolean guard for the sibling Defect definition, which returns zero precisely when Structured holds. Defect in turn feeds the nothing_cannot_exist theorem in LawOfExistence, which states that for any bound C there exists epsilon such that defect x exceeds C for all sufficiently small positive x. This closes the bridge from compiler-level validation to the claim that nothing cannot exist, consistent with the defect functional equaling J and the active-edge count A fixed at 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.