# Independent semantic audit of the complete Theorem B route

Source review: 2026-09-13, 11:29–11:32 UTC. Reviewer: the Enflo/smoothing agent. The reviewer authored the scalar maximum/majorant/truncation/noise-decay branch, but did not author the final theorem, the AL alternative, finite Grothendieck proof, interval summing transfer, intrinsic realification, or arbitrary-copy transport. Independence applies to those latter components; the smoothing branch also has a separate audit by the finite-Grothendieck agent.

**Source review, native endpoint, central type/axiom review, and full project-source rebuild: PASS. No semantic mismatch found. MainTheoremB passed warning-free at 11:37:18 UTC on 2026-09-13, ThirdProofReview passed at 11:38:13 UTC, and the frozen 222-source rebuild passed at 12:03:42 UTC.**

## Reviewed target and exact witness

`PL1/Statements.lean` SHA-256 `6ADC0894C6EE4F091160CBC77FFD39AFD6AFD1B6A6E369E1A0DA97653C6DC6B3` defines the unchanged eight-clause `TheoremBSpec`. `PL1/Definitions.lean` hash `1B56C4F85EBA48B6CBDE93D8CB7674CDA5C7227E8671FE2618F7B2DC1020D5F4` defines the actual interval L1, Hilbert sequence space, copies, and numerical bound. `PL1/LatticeDefinitions.lean` hash `3007A7906E5E8CA773BA81863BA82E796AAB0E96B9C3A87B1682AEBC11376604` defines the equivalent-lattice-norm obstruction.

The reviewed `PL1/MainTheoremB.lean` source has hash `EB8D34075256768803F6AE87154FA2A7FD2C05E07EACF04FFF63BDCA69DD8C72`. Its named witness is exactly `Noise.intervalProjection K Noise.constantRates`. Every conjunction field refers to that witness and its inherited range norm:

1. Actual continuous linear idempotent on interval L1.
2. Operator norm at most `projectionBound`, defined literally as `4 + 3 * Real.sqrt 2`.
3. Closed actual operator range.
4. Infinite-dimensional actual range.
5. Closed isomorphic scalar `Ell2 K` copy.
6. Absence of a closed isomorphic scalar `IntervalL1 K` copy.
7. Failure of the Schur property tested against the entire continuous scalar dual.
8. Absence of any compatible real lattice order and solid equivalent norm on the explicit underlying real range.

`ContainsIsomorphicCopy` includes a closed submodule and a continuous linear equivalence with continuous inverse. The sixth clause is consequently stronger than a prohibition on complemented copies, and is not replaced by absence of an injective operator or a single dyadic trace test. The eighth clause permits arbitrary lattice orders and equivalent norms; it is not restricted to the original norm being a lattice norm.

`theoremB` takes only a scalar field and its `RCLike` instance. The real and complex specializations have the exact original target names. There is no structural theorem premise at the final declaration. The source is universe-polymorphic in the scalar type; final elaboration and the central `#check @PL1.theoremB` are the evidence for those universe parameters.

## Arbitrary-copy exclusion

`PL1/EnfloNoL1.lean` (reviewed hash `FBC5DAF1717912A985CE1BFE025BD96FEBEA6A65F457976100128D08729EF42D`) explicitly discharges the generic operator-decay hypothesis with `EnfloBush.noise_comp_dyadicVanishing`. Its dyadic operators are the actual constant-rate resolvents. The generic resolvent closure uses the proved operator-norm estimate for `C_u R_t-R_t`, not a presumed operator-norm Bochner integral.

The coordinate-majorant argument uses actual increasing dyadic variation sums, with a bound uniform over every finite coordinate subset. This supplies a summable coordinate majorant. The flattening identity is proved for actual counting-product Haar L1; the whole maximum mass is the sum of coordinate maximum masses. This matters because mere coordinatewise convergence would not suffice in an ell1 sum.

The real and imaginary scalar maps are actual Lp continuous linear maps. They commute with the actual scalar convolution and therefore the actual intrinsic analysis coordinates. The intrinsic norm obeys `‖x‖≤‖realPart x‖+‖imagPart x‖`. `EnfloTwoMaps` puts both maps into the first two coordinates of a genuine ell1 sum, whose norm is exactly the sum of their norms. It never supposes that one component alone is bounded below.

An actual closed copy gives a bounded-below source operator using the inverse norm plus one, so no nonzero-inverse edge case is omitted. The contradiction excludes real interval-L1 copies in the natural real scalar space for every `RCLike K`. The actual projection-range identity and the actual interval range equivalence transport this conclusion. `scalar_L1_copy_contains_real_L1` supplies the reviewed scalar no-copy clause. A separate theorem names the explicit restricted-scalar version, preserving the inherited additive group and norm.

## Nonlattice conclusion and discharged assumptions

The hypothetical equivalent lattice norm is eliminated through `HasEquivalentRealLatticeNorm.elim_separable`, producing a separate complete separable Banach-lattice model and a real continuous linear equivalence. This does not install a new norm on the constructed projection range.

The range inclusion and projection restriction give an actual complemented copy. Transport across the equivalence and the actual real interval embedding/retraction yield a complemented Banach lattice in real interval L1. Thus the complex-to-real ambient step is an explicit pair of maps, not an assertion that complex L1's original norm is a real AL norm.

`PL1/ALAlternative.lean` (reviewed hash `46249B61A963C18DBAF80223354EAA448924A61DF8F201E7944FAE9252B39A7E`) has an endpoint taking only that actual complemented copy and the Banach-lattice/separability instances. It discharges its finite summing hypotheses using the proved real constant 128. The finite target `EllOne` is PiLp with exponent one; finite Hilbert targets are Euclidean; ordinary Pi domains use their supremum norms. The actual dyadic analysis/synthesis maps are contractive, and pointwise norm convergence transfers the constant independently of the partition level.

The disjoint-to-positive lower-one bridge was separately reviewed in `LOWER_ONE_INDEPENDENT_AUDIT.md`. The AL renorming takes a supremum over positive finite decompositions with proved upper/lower bounds. Its atomic branch supplies an isometric embedding into scalar ell1 and hence Schur. Its non-atomic branch supplies actual equal-mass fragments, compatible maps on the interval dyadic subspaces, a norm limit, and a closed isometric interval-L1 range. No full measure-space representation theorem is assumed.

The alternative therefore gives either real Schur, transported to scalar Schur through the proved real/scalar equivalence, or a real interval-L1 copy transported back to the original range. Both contradict already proved properties of the same constant-rate witness. The older conditional classification/extraction definitions remain imported for elementary transport APIs, but are not hypotheses used by this final proof.

## Native endpoint evidence

The final `MainTheoremB.lean` was reread after its namespace qualification repair. Relative to the initial source reviewed above, `open ComplementedLattice` became the unambiguous `open PL1.ComplementedLattice`; the mathematical statement and proof did not change. The final SHA-256 is `EB8D34075256768803F6AE87154FA2A7FD2C05E07EACF04FFF63BDCA69DD8C72`.

The reviewer directly read `verification/MainTheoremB-20260913T113706112Z/status.json`, stdout, stderr, and recomputed the current source hash. Status is PASS, exit code zero, source hashes agree before/after/current, elapsed native time is 12.19 seconds, and stdout/stderr are empty. The completed native check finished at `2026-09-13T11:37:18.3500672Z`. This validates the universe-polymorphic endpoint and both exact scalar specializations. It does not itself print the transitive axiom list; that belongs to `ThirdProofReview`.

The final `EnfloNoL1.lean` was also reread after its explicit real continuous-linear-equivalence bundling repair. That repair retains the original range equivalence's functions and continuity, and restricts its linear equivalence to real scalars. Its current hash is `FBC5DAF1717912A985CE1BFE025BD96FEBEA6A65F457976100128D08729EF42D`, matching native PASS `verification/EnfloNoL1-20260913T113502496Z`, completed at 11:35:16 UTC. The final `ALAlternative.lean` hash quoted above matches native PASS `verification/ALAlternative-20260913T112719359Z`, completed at 11:27:30 UTC.

## Central type and axiom evidence

The reviewer directly read the completed central status, full stdout and empty stderr in `verification/ThirdProofReview-20260913T113803363Z`. The check is PASS, exit code zero, 10.51 seconds, completed at `2026-09-13T11:38:13.9200588Z`. Before/after/current source hashes agree at `1F46A6DF4070B0D0BACF4E967CED3CE3EB7D86BB38FE4B60513A14796F2E8646`. The output prints the original `TheoremBSpec`, its real and complex target aliases, and the universe-polymorphic type `∀ K [RCLike K], TheoremBStatement K`. The exact target examples and the combined `MainTheoremsStatement` example elaborate successfully.

Every printed axiom report contains only `propext`, `Classical.choice`, and `Quot.sound`, including `theoremB`, `theoremBReal`, `theoremBComplexStrong`, the unconditional matrix Grothendieck constant, the full complemented-AL alternative, actual smoothing, summable coordinate domination, actual flattening, real/imaginary graph norm bound, and both natural/explicit-underlying real no-L1 statements. There is no `sorryAx`, structural axiom, or extra premise on the final endpoints. The output also verifies the separate natural and restricted-real no-copy types and the unrestricted scalar universe of the final theorem.

## Full frozen project-source rebuild

The reviewer independently read the completed build record at `verification/Project-20260913T113917105417Z/status.json` and all 222 module logs. Its final status is PASS. Every module has native exit code zero, and every corresponding log contains the native PASS result. There are 222 distinct compiled source paths, exactly matching both the build's source snapshot and the current `PL1/`, `BanLat/`, and aggregate `PL1.lean` inventory.

The build started at `2026-09-13T11:39:17.1054170Z` and finished at `2026-09-13T12:03:42.5955630Z`. The recorded elapsed duration is 1465.469 seconds, approximately 24 minutes 25.47 seconds. The build status file SHA-256 is `EC5DA806850A84EB4BDAD040DBC1D9B3B920DB31F754D0F03983E8F271AD4181`.

At approximately 12:04 UTC, the reviewer recomputed SHA-256 for every one of the 222 current Lean sources and compared each with both the recorded before-build and after-build hashes. All 222 before/after/current triples are identical; there are no missing, additional, duplicate, or differing source paths. This verifies that the compiled final source snapshot is the delivered current source snapshot.

The precise scope is all delivered project source, with pinned compiled dependencies reused. This is a full rebuild of those 222 local sources, including the delivered BanLat sources; it is not a fresh rebuild of Mathlib and every external dependency. The build explicitly records `fullFreshVerification: false`.

## Exposition and scope

`THEOREM_B_PROOF_ROUTE.md` was read in full. Its direct construction proof, positive-time exponent, clipping bound, coordinate domination, two-part realification, and lattice alternative agree with the current sources. It correctly distinguishes this route from a full Enflo–Starbird extraction proof. No assertion that the inaccessible 1979 full proof was read or formalized is needed.

This review checks the endpoint meaning and its mathematical dependency route. The native endpoint, central type/axiom review, and frozen full project-source rebuild have all passed. No additional compiler was launched by this reviewer for the final audit.