Alignment Workspace

Item 125: Distance-to-region conformance for the rowwise enforcer

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

The rowwise enforcer's guarantee is per row: every excess at most tol (WarrantForce.WarrantSchedule.excess_le_tol). The projection enforcer's is a distance: dist2 (market n) (target n) ≤ tol (EffectiveRepresentation.end_to_end_of_constraints_effective), and the Normative-Inductor page states conformance in that form. Neither implies the other without a constant: from rowwise excesses the distance to the region is bounded by a Hoffman constant of the row system, which depends on the bundle and is not computed anywhere. Wanted: either the Hoffman bound for compiled bundles (a function of the rows, computable from the state, so that a distance defect can be declared from rowwise conformance), or a theorem that the displayed-excess defect of WarrantInductor.Problem.defectOf is the right public defect for every adapter the program will use — and then the two enforcer architectures share one interface, or one is retired.

Deliverable shape: lean-proved either way; if the Hoffman route, the constant as a def on Bundle with its bound. Acceptance check: the Lean audit clean; the witness's bundles re-run. Context: .../2026-10-22-normative-inductor-integration/HANDOFFS.md (the conformance arrow); ProjectionForce.dist2. Consumed by: any unification of the projection and rowwise enforcers; the wiki's conformance statement.

Deliverable shape: lean-proved either way; if the Hoffman route, the constant as a def on Bundle with its bound.

Acceptance check: the Lean audit clean; the witness's bundles re-run.

Registered results bearing on this item

None registered.

Where it hangs

Rounds and decisions that touch it