Item 63: `Sigma_n` as a computable deductive process

IsLogicalInductor is stated against a process carrying ComputableDeductiveProcess. The slice's Sigma_n = D_n union Sem_L(L_n) is computable by construction and no computability statement is made about it, so E3 in the slice's assumption list is declared rather than discharged. The same gap covers RationalConstraintSchedule.Computation for the schedules the slice generates.

Deliverable shape: lean-proved for the union case — given ComputableDeductiveProcess D and a primitive-recursive sem_L over an enumerable ledger, the union is a ComputableDeductiveProcess. Acceptance check: the lean job; the witness is a settled ledger with a decidable reading. Context: projects/normativity/legitimacy/rounds/2026-08-25-end-to-end-vertical-slice/SETTLEMENT_SEMANTICS.md §1 and §9. Consumed by: any round quoting IsLogicalInductor over a record-fed substrate.