# Double induction: verified two-parameter family and scope

2026-09-05. Outcome: symbolic verification of an infinite two-parameter
family. Universal Erdős–Straus coverage remains unproved. The identity is an
instance of the earlier shift-3 construction, not a claim of new number theory.

## Explicit family

For nonnegative integers u,v, define

    B=3u+2, S=v+1, Q=u+1,
    n=4BS-3=12uv+12u+8v+5,
    x=BS, y=nQS, z=nBQS.

All are positive integers and n>=5. Because B+1=3Q,

    1/x+1/y+1/z
      = (nQ+B+1)/(nBQS)
      = Q(n+3)/(nBQS)
      = 4/n.

Thus the family theorem holds for every u,v>=0. Point mass on this explicit
witness is a normalized SWC distribution with accepted mass one.

## Nested induction organization

Let P(u,v) assert the displayed parameter relations, integrality, positivity
and the witness identity.

For a fixed u, the inner induction runs over v:

* At v=0, S=1 and the displayed algebra proves P(u,0).
* At v+1, S increases by one and n increases by 4B. The identity B+1=3Q
  is unchanged, and the same algebra proves the successor witness.

The outer induction runs over u, with claim forall v>=0, P(u,v).
The row u=0 follows from the inner argument. At u+1, replace B by B+3
and Q by Q+1. This preserves B+1=3Q, supplies the next row's v=0 base,
and the inner induction establishes the entire row.

The explicit identity is sufficient for these steps without using every
induction hypothesis. Double induction is a valid way to organize the family
proof; it does not add a coverage conclusion to the identity.

## Checker extension

The kernel now supports polynomial_family_2d and instantiate_2d.
A coefficient matrix entry [i][j] represents the coefficient of u^i v^j.
The family checker verifies the entire polynomial identity

    4xyz=n(xy+xz+yz)

by exact coefficient multiplication, and checks sufficient nonnegative
coefficient conditions for integrality and positivity over all u,v>=0.
It reports the target polynomial as its scope.

It does not attempt to validate arbitrary induction proofs. Its implemented
proof rule is symbolic polynomial identity plus positivity. The mathematical
induction organization above explains the resulting family theorem.

The tests include changed mixed coefficients, negative parameters, family
instantiation and forged claims of all-prime coverage. All 20 tests pass.
This is an exact-arithmetic Python prototype, not a Lean/mathlib development.

## Coverage is a separate theorem

An integer n occurs in this family exactly when (n+3)/4 factors as BS
with B>=2 congruent to 2 modulo 3 and S>=1.

For p=73, (p+3)/4=19, whose divisors 1 and 19 are both 1 modulo 3.
Therefore no u,v in this family produce 73. Other previously verified
constructions do solve 73; this demonstrates a gap in this family's coverage,
not a counterexample to Erdős–Straus.

To complete the universal conjecture using a union of families, one must
still prove that every target prime is in at least one verified family,
or is covered by a separate positive-mass or descent certificate. The
double induction does not establish that assertion.

More general lexicographic induction on two ranks has the same obligation:
every nonbase target must have a proved transition to a smaller rank pair,
and every terminal branch must be accounted for. Nested loops alone do not
guarantee positive witness mass at their starting states.

Run the symbolic certificate:

    python3 -B research/swc_certificate_kernel.py research/evidence/swc-kernel-double-family.json

Run tests from the research directory:

    python3 -B -m unittest test_swc_certificate_kernel

Only small coefficient calculations and tests were used; no prime sweep ran.
