[kreneskyp]

Draft source-backed correction for IR-709. Current generated Boolean, equality, function and pre-check source has seven genuine typed CheckedInvariantCause producer paths. GeneratedUnexpectedOutcome and GeneratedEnvironmentRejected have no producer occurrence in src/oracle; the checked Boolean/function result arms are exhaustive and environment admission does not supply a fallible path for those names. The merged quire-exact FR-369 spec still lists nine assignments; a new owner-side PR must pair with this one if seven is authorized. No code, schema or artifact is copied between repositories.

This draft changes FR-042's nine-producer claim to seven real producers and keeps every actual cause, nested IllTypedCause, charge/failure behavior, downstream replay obligation, and TC-057 verification requirement. It aligns FR-018 AC-8/AC-17 and TC-029 with the existing typed Refusal::CheckedInvariant { cause } payload, including the GeneratedTypeCheckRejected cause carried from check_type. It updates TC-057 and the oracle matrix status. The source scan found the seven producer names in src/oracle/function/mod.rs, src/oracle/equality/mod.rs and src/oracle/boolean_v1.rs, and neither disputed name in src/oracle.

Validation: changed-scope Quire validation and computed matrix analysis passed. The matrix still marks FR-042-AC-1 untagged; FR-018-AC-8 and AC-17 are tagged. TC-057 controls and the seven-producer implementation/evidence slice remain open. Spec-only change: no Cargo, Kani, replay or full CI run.

Decision hold: this proposal reduces FR-042-AC-1's literal count from nine to seven. The direct task instruction says never narrow an AC; this draft will not merge until Peter directly authorizes the source-backed correction or a resolved operator escalation records that decision. Opus spec review found the cross-repository contradiction and left it deferred pending that decision and a new paired quire-exact PR; the remaining findings are in disposition.

Ticket stays open: IR-709 still needs TC-057 tagged proof of all seven real producer paths, payload and charge/failure behavior, plus remaining FR-018 AC-8/17 and TC-029 work. IR-356 remains open for its typed CheckedInvariant parent scope.

[kreneskyp]

Superseded by #579, which preserves all nine FR-042-AC-1 producer obligations and carries the reviewed source-backed wording corrections. This seven-producer draft will not merge.