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.
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.
STATUS (18 October 2026). The physics programme that motivated this work was concluded in October 2026 and its claim of a unified derivation withdrawn. The results in this paper do not depend on that programme and stand as stated. NOTE ON SCOPE (18 October 2026). Where this paper says that the Standard Model's matter content, charges or gauge structure are derived from, forced by or emerge from the eight-bit error-correcting cell, read encoded in or assigned to. The finite results themselves stand: the code, its constraints and the anomaly arithmetic are exact. But two things are premises of the framework, not consequences: the identification of codewords with particles, and the choice of the eight-bit [8,4,4] cell. In particular, the step from read/write balance to a single CSS code is not derived [R22]. The author's October 2026 review of the programme concluded that the framework's Standard-Model content is assigned rather than derived. No observation currently distinguishes the framework's account from the Standard Model itself. This revised note argues that, within the accepted complex quantum-error-correcting record substrate, the quadratic Born form arises from linear record writing, orthogonality of record sectors, and isometric normalization before any probability measure is introduced. Conditional uniqueness is treated separately through Gleason-type and refinement-stable record-sector routes. The 30 August 2026 additivity-audit revision cites Jiaxuan Zhang's analysis of five Born-rule derivations (arXiv:2603.06211) and makes the premise accounting explicit: a Gleason frame function includes orthogonal additivity, while Marko Lela's route begins with a non-negative extensive valuation on disjoint continuation bundles. The closed-record-pair route assumes neither measure-level object, but establishes the quadratic form rather than a standalone uniqueness theorem. The resulting open frontier is to obtain both form and uniqueness without importing measure-level additivity. The paper also records the minimal [8,4,4] record cell and the bare monitored service rate alpha_0 = 1/137, while retaining the deeper reconstruction question as open.
We study how much of the Hilbert-space and Born-rule structure of quantum theory can be obtained from operational primitives that involve records but not probabilities. The setting is a regime in which coherent alternatives recombine without leaving a stable record. We obtain three results of different kinds. Geometry. From composable contributions, record-inert reversible controls and amplitude scalings, under named conditions, we obtain a real inner-product event geometry. The existence of the inner product is equivalent to bounded mixing and is assumed in that form. In a worked interferometer with one mode per channel, the metric is not an input: metric-free port swaps and phase flips fix the form up to scale, and boundedness only forces the other controls to preserve it. Its uniqueness up to scale, the orthogonality of distinct outcomes, and the representation of events by orthogonal projections are derived. Obstruction. This geometry, even with full symmetry about the preparation and exact dyadic standards, does not select the quadratic weight: the preparation mixed with the maximally mixed state survives. The structural operations exhibited here certify only values on which the quadratic weight equals the counting weight. On restricted event families where Gleason’s theorem is unavailable, a calibration order oriented by the quadratic magnitude selects it: given exact standards, a state is the quadratic one exactly when it respects all such brackets. Whether such an orientation can be earned is the open problem. Given such brackets and refinement only to a finite depth K, every admissible state lies within 2^-K of the quadratic weight, without the Archimedean step. On the full projection lattice, Gleason’s theorem with null support, or sphere-transitive symmetry with null support, gives other conditional routes. Bridge. A predictive probability kernel is introduced separately. Its identification with the real quadratic weight ||P_A ψ||² / ||ψ||² is conditional on kernel-admission hypotheses, one of which is equivalent to the Born value; the complex form needs phase invariance in addition. The hypotheses select a class of contexts, and none is shown to be forced. For each we state the physical feature it expresses and a sufficient condition where one is known, and we work out one apparatus in which the geometry-stage hypotheses hold together. For all but one we give a context in which it fails (for the founding conditions, one that leaves the regime); for the remaining one, TCC-1, we give an illustration. This paper is the first in a series built on a common framework, Structural Ledger Consistency (in preparation).
⚠️ CORRECTION NOTICE (added 2026): The author has since identified serious errors in this work through a systematic adversarial audit. The central claims of this record should not be relied upon. Specific issues found across this research program include implementation errors (e.g., conflation of signed cosine with cos²), circular definitions, proof gaps, results that reduce to known theorems, and effects that vanish under proper null models and direct-influence correction. This record is left online for transparency and as a documented case, not as a valid result. For the author's current, audited methodology, see the later work on classical-baseline auditing of quantum-like contextuality claims: https://doi.org/10.5281/zenodo.20680607 — A. Ogasawara This work investigates the structural origin of the Born rule within the framework of the Order-Projection Principle (OPP). We consider outcome-indexed measurements associated with orthonormal bases in finite-dimensional Hilbert spaces and analyze the constraints imposed by:(i) outcome-information separation (OIS),(ii) positivity and completeness of measurement operators, and(iii) non-contextuality of probability assignments. Under these conditions, we show that measurement operators reduce to rank-1 projectors and that, within an overlap-based family of candidate probability functions, the quadratic form P(e|ψ) = |⟨e|ψ⟩|² is uniquely compatible with non-contextuality. The result is obtained without introducing additional auxiliary axioms beyond the outcome-level formulation of the OPP framework. The role of linear structure (A4) and quadratic observation (A5) is also discussed, including their structural relationship to more primitive assumptions. Numerical experiments are provided to corroborate the consistency of the derivation across multiple dimensions. This work focuses on finite-dimensional, orthonormal-basis-indexed measurements and pure states. Extensions to mixed states, generalized POVMs, and continuous observables are left for future investigation. Note: Parts of the manuscript were linguistically and structurally refined with the assistance of AI-based tools.All scientific content, analysis, and conclusions are the author's own. Note: This work represents Version 1.0 of an ongoing research program on the Order-Projection Principle (OPP). Minor typographical corrections and clarifications may appear in later versions. The core conceptual claims remain unchanged.
Collapse-free quantum theories face a specific probability problem. If unitary evolution contains every measurementoutcome, an internal observer still needs a principled way to weight alternatives unequally. This article formulates threerequirements on such a weighting rule: coherence under changes of descriptive grain, stability under branch-preservingdynamics, and convergence between observers who share the same data. The main result is that the Born rule isforced along two independent routes. First, grain coherence, together with positivity, normalisation, and a minimalnull-support axiom, yields the hypotheses needed for Gleason’s theorem. In this route, the usual non-contextualityassumption is not postulated; it follows from refinement coherence itself. Second, dynamical stability and the samenull-support axiom recover the Born rule by importing Short’s theorem (2023), then extend the result to coarser grainsby refinement. Intersubjective convergence is therefore not an independent axiom but a corollary. The central theorem ofthe descriptive route has been mechanically verified in Lean 4 with Mathlib for an arbitrary perspective and cell, moduloa single explicitly isolated Gleason axiom. This verification does not prove Gleason’s theorem itself, and the dynamicalroute remains dependent on Short’s published proof. The result clarifies what the formal derivation establishes and whatremains outside it: the remaining step is the normative bridge from the characterised measure to rational expectation.
How much unitary symmetry does the Born exponent actually need? Within coordinate-additive probability rules—each outcome weighted by a function g of its amplitude modulus—invariance under a single genuine two-coordinate mixer already forces the quadratic g(x)=cx2 for every dimension n≥3, where the standard route (Gleason 1957; Hossenfelder 2021; Gogioso 2023) assumes the full unitary group. A single beam-splitter-like unitary on two coordinates, with phase freedom, reduces the invariance condition to a measurable Jensen (midpoint) functional equation whose only solutions are quadratic; the forced weight functional obeys the parallelogram law, so Jordan–von Neumann polarization reconstructs the inner product. The result is a characterization and a no-go, not a derivation of the Born rule: any axiomatization in this class demanding even one genuine mixing symmetry has already presupposed the inner product, so ‘why the exponent is two’ coincides with ‘why coordinate mixing is unitary’. Generalized permutations alone leave the exponent free; the forcing fails at n=2, mirroring Gleason’s dimension threshold; and the intermediate regime is empty for the two symmetry classes treated. Exact-arithmetic and numerical certificates are included. Target venue: Foundations of Physics. v2 (August 2026) — premise-level correction. The symmetry premise is restated at the level at which it holds, the weight functional: invariance of the normalised probability rule does not follow from it, and an explicit counterexample is given. A global probability-level invariance premise is shown to be vacuous for any genuine mixer with non-vanishing quadratic weight, and domain-of-definition conditions are made explicit. A prior-art and novelty assessment accompanies this version. Earlier versions remain in the version history.
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