Abstract We present a layered three-repository Lean 4 and Mathlib library for finite-dimensional complex quantum foundations. The corpus includes finite-dimensional Gleason and Busch representation theorems, Wigner and one-directional Uhlhorn theorems, an explicit finite Naimark dilation, Kent's contrary-inferences construction, Riedel's redundant-record decomposition, selector classifications, circuit-complexity results, and conditional Born expectation. A shared concrete operator layer supplies common definitions of Hilbert spaces, projections, effects, density operators, and trace-based Born values, supporting internal reuse across these developments. The library also proves exact classification and lower-bound results for interfaces introduced in the project. A second contribution is a partial typed premise-audit and reporting framework that adapts vacuity and specification-validation concerns to strongly typed conditional mathematical theorems. Its principal case study shows that refinement coherence alone makes a subspace weight independent of the finite orthogonal decomposition in which the subspace occurs, without normalization, and then audits conditional Born representations at weight, rational-expectation, and projection-measure levels. The released evidence includes typed inhabitants, premise-eliminability results, a dimension-two projection measure admitting no density-operator representation, further dimension-two non-Born countermodels, and a proved vacuity result, while remaining gaps are reported explicitly. Version-pinned releases are archived on Zenodo with reproducible dependency, source-guard, and axiom audits.
Abstract We present a layered three-repository Lean 4 and Mathlib library for finite-dimensional complex quantum foundations. The corpus includes finite-dimensional Gleason and Busch representation theorems, Wigner and one-directional Uhlhorn theorems, an explicit finite Naimark dilation, Kent's contrary-inferences construction, Riedel's redundant-record decomposition, selector classifications, circuit-complexity results, and conditional Born expectation. A shared concrete operator layer supplies common definitions of Hilbert spaces, projections, effects, density operators, and trace-based Born values, supporting internal reuse across these developments. The library also proves exact classification and lower-bound results for interfaces introduced in the project. A second contribution is a partial typed premise-audit and reporting framework that adapts vacuity and specification-validation concerns to strongly typed conditional mathematical theorems. Its principal case study shows that refinement coherence alone makes a subspace weight independent of the finite orthogonal decomposition in which the subspace occurs, without normalization, and then audits conditional Born representations at weight, rational-expectation, and projection-measure levels. The released evidence includes typed inhabitants, premise-eliminability results, a dimension-two projection measure admitting no density-operator representation, further dimension-two non-Born countermodels, and a proved vacuity result, while remaining gaps are reported explicitly. Version-pinned releases are archived on Zenodo with reproducible dependency, source-guard, and axiom audits.
This paper records the second layer of the Lean4 formalisation programme by isolating the finite-dimensional measure-and-weight layer that sits between deterministic volume typicality and the later operational reconstruction. Building on LF1, which proves that empirical frequencies converge to normalised ontic volume weights under repeated preparation, the present paper formalises the measure bridge from ontic Liouville volume to projective-state weights and then packages the Born-weight layer under explicitly stated external inputs. LF1 itself is not a Born-rule paper, and LF2 is designed to make that separation precise. The first component is a sector-conditional pushforward result. Under the symmetry-compatible quantum-effective assumptions, with a measurable projection π : Σ → CPN−1 (smooth and surjective in the underlying physical model), SU(N)-equivariance, and invariant Liouville measure µL, the pushforward measure is proportional to the Fubini–Study measure:π∗µL = c · µFS for some constant c. In the current Lean implementation, the bridge is formalised in this existential form. The explicit mass-comparison formula for c remains part of the paper-level mathematical discussion, but is not yet encoded as a separate Lean theorem. This is the measure bridge established at the paper level in TN1 and tracked in the programme dependency map as a distinct layer from the later Born-weight step. The second component is the Born-weight wrapper. Given the projective measure layer, LF2 packages the finite-dimensional probability assignment using an explicit operational consistency package together with an imported Busch effect-Gleason theorem, applied uniformly for finite dimensions N ≥ 2. Correction, 14 August 2026. The imported Busch effect-Gleason theorem named in the final paragraph is no longer an external input. It was proved on 21 July 2026 as OperationalPackage.effect_gleason_representation in CsdLean4/LF2/EffectGleason.lean, following Busch's finite-dimensional argument. It had been the Born-weight wrapper's one load-bearing external input; the wrapper is now closed under the corpus itself, which imports no axioms beyond Lean's foundational triple (propext, Classical.choice, Quot.sound). Per-theorem axiom status: https://github.com/zblore/csd-lean4/blob/main/AXIOMS.md
We report mechanized proofs, in the Lean 4 proof assistant and its Mathlib library, of Busch’s (2003) theorem on effect-valued (POVM) probability measures, together with its corollary establishing the Born rule on subspaces, and of the finite-dimensional, complex, projection-valued (PVM) case of Gleason’s theorem (n ≥ 3), together with the classical dispersion-free (nohidden-variables) corollary. All four results are verified with zero project-specific axioms: the Lean kernel reports dependence only on propext, Classical.choice, and Quot.sound, the three axioms accepted as standard throughout Mathlib. The proof of Gleason’s theorem follows the real-analytic route of Cooke, Keane and Moran (1985), with a complex reduction via real sections in the style of Dvurečenskij. The mathematical proof strategies and their Lean implementation were developed through sustained, iterative collaboration with large language models; the author’s role was to select the target theorems, orchestrate and redirect this collaboration, critically validate or reject proposed strategies, and enforce the verification discipline described in Section 4. We report this process transparently rather than as a methodological contribution.The full development is available at https://github.com/Bobart0/gleason-theorem-lean.
We formalize in Lean 4/Mathlib a finite-dimensional route to Gleason’s theorem based on Cooke–Keane–Moran and Richman–Bridges, with Dvureˇcenskij’s reduction from complex spaces to real three-dimensional sections. Cooke–Keane–Moran obtain the extremal step by compactness of a product space; in Lean we realize their accumulation point by an ultrafilter. More substantially, the opening step of their general-case argument in §7 invokes ingredients that do not, as stated, supply the required minimizer orthogonal to a maximizer. We give the missing two-frame argument explicitly and machine-check the resulting theorem for Hn = Cn,n ≥ 3. On top of this representation layer we formalize the one-directional Uhlhorn–ˇSemrl theorem as an application of Gleason and Wigner. The development also includes Busch’s effect-measure theorem, a projective weight theorem whose local binary-split formulation generates finite refinement coherence, and a finite Naimark interface with a strict classification of binary implementations. Classical failures at dimension two are formalized at the exact input types of the corresponding theorems, while the effect-domain route recovers the qubit case. Together these results exhibit a distinct proof route to representation, one local justification exposed by formalization, and typed boundaries separating projection, effect, symmetry and refinement interfaces.
Can a Born-type probability structure arise on a substrate that is only a finite stochastic process? A stochastic program built from six primitive operations supplies the final matrix; a specified layered architecture constructs, from its outputs, a record layer, a two-dimensional real carrier and a quadratic law, and supports an adopted Born calculus. The six operations alone do not give this structure, and the square-root encoding and the projection are construction choices. Our main contribution is the architecture: a directed acyclic graph whose arrows are each marked as derived, chosen, adopted or standard mathematics, with the kind of check behind each. On registered populations, a snapshot predictor whose rank-two case is the law predicts the substrate's sampled label frequencies with lower aggregate loss than named competitors, and, in the construction's canonical basis, its cross terms carry its advantage over the diagonal rule. In each of 2,122 census cases the encoded state is not a function of the anonymous initial record description: two point preparations sharing all three labels differ by at least 1/25 in the trace probability of raw label 0, a statement about exact data, not operational access. This bound is retrospective: the registered bound 3/20 fails in 117 cases of the full census. On the original worked case the updates by the final matrix and its square do not lift to the carrier. The measurement rules are adopted: Lüders tests, all densities and effects, and additivity; on them the trace rule is unique, and finite ontic models with additive responses, and measurable preparation-noncontextual representations preserving the specified mixtures, are excluded. We do not claim that the substrate produces the measurement rule, that the layer forms in the run, or a derivation of quantum theory. The source code of the stochastic program, the constructions, the reproduction pipeline, the verification commands and the Lean 4 proofs are available at https://github.com/ioannist/six-birds-born (release v1.0). AI systems were used throughout this work, as the manuscript describes; the author directed the research, made the scientific decisions and is responsible for the content.
Complementarity-First Foundational Release III develops reciprocal phase architecture, conditional gauge and incidence geometry, finite Lorentzian connection selection, and relational quantum-information tasks. This paper synthesizes the eight research preprints and one reproducibility dataset in Waves A–C without transferring theorem ownership or treating their separately admitted carriers as a single derived physical system. The release is organized by four distinctions: structural admission versus conditional selection; geometric covariance versus operational implementation; restricted agreement versus complete identification; and mathematical existence versus a resource-accounted realization. The reciprocal quantum construction separates local inclusion, coherent completion, entanglement, finite projective valuation, and individual outcomes. Its synthetic biphoton companion distinguishes image intensity from phase-sensitive entanglement evidence. The geometric papers distinguish a derived compact phase-frame type from electromagnetic gauge interpretation and constitutive dynamics, anti-linear opposite-weight pairing from same-bundle reversal, an indefinite incidence form from positive records, and geometric-section agreement from independent connection variation. The Wave C papers supply finite addressing classifications, task- and record-relative recovery, encoded-preparation advantages, and exact exchange constructions with trajectory and timing bounds. Cross-wave comparisons locate genuine imported interfaces and identify bridges that remain absent, including the passage from finite Born-form valuation to general instruments and from a recorded group-error model to a physical timing-error model. Analytic proofs, finite calculations, numerical certificates, recorded replays, and scoped Lean verification are assigned distinct evidentiary roles. The contribution is a source-attributed scientific synthesis and an explicit dependency and residual-premise map, not a new primitive derivation of quantum theory, electromagnetism, or gravity.
This record contains a technical note on a conditional derivation of the quadratic Born density from a minimal two-cell structural mixing condition. The article starts from a Hilbert-space representation of states and assumes that event weights admit a local gauge-invariant pointwise modulus density. It then adds one structural invariance condition: the total weight of two equal cells is unchanged under a real rotation mixing their amplitudes. Under these assumptions, the local density is forced to be quadratic, f(r) = cr², yielding the usual Born weight after normalization. The result is not presented as a replacement for Gleason-type or decision-theoretic derivations of the Born rule. Its purpose is narrower: to isolate a simple local route by which the square law follows once the density form and a minimal two-cell basis-independence principle are granted. The functional-equation core and the two-cell reduction have been formalized in Lean 4 using Mathlib. The accompanying Lean development is archived separately at Zenodo: https://doi.org/10.5281/zenodo.20528721. The reported axiom footprint for every formalized theorem in the development, including the measure-theoretic born_density and born_rule_weight, is the standard classical Lean base, with no admitted steps (sorryAx) in any of the formalized theorems. The manuscript and the accompanying Lean development were prepared with extensive AI assistance. The author reviewed, selected, corrected, and revised the outputs and remains responsible for the final text, the mathematical claims, the Lean formalization, and the interpretive framing.