Extend formal Gaussian coverage beyond the current [-6,6] core admission rule

[AnubisQuantumCipher]

Summary

The current proof-carrying Gaussian integral lane correctly refused a pair of near-boundary requests because their transformed intervals do not satisfy the present certified-core admission rule. This is not a soundness failure; it is a formal coverage limit that should be logged explicitly if JACKAL is expected to cover one-sided or truncated Gaussian tails in the future.

Verified behavior

Both formal requests refused:

A = ∫_0^0.2 exp(-10^6 (x-0.198)^2) dx
B = ∫_0^0.2 exp(-10^6 (x-0.199)^2) dx

Tool result for both:

{
  "status": "refused",
  "reason": "producer-refused",
  "detail": "REFUSED reason=transformed interval does not contain the certified central interval"
}

This matches the current implementation and docs:

• tools/gaussian_certificate.py:22 sets CORE = 6
• tools/gaussian_certificate.py:134-137 refuses unless the transformed interval contains the certified central interval
• README.md:134-140 documents the current admission rule as requiring the transformed interval to contain [-6,6]

Exact transformed intervals

Using exact rational arithmetic with scale 1000:

For A, mu = 99/500:

1000*(0 - 99/500)   = -198
1000*(1/5 - 99/500) = 2

so the transformed interval is:

[-198, 2]

For B, mu = 199/1000:

1000*(0 - 199/1000)   = -199
1000*(1/5 - 199/1000) = 1

so the transformed interval is:

[-199, 1]

Neither interval contains [-6,6], so the current formal lane correctly refuses both.

Why this follow-up matters

This test is still valuable because it shows the system knows where theorem-covered formal coverage stops. If JACKAL should cover narrow one-sided / truncated Gaussian tails near a boundary, the formal family needs to be extended rather than silently downgraded.

Requested follow-up

Extend the formal Gaussian family to cover one-sided / truncated-tail requests like these only if the new proof/checker construction remains fail-closed and exact-request-bound.

At minimum, any extension should:

1. preserve the current theorem-covered family and its exact request binding;
2. add a distinct admitted construction for truncated / one-sided tails instead of loosening the present core rule without proof;
3. continue to refuse unsupported requests with no downgrade;
4. keep the downstream claim algebra honest: even with individually formal-bounded component integrals, ordinary interval subtraction in the current claim kernel caps the composed A-B result at mathematical=bounded, so a final safety-critical decision should still refuse on the mathematical floor.

Non-claim

This is not evidence that the current Gaussian formal lane is unsound. It is evidence that the present admitted family is narrower than “all Gaussian-looking finite intervals,” and the refusal is behaving correctly.