# Library provenance and mathematical meanings

The dependency pins are unchanged:

- Lean: `leanprover/lean4:v4.34.0-rc2`.
- Mathlib: `4cbb42e75a050e830b7cf0f2ae748d7644f59cf7`, from [mathlib4](https://github.com/leanprover-community/mathlib4).
- BanLat upstream: `5c9360ccd9cef27b749f3cabda6348fd2529d1a3`, from [banlat](https://github.com/davidmunozlahoz/banlat), Apache 2.0, reused through the prior Lean-4.34 compatibility port.

The ordinary project runner resolves Mathlib and its pinned compiled dependencies through `../lean_trial_2026-09-05/.lake/packages/mathlib`; transitive revisions are fixed in `lake-manifest.json`. The earlier cached-dependency builds remain preserved: the [second-pass report](verification/SECOND_CONSTRUCTION_REPORT.md) covers 189 sources, and the [third construction report](verification/THIRD_CONSTRUCTION_REPORT.md) covers the 222-source build completed at 12:03:42 UTC on 13 September 2026. The latter records 154 central axiom reports, zero unexpected axioms, zero forbidden executable proof tokens, nine unchanged dependency records and ten unchanged reviewed files.

The later [fresh verification](verification/FRESH_VERIFICATION_REPORT.md) passed all required stages. Direct native compilation rebuilt the entire imported non-toolchain closure into an initially empty artifact directory: 222 project modules, 2,920 Mathlib modules and 257 other dependency modules, totaling 3,399. No pre-existing compiled project or non-toolchain dependency artifacts were reused; the resumed session used only hash-verified outputs produced earlier in this same fresh run. The pinned compiler, bundled standard libraries, runtime and official checker were retained. Compiler bootstrapping and a full Lake build, including optional Mathlib style linters and Lake cache hooks, were outside this run.

The official pinned `leanchecker --fresh --verbose PL1FreshAudit` passed in 1,063.6 seconds. Its imported environment contains 3,400 fresh modules including the audit root and 1,552 retained toolchain modules; these are inventory counts, not a checker-emitted declaration count. Replay starts from an empty environment using Lean's own kernel, not an independently implemented kernel. Its unsafe/partial exclusions are inventoried separately. Raw inspection asserts the four exact scalar theorem types and traverses 157 claim records and all 5,683 eligible project-origin declarations; their reachable axioms are limited to `propext`, `Classical.choice` and `Quot.sound`. The full imported axiom inventory is reported separately and is not subject to that blanket claim. Reviewed definition bodies and generic theorem types are also recorded; source and artifact identity is bound by the final hashes.

## Pinned Mathlib components

| Component | Library source / declaration | Meaning used |
|---|---|---|
| Lp and interval L1 | `MeasureTheory/Function/LpSpace/Basic.lean`, `MeasureTheory.Lp`; restricted Lebesgue `volume` | Actual a.e. quotient spaces with the library norm, at exponent one on `[0,1]`. |
| Sequence ell1/ell2 | `Analysis/Normed/Lp/lpSpace.lean`, `lp` | Norm-power summability on the countable coordinate set, exponents one or two. |
| Scalars and realification | `Analysis/RCLike/Basic.lean`, `RCLike`; `RestrictScalars`, `NormedSpace.restrictScalars` | Real/complex field structure; original addition and norm with only the scalar action restricted. |
| Isomorphisms | `Topology/Algebra/Module/Equiv.lean`, `ContinuousLinearEquiv` | Actual linear equivalence continuous in both directions. |
| Vector measures and variation | `MeasureTheory/VectorMeasure/Basic.lean`, `Variation/Defs.lean` | Countable additivity and ENNReal-valued total variation. Finite variation is explicit in the project RNP predicate. |
| Bochner integration | `MeasureTheory/Integral/Bochner/Basic.lean` | Integrable vector densities with identities on all measurable sets. |
| Conditional expectations and martingales | `MeasureTheory/Function/ConditionalExpectation`, `Probability/Martingale/Basic.lean` | Genuine Bochner conditional expectation and Mathlib `Martingale` for the constructed first-coordinate filtration. |
| Probability models | Countable product, Haar, Bernoulli/exponential laws, probability kernels | Actual measures and integration used for the noise and resolvent constructions. |
| Interval sampler/retraction | `Probability/Kernel/Representation.lean`, `Measure.exists_measurable_map_eq`; `Probability/Kernel/CondDistrib.lean`, `condDistrib` | Isometric probability pullback and contractive conditional-distribution left inverse, with their measure identities. |
| Equivalent norms | `Analysis/Normed/Module/Seminorm/Basic.lean`, `Seminorm`; `Seminorm/Norm.lean`, `normSeminorm` | The project supplies positivity, solidity and two-sided norm bounds, then realizes the actual complete normed lattice. |

Positive-measure Radon–Nikodým is not substituted for Banach-space RNP. The project proves the needed vector-measure density and operator implications. Likewise, the sharp two-point inequality, finite tensorization, actual noise extension, lattice atomicity and Daugavet argument are project proofs, not informal references treated as library theorems.

## All 21 reused BanLat sources

Every vendored `.lean` file was compared by SHA-256 with its counterpart under `../lean_trial_2026-09-05/BanLat` again during the third pass; **all 21 are byte-identical**. They are unchanged copies of the prior compatibility port, not claims of byte identity with the older upstream checkout. Existing copyright headers are retained.

| Group | Reused modules | Role |
|---|---|---|
| Core: 8 | `Basic`, `Normed`, `Disjoint`, `Dual`, `LLexpr`, `OrderComplete`, `OrderUnit`, `RieszDec` | Real vector/normed/Banach lattices, disjointness, positive dual functionals and order completeness. |
| Operators: 5 | `Operators/Hom`, `OrderBounded`, `Positive`, `Regular`, `RieszKantorovich` | Actual order-compatible linear maps and dual/order constructions. |
| Substructures: 2 | `Substructures/Ideal`, `Substructures/Sublattice` | Ideals, sublattices and their order APIs. |
| Bands: 6 | `Substructures/Band/Basic`, `DisjointComplement`, `Generated`, `Lattice`, `PPP`, `Projection` | Generated and complementary bands and actual principal-band projections. |

`VectorLattice` is the real ordered vector-space structure. `NormedVectorLattice` adds the solid norm, and `BanachLattice` adds completeness; the ambient lattice, ordered addition and normed additive group remain explicit. These are the structures used by the actual Schur-lattice theorem. The atom definition is the project's vector-lattice atom: a positive nonzero vector with a one-dimensional positive interval. Mathlib's order-theoretic atom of a positive cone is not substituted for it.

The first pass used four BanLat sources; its provenance/report remains historical. The expanded 21-source closure is needed by the second-pass positive-dual and atomic-band construction. No dependency Git revision was changed to obtain it.

## Project-defined predicates and evidence

`PL1/Definitions.lean` and `PL1/LatticeDefinitions.lean` retain the reviewed meanings of RNP, Schur, copies, projections and equivalent real lattice norm. `PL1/Statements.lean` retains the complete A/B target bodies. `LatticeBridge` and `LatticeRenorming` prove the equivalence between an actual BanLat model and the reviewed compatible-norm predicate under the displayed completeness hypotheses. `MainTheoremA` now uses the proved structural RNP theorem to exclude that predicate for the actual Schur range.

Full B is now proved by `MainTheoremB` without structural premises. The project proves the needed complemented-lattice alternative directly using its finite Grothendieck, positive-family and AL-lattice constructions. It also proves the actual constant-rate range's arbitrary-L1-copy obstruction directly from hypercontractivity and dyadic maximum decay. The older `theoremB_real_and_complex_of_real_structural_properties` remains a conditional reduction; its general premises are neither axioms nor claimed library theorems and are not used by the completed endpoint. See [THEOREM_B_PROOF_ROUTE.md](THEOREM_B_PROOF_ROUTE.md).

The exposed-point result is the exact norm-one functional and unique-maximizer statement; no optional Mathlib `IsExposed` wrapper is claimed. `DaugavetDiameter` uses actual `Metric.diam`, with boundedness proved, and an explicit sequential failure of strong exposure. The completed interpolation endpoint uses the actual complete generator graph domain and an explicit standard K-functional infimum/integral; it does not substitute a named interpolation-space predicate or a discrete norm for that integral.

`InterpolationNorm.Space` is a separate carrier copy carrying the literal integral norm, with its own proved norm laws, completeness and continuous linear equivalence to the original intrinsic space. This equivalent-norm bundle does not change the norm used by the projection or Daugavet statements.

The first- and second-pass checkpoints preserve prior source manifests, verification reports and earlier docs. Per-module native logs record the compiler path, dependency search path, true exit code and source hashes. The latest evidence is linked from the [fresh verification report](verification/FRESH_VERIFICATION_REPORT.md); `verification/Project-20260913T113917105417Z/` remains the earlier project-only build record. See also the [third construction report](verification/THIRD_CONSTRUCTION_REPORT.md), [THIRD_THREE_HOUR_RUN.md](THIRD_THREE_HOUR_RUN.md), [MAIN_THEOREM_B_INDEPENDENT_AUDIT.md](verification/MAIN_THEOREM_B_INDEPENDENT_AUDIT.md), [MAIN_A_SEMANTIC_AUDIT.md](MAIN_A_SEMANTIC_AUDIT.md), and [HYPERCONTRACTIVITY_AUDIT.md](HYPERCONTRACTIVITY_AUDIT.md). The original supplementary drafts are historical and are not included in the production source count; the promoted production proofs are counted.