# Manuscript coverage: third development pass

**The exact reviewed Theorems A and B are proved**, over real scalars and complex scalars with the stronger underlying-real nonlattice conclusions. Reviewed definitions, target statements, manuscript inputs and dependency pins are unchanged. The [fresh verification report](verification/FRESH_VERIFICATION_REPORT.md) records PASS for the 3,399-module imported-source rebuild, official same-kernel `leanchecker --fresh` replay and separate raw type/axiom inspection. The [third construction report](verification/THIRD_CONSTRUCTION_REPORT.md) preserves the preceding 222-source project build and its audits.

Geometry below concerns the actual intrinsic space with its original inherited ell1 graph norm. Scalar specialisations use `RCLike`; underlying-real statements preserve the norm and explicitly restrict scalars.

| Paper result | Proved coverage and main files | Remaining scope |
|---|---|---|
| A, `thm:main` | `MainTheoremA`: `theoremA`, `theoremAReal`, `theoremAComplexStrong` prove every reviewed clause for the actual Schur-rate interval projection, with bound `4+3√2`. | None in the reviewed target. |
| B, `thm:non-schur` | `MainTheoremB`: `theoremB`, `theoremBReal`, `theoremBComplexStrong` prove every reviewed clause for the actual constant-rate interval projection: projection bound, closed infinite-dimensional range, closed scalar ell2 copy, no scalar interval-L1 copy, non-Schur and the stronger underlying-real nonlattice conclusion. | None in the reviewed target. No classification, L1 representation or copy-extraction premise remains. |
| Stronger real L1-copy exclusion for B | `EnfloSmoothing`, `EnfloVanishing`, `DyadicCoordinateDomination`, `EnfloSum`, `EnfloIntrinsic`, `EnfloTwoMaps`, `IntrinsicRealParts`, `EnfloCopyExclusion`, `EnfloNoL1`: the actual constant-rate interval range contains no real interval-L1 copy, even on the underlying real space of the complex construction. | Complete for the construction. A general Enflo–Starbird extraction theorem is not asserted. |
| Finite and interval summing estimates | `FiniteRademacherClipping`, `FiniteGrothendieckNormalization`, `FiniteGrothendieck`, `FiniteSummingFromMatrix`, `DyadicL1Coordinates`, `IntervalSumming`: actual finite matrix Grothendieck inequality with constant 128, both finite summing estimates and their passage to actual real interval L1. `SummingTransport` transfers them through actual complemented copies. | Complete sufficient estimates. The constant is not claimed optimal. |
| Complemented Banach-lattice alternative | `PrincipalIdealDual`, `DisjointNormingFunctionals`, `FiniteDualDisjointization`, `PositiveLowerOneBridge`: disjoint lower-one bounds without primal PPP, then the same-constant bound for all positive families. `ALRenorming`, `ALOrder`, `ALFragments`, `ALAtomic`, `ALDyadicEmbedding`, `ALAlternative`: an actual equivalent AL norm and the unconditional Schur-or-real-interval-L1 alternative for a separable Banach lattice complemented in real interval L1. | Complete direct alternative needed for B. General Kakutani representation and the previously proposed classification/extraction predicates remain separate library results. |
| `lem:dp` | `L1UniformIntegrability`, `L1Truncation`, `CompactRestriction`: compact L∞ restriction implies DP on actual L1. | Complete; uses direct weak-sequence uniform integrability and truncation. |
| `lem:schur-lattice` | `SchurLatticeAtomicity`, `AtomicBandDecomposition`: separable Schur Banach lattices are atomic and have the full reviewed vector-measure RNP. | Complete. No atomicity, decomposition or weak compactness premise remains. |
| `lem:carrier` | `SingularCarrier`, `CarrierAsymptotics`: explicit Haar-null tail carrier of full noise and resolvent mass for both rates. | Complete, including nonnegative noise times. |
| `prop:resolvents` | `NoiseMeasures`, `ConcreteResolvents`, `NoiseSemigroup`, `BochnerResolvents`: actual probabilities, Walsh formulae, contraction, resolvent identities, commutation, strong limits and Bochner representation; compact L2 resolvents for increasing rates. | Complete stated operator ingredients. |
| Hypercontractive ingredient | `BonamiTwoPoint`, `BonamiTensorization`, `BonamiHaarBridge`, `ConvolutionHypercontractivity`, `NoiseHypercontractivity`: actual infinite-product Lp-to-L2 contraction at the sharp exponent `1+exp(-2u)`, both fields. | Complete sufficient estimate; positive time gives exponent below two. |
| `lem:intrinsic`, `prop:projection` | `IntrinsicGraph`, `SeparableRange`, `L1Sum`, `DyadicProjection`, `ConcreteResolvents`: complete separable intrinsic graph, actual synthesis/retraction, projection identity and bound. | Complete. Evaluation at zero identifies graph vectors with the paper's functions injectively. |
| `prop:schur` and interval transfer | `SchurExample`, `DyadicSchur`, `IntervalModel`, `IntervalRetraction`, `IntervalWalsh`, `ProjectionRetract`: actual Schur/DP and interval witnesses. | Complete; an isometric embedding with contractive retraction replaces a global ambient measure-space isomorphism. |
| `lem:singular` | `SingularConvolution`, `RNPBridge`, `ScalarRealification`, `SingularResolvents`: actual singular convolution forbids the full Bochner setwise density; real and underlying-real non-RNP. | Complete reviewed RNP obstruction. |
| Trace-smoothing and matrix lemmas | `SmoothingTrace`, `MatrixSmoothing`, `TruncatedResolventFactorization`, `NoiseTraceObstruction`, `ConstantNoiseTrace`: smoothing limits, actual matrix entries/column summability, constant-rate trace vanishing and identity-distance obstruction. | Operator premises discharged. The old arbitrary-subspace extraction route is no longer needed for B. |
| `lem:tail-spikes` | `TailSpikes`, `ConstantTailSpikes`, `HeadTail`, `TailSpikeMultiplication`: actual finite tail densities, concentration, positivity, mass one, finite average one, independence and quantitative semigroup/resolvent estimates. | Complete for both rate sequences. |
| `prop:daugavet` | `IntrinsicSpikeFamilies`, `DaugavetAveraging`, `MainDaugavet`, `DaugavetRealification`: actual slice criterion and every rank-one norm equation, for both rates and also all real rank-one maps on each underlying real space. | Complete Daugavet conclusion in the original intrinsic norm. |
| Unlabelled exposed-point claim | `IntrinsicExposedPoint`: actual Haar-integral functional has norm one and unique maximizer `intrinsicCharacter K rates ∅` on the unit ball; strict inequality elsewhere. `DaugavetDiameter` gives maximizing sequences at distance tending to two from this point. | Complete exposing-functional statement for both rates; the exposure is not strong. No optional Mathlib exposed-point wrapper is asserted. |
| Diameter of slices | `DaugavetDiameter`: explicit pairs at distance greater than `2−ε`, upper bound two, and exact `Metric.diam=2` for every normalized real-part slice. | Complete for both intrinsic rate spaces, both fields and the full underlying-real dual. Arbitrary relatively weakly open subsets remain separate. |
| `prop:fdd` | `IntrinsicWalshBlocks`, `MetricApproximation`, `IntrinsicTailNorm`: rank `E_m=2^m`, initial block `E_0` of dimension one, difference block `E_(m+1)−E_m` of dimension `2^m`, unique norm expansion, norm-one projections, MAP and exact `‖I−E_m‖=2`. | Complete for both constructions. |
| `prop:martingale` | `ExplicitMartingale`, `ExplicitMartingaleFiltration`, `IntrinsicNonBoundedComplete`: exact cylinder-resolvent sequence and minimum-index coherence, bound `4+3√2`, genuine coordinate-filtration Mathlib martingale, every trajectory norm non-Cauchy, failure of bounded completeness. | Complete for both rates and both fields. |
| Weak-trajectory discussion | `ExplicitMartingaleWeak`: every Schur-rate trajectory is not weakly Cauchy against the full scalar dual or full real dual; an actual functional witnesses persistent scalar oscillation. | Proved for the Schur construction only. |
| `prop:interpolation` | `MainInterpolation`: `mem_intrinsic_iff` and `intrinsic_eq_realInterpolation` identify the actual intrinsic functions with the finite standard K-functional integral for the true generator's complete graph-norm domain, with explicit universal lower and upper norm bounds. `InterpolationNorm` bundles the complete integral norm and a function-preserving continuous linear equivalence. | Complete at θ=1/2, q=1, for every nonnegative rate sequence and both scalar fields. General θ remains separate. |
| Constant-rate later geometry | Actual ell2 copy, non-Schur, underlying-real non-RNP, Daugavet including underlying real, FDD/MAP, tail norm two, exposed point and explicit martingale, together with the full B endpoint. | The later open consequences listed below remain separate. |

The former B hypotheses `ComplementedL1LatticeClassification ℝ`, `SeparableRealL1Dichotomy.{0}` and `L1CopyExtraction ℝ` remain explicit predicates in the older conditional route. They have not been silently promoted to proved general theorems. The unconditional `MainTheoremB` instead combines the proved complemented-lattice alternative with direct exclusion of real L1 copies in this particular projection range. Neither a general measure-space representation nor extraction of a complemented copy is required.

The finite-summing and finite-clipping supplements from the second pass have been promoted into the production proof chain and their former matrix/interval premises discharged by the new modules. Their historical supplementary reports still describe their earlier limited scope.

General positive RNP results quantify independently over the measurable-source universe. Counterexample RNP targets retain source universe zero and the exact reviewed original norm/real scalar structure. `Ell1RNP` and `IntervalEll1Obstruction` also show neither actual interval range is isomorphic to scalar ell1; this does not prohibit ell1 subspaces.

Diameter two for arbitrary relatively weakly open subsets and the PCP consequence, nonembedding into unconditional sums of reflexive spaces, and the general-θ construction/interpolation discussion are not claimed complete. See [NEXT_STEPS.md](NEXT_STEPS.md) for remaining work, [PROOF_ROUTE.md](PROOF_ROUTE.md) for proof replacements, and the [fresh verification report](verification/FRESH_VERIFICATION_REPORT.md) for final verification scope and evidence. Verification retained the pinned compiler and bundled toolchain libraries; it was a direct native build rather than a full Lake build or compiler bootstrap. Research notes or drafts under `verification/` are not counted as proofs unless their actual checked production endpoints are identified here. Earlier inventories are preserved in `verification/Pass1Checkpoint-20260913T074716Z/` and `verification/Pass2Checkpoint-20260913T104653Z/`.