# Induction and case composition over verified constructions

2026-09-05. Outcome: one checked union of twelve infinite families and two
individual instances. Universal prime coverage remains unproved.

## The combined judgment

Let C_i be the domain of construction i, and suppose its SWC certificate proves
existence at every n in C_i. Define U_k=C_1 union ... union C_k.

Induction on k establishes existence for every n in U_k:

* The base is the first checked construction.
* At the successor, n in U_{k+1} is in U_k or C_{k+1}. Apply the corresponding
  checked certificate.

This is proof by cases over domains. It is not a probability mixture of
different target integers. For a fixed n in the union, one can select a
covering case and use its accepted witness distribution. The kernel keeps
case unions and same-target probability mixtures as different rules.

The family certificates themselves use symbolic identities valid for all
permitted parameters, compatible with the previous single or double induction
arguments. Thus the proof combines family-level universal statements and
case-level induction, while retaining their exact domains.

## Checked bundle

The bundle includes:

1. The six hard-residue progressions from swc-six-targeted-families.md.
2. The double family n=4(3u+2)(v+1)-3, covering the shift-3 factor condition.
3. Three shift-7 families n=8(7u+r)(v+1)-7, r=3,5,6.
4. The p+1 family n=(4u+3)(4v+2)-1.
5. The p+4 family n=(4u+3)(4v+3)-4.
6. Explicit witness instances at n=73 and n=8803369.

All parameters are nonnegative integers. Each of the twelve family identities
is checked by exact polynomial coefficient comparison, with sufficient
positivity and integrality conditions. Each individual triple is checked
against 4xyz=n(xy+xz+yz). The complete certificate has fifteen nodes:
twelve families, two instances, and one case-union node.

The shift-7 parametrizations include the sufficient prime-factor construction:
if C=(p+7)/4 is even and contains an odd nonresidue prime r modulo7, then
C=2rS and r=7u+r0 for r0 in {3,5,6}.

The last two polynomial families cover the sufficient p+1/p+4 filters:
the relevant divisor is 4u+3, and the cofactor's residue modulo4 determines
4v+2 or 4v+3 respectively. These are explicit repackagings of the existing
constructions, not originality claims.

## Where all-prime induction would enter

The case induction proves

    n in U => existence for n.

A full proof still needs either every prime to belong to U, or a theorem
giving a sound reduction for each prime outside U into already certified
instances. A smallest-prime induction cannot fill that missing branch merely
by assuming smaller primes have some witnesses: the reduction must preserve
the target equation and the required witness compatibility.

For example, 806521 lies outside this particular bundle's symbolic union.
Its shifted factors are

    (p+3)/4 = 163*1237,
    (p+7)/4 = 2^5*6301,
    p+1 = 2*403261,
    p+4 = 5^2*32261.

The shift-3 factors are all 1 mod3; the shift-7 factors are quadratic residues
mod7; the p+1/p+4 factors have no 3-mod4 prime factor. It belongs to none of
the six listed progressions. Earlier computations already give this prime
an individual witness, so it is not a counterexample to Erdős–Straus.
Adding that witness would expand the finite part of the bundle, not prove
the unbounded remaining coverage assertion.

## Kernel behavior

The new case_union rule outputs a union_of_verified_domains judgment.
It rejects zero-mass instance cases and caller-supplied claims of all-prime
coverage. It cannot merge differently targeted instances through the mixture
rule. The extended suite has 24 passing tests, including the saved combined
certificate.

The implementation is an exact-arithmetic Python prototype, not a
proof-assistant formalization. No large prime sweep or public publication
change was performed.

Reproduce:

    python3 -B research/build_swc_case_union.py --out research/evidence/swc-combined-cases.json
    python3 -B research/swc_certificate_kernel.py research/evidence/swc-combined-cases.json
