# Arithmetic conditioning composed with SWC induction

2026-09-05. Status: elementary conditional improvement theorem, supported by
a separate arithmetic checker. This does not prove universal Erdős–Straus
existence, and no novelty or proof-assistant verification is claimed.

## Domain and necessary character condition

Let a state be (n,x), with n>=2, h=4x-n>=3, h congruent to 3 modulo 4,
and gcd(x,h)=1. Write x=product r_i^e_i. Choose signed exponents z_i
independently and uniformly from [-e_i,e_i]. Set

    R=product r_i^z_i modulo h.

The fixed-anchor Type-II acceptance condition is R=-1. The divisor
d=product r_i^(e_i+z_i) satisfies d|x^2 and d=-x modulo h. The corresponding
positive integers b=(x+d)/h and e=(x+x^2/d)/h give the desired witness
(x,nb,ne). The complementary congruence follows from gcd(x,h)=1.

Let chi be the Jacobi character modulo h. Since h is 3 modulo 4,
chi(-1)=-1. Therefore every accepted exponent vector satisfies chi(R)=-1.
Conditioning on this necessary property cannot discard an accepted vector.
It need not make an accepted vector exist.

## Exact conditioning probability

For chi(r_i)=+1 the local character expectation is one. For chi(r_i)=-1,

    E[chi(r_i)^z_i] = (-1)^e_i/(2e_i+1).

Independence therefore gives

    eta = E[chi(R)]
        = product_{i: chi(r_i)=-1} (-1)^e_i/(2e_i+1),
    Z = Pr(chi(R)=-1) = (1-eta)/2.

This normalization depends on the arithmetic character of the prime factors,
not on finding a valid witness. If no factor has negative character, eta=1,
Z=0 and the original acceptance mass is zero. In that case the procedure
returns rejection rather than conditioning on a null event.

Otherwise -1/3<=eta<=1/5:

* If eta<0, its denominator is at least 3.
* If eta>0, the sum of the negative-character exponents is positive and even,
  hence at least 2. The product of (2e_i+1) is at least
  1+2 sum e_i, hence at least 5.

Consequently

    2/5 <= Z <= 2/3.

If D is the original direct accepted mass, the conditioned mass is D/Z.
Thus, including the zero-mass case with the explicit rejection convention,

    (3/2)D <= D_conditioned <= (5/2)D.

For positive D, the improvement is between 1.5 and 2.5. This compares with
uniform signed exponents; it is not a claim about every previously tested
proposal distribution.

## Nested recursion and induction

The eligible recursive edges are divisors L>=2 of x with

    y=x/L, q=4y-h>=2.

They preserve h and coprimality. Also y<=x/2 and q<n/2. A parent witness
(y,qb,qe) maps to (Ly,Lnb,Lne), which satisfies the identity at n.

Use the same branch probabilities for both samplers: when parents exist,
half the probability goes to the direct branch and half to the uniform
mixture of recursive parents. With no parents, use the direct branch.
Let U(n,x) be its success mass with uniform direct exponents, and C(n,x)
its mass with character-conditioned direct exponents.

Well-founded induction on x proves

    (3/2)U(n,x) <= C(n,x) <= (5/2)U(n,x).

At a leaf this is the preceding direct bound. At an internal node multiply
the direct and parent inequalities by their common nonnegative branch
weights and add. Every recursive call decreases rank, so the proof reaches
the leaves after finitely many levels. Soundness and normalization follow
by the same induction and the exact witness transformer.

This is a theorem for every state in the stated domain. It is a comparison
theorem, not a theorem asserting positive mass at every state. In fact it
implies C>0 if and only if U>0. Improving probabilities cannot bridge the
missing universal witness-coverage premise.

## Verified examples

| n | First denominator x | Uniform recursive mass U | Conditioned recursive mass C | Gain |
|--:|--:|--:|--:|--:|
| 73 | 19 | 0 | 0 | undefined |
| 73 | 20 | 41/270 | 41/180 | 3/2 |
| 241 | 63 | 23/270 | 23/180 | 3/2 |
| 1249 | 315 | 20/243 | 10/81 | 3/2 |
| 118801 | 29715 | 301/12960 | 301/8640 | 3/2 |
| 2458369 | 614606 | 29/2106 | 7/234 | 63/29 |
| 8803369 | 2200869 | 253/51300 | 253/34200 | 3/2 |

These are fixed-anchor Type-II distributions, so they must not be compared
directly with earlier all-shift or two-target masses.

The producer computes Jacobi symbols with the Euclidean algorithm and
residue masses by convolution. The separate verifier imports no producer
modules: it factors the modulus, evaluates characters through Euler's
criterion, enumerates divisors, checks all accepted witness identities and
recomputes the mass recurrence. It also rejects a forged mass value.

The recorded artifact contains 83 states. The general proof is the argument
above; the finite arithmetic audit does not replace a formal proof of it.
No Lean/mathlib verification was performed.

## Reproduction and resource scope

    python3 -B research/swc_character_induction.py --out research/evidence/swc-character-induction.json
    python3 -B research/verify_character_induction.py research/evidence/swc-character-induction.json

These commands use the listed small collection of factorized states, not a
dense sieve over millions of integers. The continuation after the reported
computer crash avoids large prime sweeps and parallel numerical searches.
