# v0.9.0 strict-build failure and corrective candidate

The published commit `ef78e9da90ac3ee854e8c0edf3dc205831cfe697` fails the
configured strict build at `Verification/DeFiAMMIntegerSwap.lean:6:7`.
Both hosted runs failed before the subsequent tests and audits:
[main](https://github.com/solanaqubits/leanbook/actions/runs/40211178946) and
[tag](https://github.com/solanaqubits/leanbook/actions/runs/40211179179).
The failure was independently reported and reproduced in a new local worktree.
The broad `Mathlib.Tactic` import violates the enabled header linter.

## Reproduced cache mechanism

Mathlib's header linter checks whether a module is directly imported by its
library root. A controlled reproduction with the published source showed:

1. With its root import absent, the module builds successfully.
2. Adding that root import leaves the module source unchanged. Lake replays
   the previous artifact and reports a successful build.
3. Fresh elaboration with `lake lean` applies the workspace options and rejects
   the same registered module. The former `lake env lean` invocation passes.

This is a demonstrated mechanism consistent with the observed cache. It does
not establish the historical creation sequence of the original artifact.
Original artifacts, traces and evidence are preserved for the independent audit.
The defect withdraws the release qualification; it does not by itself prove a
false theorem or an unapproved axiom in an existing artifact.

## Corrective changes

- Replace the broad import by the natural-number, linear-arithmetic and
  positivity imports actually needed. Mathematical statements and proof bodies
  are unchanged.
- Use `lake lean` for the verifier's fresh elaboration and generated axiom audit,
  preserving workspace options after the incremental build.
- After registration, integration freshly checks both the candidate and
  `MasterSuite`, rather than elaborating only the importing registry.
- Add a live regression that primes an unregistered module's cache, registers
  it, and requires the verifier to reject its configured header violation.
  The same regression fails against the published verifier.
- Run the new module regression drivers with workspace options. Format the
  existing fixtures to satisfy those options without changing their claims.
- Require the Feldman rejection test to pass a matching valid control and then
  report exactly one unsolved false goal. An arbitrary compiler error is not
  accepted as evidence of rejection.

## Qualification boundary

These are corrective candidate changes, not a replacement release or a completed
semantic audit. Changing verification tooling requires a new full beta gate
before publication. Targeted checks and any successful root build do not replace
that gate. The immutable v0.9.0 tag and original evidence remain available;
v0.8.0 is the last successful beta until a corrected checkpoint is qualified.