Alignment Workspace

Item 79: Convex representability and compiler completeness for a declared requirement class

Deference line — second wave · difficulty open · project normativity · open · node item-79

Compiler soundness, Farkas conflict certification, and conservation on failure are Lean-proved (NormativeInductorComposition §2). What is missing is the object those theorems are about: a class of anchored requirements — in the consolidation's terms, a class of Protocol.Evidence types — for which a sound finite rational-row realization over a security fragment exists, and a compiler complete for that class. Keep the five properties apart: representability of the class, soundness, completeness within the class, joint feasibility of a serviced bundle, affordable enforceability.

Deliverable shape: a Lean definition of the class, a compiler for it, and soundness and completeness theorems with a nonvacuity witness and a requirement outside the class that no row realizes. Acceptance check: the module audits clean and python3 tests/run.py is green.

Context: CONSOLIDATION.md §9.1 of the mathematical-consolidation round; NORMATIVE_INDUCTOR_REALIZATION.md §4 of the realization round for the five properties. A solution ships: the class, the compiler, and the two theorems.

Deliverable shape: a Lean definition of the class, a compiler for it, and soundness and completeness theorems with a nonvacuity witness and a requirement outside the class that no row realizes.

Acceptance check: the module audits clean and python3 tests/run.py is green.

Registered results bearing on this item

None registered.

Where it hangs

Rounds and decisions that touch it

None recorded.