Item 82: Aggregation laws with several parents

OccurrenceIntegrity.LocalLaw transforms one requirement into successors with maps of resolution witnesses in both directions. A genuine aggregation (r₁, r₂) ↦ c — one successor resolved only by resolving both parents jointly — is not expressible: each parent would need its own law, and the no-growth map of each demands that the parent alone resolves c. No landed theorem or application needs aggregation; it is filed so that the limitation is a recorded boundary rather than a discovered one.

Settle whether an application needs it. If so, add a law with a finite family of parents, a joint no-growth map from the parents' witnesses to the successor's, and a faithful-carry map back to each parent, and re-prove Program.evaluate_subst, terminals_subst and livePorts_subst for accounts that share such a node across occurrences.

Deliverable shape: the extended law and the three re-proved lemmas, with a witness in which two occurrences are jointly closed by one successor and neither alone. Acceptance check: the module audits clean and python3 tests/run.py is green.

Context: READINESS.md §1 of the final pressure pass; OccurrenceIntegrity.lean, the LocalLaw docstring. A solution ships: the extension, or a statement that no application needs it.