# Independent audit of the full Theorem A endpoint

Auditor: the atomic-band/decomposition agent, separately from the authors of
the first-pass RNP endpoint and the final MainTheoremA integration.
Audit and matching source-evidence snapshot completed on 2026-09-13 at approximately 08:31 UTC.

**Finding: no semantic defect or extra mathematical assumption was found.**
The final theorem proves the previously reviewed Theorem A statement, including
the obstruction to every equivalent real lattice norm. This finding concerns
the exact Lean definitions described below; it does not silently substitute
another formulation of RNP or a new complex-lattice predicate.

## Exact target and source preservation

`MainTheoremA.theoremA` has only the scalar type and its `RCLike` instance as
parameters. Its real and complex specializations prove `TheoremARealStatement`
and `TheoremAComplexStrongStatement`. The supplied proof of
`SeparableSchurLatticeRNP` discharges the structural premise in LatticeReduction;
atomicity, order-interval compactness, a decomposition, and an external RNP
theorem are not additional hypotheses of MainTheoremA.

LatticeReduction uses the single explicit witness
`Noise.intervalProjection 𝕜 Noise.schurRates`. Idempotence, the bound
`4 + 3 * sqrt 2`, closed and infinite-dimensional range, the Dunford–Pettis
property, the Schur property, failure of RNP, and the lattice obstruction all
refer to this same projection and its actual range with the inherited norm.

The exact reviewed source bodies, manuscript inputs, guidance and pinned
compiler/dependency files remain byte-for-byte unchanged. The fresh check in
`verification/MainAReviewedSourcePreservation.json` compares all ten original
hashes against `verification/reviewed-source-preservation.json`. In particular:

| Reviewed file | SHA-256 |
| --- | --- |
| Definitions.lean | `1B56C4F85EBA48B6CBDE93D8CB7674CDA5C7227E8671FE2618F7B2DC1020D5F4` |
| LatticeDefinitions.lean | `3007A7906E5E8CA773BA81863BA82E796AAB0E96B9C3A87B1682AEBC11376604` |
| Statements.lean | `6ADC0894C6EE4F091160CBC77FFD39AFD6AFD1B6A6E369E1A0DA97653C6DC6B3` |

The complex endpoint forbids an equivalent lattice norm on the underlying
**real** space, exactly as in the previously reviewed strong target. It is not
being reported as a separate formal theorem about an unspecified definition of
complex Banach lattice.

## Full vector-measure RNP

`HasRadonNikodymProperty.{u,v} E` quantifies over every source type `Ω : Type v`,
every measurable structure on it, every finite positive measure, and every
countably additive E-valued vector measure of finite variation which vanishes
on measurable null sets. Its conclusion supplies a Bochner-integrable density
with the required integral identity on every measurable set.

The source universe `v` stays independent of the target universe `u` throughout
FiniteDimensionalRNP, DecompositionRNP, UnconditionalRNP, and
`SchurLattice.hasRadonNikodymProperty_of_schur`. There is no separability,
standard-Borel, countable-generation or topology assumption on the source
measurable space. LatticeReduction only needs its `v = 0` specialization because
that is the source universe fixed in the reviewed counterexample target.

The finite-dimensional proof obtains scalar signed-measure RN derivatives,
assembles finitely many coordinates, and transports them along a genuine
continuous linear equivalence. The decomposition proof forms densities of
`P_n ν`, proves their almost-everywhere coherence by uniqueness of densities,
and uses countably many null-set exclusions. It constructs a common integrable
bound from the actual scalar RN derivative of the variation of ν and a uniform
operator-norm bound. That domination is proved, not supplied as a premise.
Bounded completeness then yields an almost-everywhere norm limit. Measurability,
integrability and the integral identities follow from the proved domination
and dominated convergence, applied also to arbitrary restricted measures.

UnconditionalDecomposition proves bounded completeness from the Schur property:
coherent bounded branch differences have bounded signed partial sums by the
operator estimate, and the Schur bounded-completeness theorem gives convergence.
It does not assume the desired vector-measure RNP or the bounded completeness
being established. AtomicBandDecomposition supplies the finite-dimensional,
nested, strongly convergent band projections and their sign bound in the given
lattice and norm. Actual atomicity is discharged by SchurLatticeAtomicity.

## Transport and the concrete counterexample

The interval space is the actual Mathlib `L¹` space for volume restricted to
`[0,1]`. The interval model has an isometric embedding with a contractive left
inverse. Projection transport is `J P R`, with the proved identity `R J = id`;
the actual range equivalence preserves norms. The projection, range, Schur,
Dunford–Pettis and infinite-dimensional conclusions use these maps rather than
an abstract existential copy of the counterexample.

The non-RNP endpoint uses the actual singular resolvent measures for the Schur
rates. A common Haar-null carrier has full resolvent mass, and the zeroth
resolvent factors through the intrinsic range. RNP would turn the operator's
indicator vector measure into an integrable vector density. Applying scalar
Walsh functionals determines all countably many moments on a common full-measure
set; one fiber then yields an absolutely continuous measure with the singular
resolvent's moments, contradicting the null carrier. The proof does not assume
a jointly measurable choice of L¹ representatives. Scalar realification and
restriction of scalars are implemented by actual continuous linear maps and
preserve the original norm and the full RNP quantifiers.

Finally, a candidate equivalent solid lattice seminorm has a positive lower
bound, so LatticeRenorming makes it a genuine Banach-lattice norm. The upper and
lower bounds give a real continuous linear equivalence, transporting completeness,
separability, the full Schur property and RNP. Applying the newly proved
separable-Schur-lattice RNP theorem contradicts the actual range's failure of
RNP. No atomicity or order-completeness premise is inserted in this renorming
argument.

## Evidence and audit limits

`verification/MainASemanticReview.lean` independently prints the target and RNP
definitions with universes, checks the full endpoint signatures, and requests
axiom reports for thirteen central declarations. Native Lean exited 0 in
`verification/MainASemanticReview-20260913T082536090Z/`; every report contains
only `propext`, `Classical.choice`, and `Quot.sound`. Cached compiled dependencies
were reused, as disclosed by the runner; this was not a clean rebuild of Mathlib.

`verification/MainASemanticAuditSources.json` records exact hashes and matching
native-pass evidence for the audited production sources. This semantic audit
read the RNP/decomposition proofs and the final reduction in detail, plus the
critical interval/range/singular-convolution transport chain. The older interval
sampling foundation was checked through its actual map definitions, contracts
and identities; this note is not a claim to have independently reconstructed
every earlier analytic proof from scratch. The preceding order-continuity and
fragment/halving audit is recorded separately in `LATTICE_FRAGMENT_AUDIT.md`.