# Updated PL1 formalisation

**The full reviewed Theorems A and B are proved over both real and complex scalars.** Both retain the original projection bound `4 + 3√2` and the stronger reviewed underlying-real nonlattice conclusion.

**Fresh verification passed:** all 3,399 imported non-toolchain modules were rebuilt from source, the official `leanchecker --fresh` replay passed, and separate raw dependency, axiom and theorem-type inspection passed. See the [fresh verification report](verification/FRESH_VERIFICATION_REPORT.md) and [manuscript inventory](THEOREM_INVENTORY.md).

The preceding 222-source project rebuild passed at 12:03:42 UTC on 13 September 2026, in 24.42 minutes, with 154 standard-axiom reports and no forbidden proof tokens. Its [third construction report](verification/THIRD_CONSTRUCTION_REPORT.md) and [run record](THIRD_THREE_HOUR_RUN.md) remain historical evidence.

## Main results

| Result | Lean source and declarations |
|---|---|
| Full A | [MainTheoremA.lean](PL1/MainTheoremA.lean): `PL1.theoremA`, `theoremAReal`, `theoremAComplexStrong` |
| Full B, with its actual witness | [MainTheoremB.lean](PL1/MainTheoremB.lean): `PL1.constant_intervalProjection_theoremBSpec`, `theoremB`, `theoremBReal`, `theoremBComplexStrong` |
| Stronger arbitrary-copy exclusion | [EnfloNoL1.lean](PL1/EnfloNoL1.lean): `Noise.constant_intervalProjection_range_no_real_L1`, `constant_intervalProjection_range_no_underlying_real_L1`, `constant_intervalProjection_range_no_L1` |
| Exact reviewed types and axioms | [ThirdProofReview.lean](PL1/ThirdProofReview.lean), including an example of the original `MainTheoremsStatement` |

Every B clause concerns the same actual projection `Noise.intervalProjection K Noise.constantRates`: idempotence, norm at most `4+3√2`, closed infinite-dimensional range, a closed scalar ell2 copy, absence of a scalar interval-L1 copy, failure of the Schur property, and absence of an equivalent real lattice norm on the underlying real range. The no-copy theorem also excludes real interval-L1 copies in the complex range viewed over the reals.

A uses the actual Schur-rate projection and proves its Dunford–Pettis and Schur properties, full vector-measure RNP failure, and nonlattice conclusion, with the same bound. No structural premises remain in either main endpoint.

## The new B proof

[THEOREM_B_PROOF_ROUTE.md](THEOREM_B_PROOF_ROUTE.md) explains the concrete argument and its Lean components.

The lattice branch proves finite real Grothendieck with constant 128, both actual interval summing estimates, disjoint and positive-family norm estimates without assuming primal band projections, an equivalent AL norm, and the direct Schur-or-interval-L1 alternative for every separable Banach lattice complemented in real interval L1.

The construction branch proves maximum-mass decay after positive-time noise, using a common integrable dyadic majorant, clipping and the actual hypercontractive estimate. Operator-norm approximation gives decay for the resolvents and intrinsic coordinates. A proved summable coordinate majorant gives decay in the entire actual ell1 graph. A finite Rademacher inequality then excludes every bounded-below L1 embedding. Joint real/imaginary-part maps establish the stronger real obstruction for complex scalars.

The older conditional `ComplementedLatticeReduction` and `ComplementedLatticeRealAmbient` results remain valid. Their general representation and extraction premises are not claimed as proved; the completed direct B proof does not use them. Earlier research and source-access notes in `verification/` are historical.

## Other manuscript results and remaining scope

Previously proved results remain in the source tree: sharp actual noise hypercontractivity; Schur-lattice atomicity and vector-measure RNP; Daugavet for both original intrinsic norms and their underlying real spaces; exact FDD dimensions and expansions, MAP and tail norm two; explicit bounded coordinate-filtration Mathlib martingales with every trajectory non-Cauchy; Schur weak non-Cauchy trajectories; the exposed constant and non-strong exposure; and the full `theta=1/2, q=1` identification with the actual generator-domain K-functional integral and its complete integral norm.

Diameter two for arbitrary relatively weakly open subsets, the PCP consequence, unconditional-sum nonembedding and the general-theta extension remain separate work. Completion of A and B is not a claim that every later manuscript result or external structural theorem is formalised. See [NEXT_STEPS.md](NEXT_STEPS.md).

## Verification and reproduction

The reviewed `Definitions.lean`, `LatticeDefinitions.lean`, `Statements.lean`, manuscript inputs and dependency pins are unchanged. The native endpoint checks use only `propext`, `Classical.choice` and `Quot.sound`; no `sorry`, custom mathematical axiom or proof-checking bypass is used. Independent semantic audits are linked from the [third construction report](verification/THIRD_CONSTRUCTION_REPORT.md).

Lean is pinned to `leanprover/lean4:v4.34.0-rc2`, Mathlib to `4cbb42e75a050e830b7cf0f2ae748d7644f59cf7`. All 21 vendored BanLat sources match the prior compatibility port. See [LIBRARY_PROVENANCE.md](LIBRARY_PROVENANCE.md).

The fresh run rebuilt the complete imported non-toolchain closure into an initially empty artifact directory: 222 project modules, 2,920 Mathlib modules and 257 other dependency modules. It retained the pinned compiler, bundled standard libraries, runtime and official checker. This was a direct native Lean build; optional Mathlib style linters and Lake cache hooks were not run, and the compiler was not bootstrapped.

The official `leanchecker --fresh --verbose PL1FreshAudit` replay passed in 1,063.6 seconds using Lean's own kernel from an empty environment. It is not an independently implemented kernel; its unsafe/partial exclusions are inventoried. Separate raw inspection checked 157 claim records, all 5,683 eligible project-origin declarations and the four exact scalar endpoint types. Their reachable axioms are confined to `propext`, `Classical.choice` and `Quot.sound`. These dependency checks are distinct from the full imported axiom inventory and the manuscript's semantic review.

For the ordinary project check using cached dependencies, run from this directory:

```powershell
./scripts/run-lean.ps1 -LeanFile PL1/MainTheoremB.lean -EmitOlean
./scripts/run-lean.ps1 -LeanFile PL1/ThirdProofReview.lean -EmitOlean
& '{USER_HOME}/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/python.exe' scripts/check-project.py
& '{USER_HOME}/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/python.exe' scripts/summarise-checks.py
& '{USER_HOME}/.cache/codex-runtimes/codex-primary-runtime/dependencies/python/python.exe' scripts/write-third-construction-report.py
```

These helpers run the native compiler in dependency order, with at most two concurrent compiler processes, and record real exit codes and before/after source hashes. They reuse the pinned dependency cache in the neighbouring trial workspace. The separate fresh run's commands, isolated paths, replay and inspection records are linked from the [fresh verification report](verification/FRESH_VERIFICATION_REPORT.md). A standalone `lake build` in a new checkout has not been tested.

The earlier 95-source and 189-source results, reports and documentation are preserved in `verification/Pass1Checkpoint-20260913T074716Z/` and `verification/Pass2Checkpoint-20260913T104653Z/`. The original two finite supplements remain historical standalone artifacts; their completed arguments now belong to the production proof.