A post-release exact-arithmetic audit found a load-bearing global-amplitude gap in the Bellman upper-bound assembly of the earlier releases (v1.0.0-v1.2.0). Those releases are preserved as historical records; their exact-optimum, nonattainment, spatial-separation, and nonclosure claims are under correction and are not asserted by this version. What this version rigorously and unconditionally certifies: 0.2508753845015185 < omega_tensor <= omega_commuting <= 0.250875388108398 (window width 3.61e-9), with the lower endpoint an explicit 255-dimensional rational tensor-product strategy verified in exact arithmetic and independently reconstructed at 160-digit interval precision, and the upper endpoint an exact rational Bellman subsolution with an endpoint-clustered 25,601-knot witness, independently reconstructed cell by cell. The certificate stack, the audit that found the gap, a structural explanation (Bellman contact versus amplitude-normalization duality), and one recorded failed quantitative prediction are all included. Every load-bearing claim maps to replayable source and a frozen receipt.
A post-release exact-arithmetic audit found a load-bearing global-amplitude gap in the Bellman upper-bound assembly of the earlier releases (v1.0.0-v1.2.0). Those releases are preserved as historical records; their exact-optimum, nonattainment, spatial-separation, and nonclosure claims are under correction and are not asserted by this version. What this version rigorously and unconditionally certifies: 0.2508753845015185 < omega_tensor <= omega_commuting <= 0.250875388108398 (window width 3.61e-9), with the lower endpoint an explicit 255-dimensional rational tensor-product strategy verified in exact arithmetic and independently reconstructed at 160-digit interval precision, and the upper endpoint an exact rational Bellman subsolution with an endpoint-clustered 25,601-knot witness, independently reconstructed cell by cell. The certificate stack, the audit that found the gap, a structural explanation (Bellman contact versus amplitude-normalization duality), and one recorded failed quantitative prediction are all included. Every load-bearing claim maps to replayable source and a frozen receipt.
This preprint constructs finite rational proof objects for both sides of the quantum value of I3322 Bell inequality. Let 𝑄t denote the supremum over finite-dimensional tensor-product binary measurements and𝑄c the commuting-operator value. On the complete word space of total length at most four, we construct a rational Gram certificate. The full signed setting-relabeling stabilizer is the dihedral group of order eight, reducing the certificate to five rational blocks. Ex-act affine reconstruction and a uniform diagonal shift of certified positive interior prove: 𝑄c (𝐼3322) ≤ 62718846253/250000000000 = 0.250875385012. Independently, a local-dimension-499 strategy specified by rational projectors and a nonzero unnormalized rational Schmidt vector has exact normalized value 𝐿499 = 0.25087538451397653548 . . .. Con-sequently, 𝐿499 ≤ 𝑄t(𝐼3322) ≤ 𝑄c (𝐼3322) ≤ 0.250875385012, with endpoint difference below 5 × 10−10. The lower certificate also proves 𝑄t(𝐼3322) > 1/4. Every theorem is checked using exact rational or integer arithmetic; floating-point computation is used only to discover candidates. Complete certificates, source code, tests, and reproducibility materials are archived at: doi:10.5281/zenodo.21462892.
We determine the quantum value of the three-setting, two-outcome Bell functional I3322. The value is the unique intersection q† of an analytic A-high stable curve of the exact Jacobi characteristic map with a central reverser curve. A computer-assisted proof isolates this intersection in a rational interval of width 10−55, beginning 0.2508753845139765356173366109459512989013219739714764755. We prove that the supremum over finite-dimensional tensor-product strategies, the unrestricted spatial value and the commuting-operator value all equal q†. No finite-dimensional strategy attains the value, whereas a normal infinite-dimensional spatial strategy and a commuting GNS strategy do. The proof combines an exact Bellman/path variational reduction, extraction of a positive bilateral calibrated Jacobi fibre from a maximizing weak-star state, a reflected-fibre central-incidence theorem and interval certificates for the unique stable/central intersection. A separate operator-positive three-remainder decomposition gives the commuting upper bound. The complete verification record is archived at DOI 10.5281/zenodo.22160086.
This record contains the manuscript and complete verification artifact for the Bell inequality J62_4422 of Pál and Vértesi.It certifies the exact rational bracket750075557472719639 / 10^18 ≤ β_Q ≤ 750091086083765047288227625 / 10^27,and exact attainment of 3/4 by the stated two-qubit strategy. The lower endpoint is an exact rational strategy. The upper endpoint is certified by a sum-of-squares chain for the retained 365-word relaxation level.The Krawczyk certificate localizes the underlying KKT zero and establishes a strict local maximum, including negativity of the border form in all 256 boundary strata; it does not establish global optimality of that localized point. Accordingly, this work does not claim the exact quantum value, qubit-restricted optimality, minimum optimizer dimension, or global optimality of the localized KKT point.The archive includes SHA-256 manifests, standard-library replay programs, independently written certificate checks, mutation controls, and pinned full Krawczyk replays. The acceptance programs are fail-closed under optimized Python. The manuscript and certificates are licensed CC BY 4.0; verification code is licensed MIT.Version 1.1 is a hygiene-only update: it replaces one machine-local default path in a helper with the portable repository root ".", updates the corresponding checker and certificate source bindings, and leaves the mathematical calculation, inputs, claims, and replay outputs unchanged.
A Kernel-Role Determinacy Theorem for Bell-Witness Fixation, No-Signaling, and Tensor-Level Compatibility This manuscript develops a fixed-domain AASC analysis of Bell-nonlocal quantum entanglement as a theorem of reusable witness determinacy. It does not introduce hidden variables, modify quantum mechanics, derive Hilbert-space formalism from below, or propose a new signaling mechanism. Instead, it asks a prior structural question: once a Bell-type operational family is used as the same non-degenerate witness across settings, lawful transformations, retained records, comparison, and later classification, what admissible same-domain standing form is forced? The governing claim is that AASC is not an optional interpretive overlay on physics. Once an operational Bell family is asserted as a determinate reusable witness, admissibility, standing, reference, and irreversibility are already active as minimal necessity conditions of same-witness objecthood. Target instantiation therefore carries governance occupancy: an alleged determinate Bell witness with no admissible governance realization is not an empty alternative, but a refusal or retyping of the target. The manuscript defines finite operational Bell objects with explicit setting carriers, outcome families, channel/interface data, standing-token valuations, continuation and report/reuse structure, comparison profiles, and act-time status. It then defines object-indexed query sorts, dependent response families, exactly recoverable operational simulations, lawful Bell groupoids, six governance-effect functors, and target-active extensional governance equivalence. The result is a typed interface in which arbitrary native formalisms can be compared by their target-bearing governance effects rather than by their internal syntax. The central Bell-specific theorem states that every same-target candidate-admissible Bell-governance construction is forced component by component into the certified boundary-compatible standing form on the complete target-active practice. Candidate admissibility does not assume the canonical form at the outset. Instead, target occupancy, lawful transport, standing-flow exclusion, compatibility certification, coordinate-deviation exhaustion, and componentwise closure force exact target-bearing realization and governance equivalence to the canonical representative CP∗C^{*}_{P}CP∗. The target-induced governance quotient therefore has exactly one element. The Bell carrier is treated as a compatible empirical model on a finite measurement cover. Bell-local completion is identified with the existence of a global section, and Bell nonlocality is the obstruction to such a section. The manuscript separates operational marginal invariance, absence of controllable communication, and exclusion of same-domain standing transport. No-signaling is therefore preserved without retyping Bell nonlocality as superluminal communication, metric transport, distant repair, or hidden standing transfer. The finite-dimensional quantum specialization uses the standard bipartite tensor-product and local-POVM carrier. Every separable realization in that carrier is Bell-local; therefore, if the fixed Bell-nonlocal empirical model has such a finite-dimensional quantum realization, every realizing state in that carrier is entangled. Post-quantum Bell-nonlocal no-signaling models remain within the general witness theorem but outside the quantum-entanglement corollary. The accompanying Lean 4 development, release v0.8.0, directly verifies the finite Bell-side witness carrier: denominator-32 vector/Born weights, structural no-signaling, CHSH numerator 808080, all sixteen deterministic local extrema, finite denominator-32 Bell-local-envelope exclusion, and conditional endpoint routing. Its direct witness certificate is vectorBorn_flagship_spine, and its deepest released endpoint is reasonableDeepestFiniteEntanglement_spine. The manuscript-level typed governance interface, empirical lawful groupoid, compatibility equivalence, coordinate-deviation exhaustion, completed role collapse, candidate-to-canonical derivation, and finite-dimensional quantum specialization are not attributed to the released Lean layer. This paper is the Bell-witness member of the paired AASC quantum determinacy arc. The record-side manuscript, Admissible Record Construction in Physically Non-Selective Quantum Regimes, fixes when local physical record occurrences stand as the same evidential record objects. The present manuscript fixes when the Bell operational family sampled by such records stands as the same reusable witness. The paired endpoint is therefore: record-role fixation+Bell-witness compatibility.\text{record-role fixation} + \text{Bell-witness compatibility}.record-role fixation+Bell-witness compatibility. The manuscript is classificatory and eliminative rather than mechanistic. It does not claim that AASC generates the Bell probabilities or supplies a hidden physical influence. Its claim is that reusable Bell-witness determinacy strongly constrains how Bell-nonlocal correlations may be coherently classified on a fixed domain: not as independently complete local states later connected by a mechanism, not as Bell-local hidden-variable value assignments, not as superluminal signaling, and not as same-act repair, but as boundary-level compatibility carried by one standing-preserving Bell witness.
Let S be the common tensor-product and commuting-operator supremum of the I3322 Bell functional in the Collins-Gisin normalization. Starting from a certified value window and Bellman/path equivalence, we prove that no finite-dimensional quantum strategy attains S, whereas a spatial strategy on ℓ2(Z)⊗ℓ2(Z) does. The finite-dimensional statement includes mixed states and binary POVMs. Consequently Cq(3,3;2,2) is not closed and Cqs(3,3;2,2)∖Cq(3,3;2,2) is nonempty. We also establish the dimension complexity D(ε)=Θ(log(1/ε)): approaching S requires and suffices local dimension logarithmic in inverse error. The constructive upper bound is D(ε)≤23.9010650log(1/ε) for all sufficiently small ε, with natural logarithms; the lower constants are existential. The proofs use critical Bellman storage, spectral transport and normalizable orbit measures. A finite weighted-flow argument supplies the unrestricted quantitative lower bound without identifying distinct joint spectral components. This revision replaces an unsupported step in the earlier lower argument and records additional proof corrections. Prior numerical certification and independent concurrent attainment results are credited. Exact arithmetic and Lean 4 check specified numerical, scalar and finite accounting facts; the complete analytic proof is not formalized.
Version 4 (2026-08-25). Two additions from the correction campaign, carried as dated in-body correction records. The (2,5) entry, printed as a prediction in v3, is now census-exact -- and it was the wall law's first divergence test. At the constructed maximal-wall stratum point the stiff transverse count is exactly 10, so alpha_stratum(2,5) = 5; a fresh 60k ensemble's calibrated read is consistent with 5, with alpha = 10 (the superseded single-wall count's prediction) excluded at p = 0.000 and demonstrated power ~ 1; and a stratum-conditional paired ladder tracks the exact rank-10 Hessian form to <= 0.002 while a rank-20 comparator separates by >= 2.7 on identical draws. The law m_C(2,d) = 2(d-1) is census-exact at d = 3, 4, 5, now including the first point where it diverges (by 2x) from the superseded count. The (3,4) entry, printed open in v3, is now a PAIR of statements, and neither alone is alpha(3,4). The posted product-wall counting landed census-exact (alpha_stratum(3,4) = 5, so the asymptotic exponent satisfies alpha(3,4) <= 5), while the accessible window at n = 3e4 is steeper (calibrated 90 percent set [5.4, 6.9], with the previously read 4.0-4.1 excluded at power ~ 1): the codim-10 stratum's prefactor has not engaged at reachable depth, and window and asymptote have visibly decoupled. This is the scope lesson of the (d >= 3) x (d' > d) regime -- census plus conditional ladder measure the law, global windows measure the pre-asymptotic shoulder -- and it retro-explains the earlier fresh-seed ladders' instability as shoulder reads. Version 3 (2026-08-20). One SUPERSESSION: the qutrit-qutrit exponent closes. Versions 1 and 2 left alpha(3,3) open, v1 by a small-sample fit reading 3.25 and v2 by the bracket [2.3, 3.0] read off a descending window ladder. Both readings were artifacts of the estimator problem for which the pair-type table was already corrected in v2. The descent is attenuation tracking sample count rather than tail depth: an ensemble drawn from an EXACT alpha = 3.0 law descends by 0.62 across the ladder against the real data's 0.34, so a descending ladder is evidence FOR a constant exponent, not against one. Replacing the window fit with a calibrated Monte-Carlo test and inverting it over candidate exponents gives alpha(3,3) = 3.0 at p = 0.517 with a 90 percent confidence set [2.75, 3.10]; v1's 3.25 is excluded at p = 0.017. Power against alternatives is 0.990 / 0.590 / 0.120 / 0.575 / 0.990 / 1.000 at true alpha = 2.50 / 2.75 / 3.00 / 3.25 / 3.50 / 4.00. An independent re-audit at n = 10^4 reads flat near three on two seeds. Disclosed defect, carried in the paper: the test's own calibration row missed at the low edge (rejection rate 0.207 at a nominal 0.10 when the truth is alpha = 2.50, 4.4 standard errors high), so the lower end of the confidence set is softer than printed. This ensemble separates 3.0 from 3.25 with about 58 percent power and has none to separate 3.0 from 2.95. The (3,3) CARRIER family remains unattributed: the exponent is settled, the stratum that carries the accessible tail there is not. Version 2 (2026-08). Changes from v1: the pair-type exponent table is corrected (v1's alpha(2,4) = 2.08 was a 50-sample order-statistics fluctuation, placed at the 0.15th percentile of its own estimator's sampling distribution; three independent codebases now agree on the wall law alpha(2,d) = d, census-exact at d = 3 and 4); the transverse constant 1/12 is derived in closed form (diagonal cost 1/6, halved by the congruent partner's equal-cost correction); the (2,3) tail's carrier stratum is fully attributed (an isotropic-intertwiner family sharing the exponent 3); the qutrit-qutrit exponent is honestly bracketed open at [2.3, 3.0]; and the dispersion rule (tail-exponent fits print bootstrap dispersion or do not print) is adopted. The v2 ledger appendix carries the correction anatomy. Why is the multipartite certification constant heavy-tailed, where does the tail live, and what kills it? Localization: the credential pencil is exactly block-diagonal over party-subset supports; the tail is the worst pair; geometry statistics reconstruct from pair statistics (14/14 factor-band comparisons). The law: a frame-congruence theorem: whenever the two parties' operation frames subtend equal Bloch angles, the rotation intertwining them is an exact common kernel direction; the zero set is codimension one at generic angles, transverse growth is universally quadratic (mu = (Delta theta)^2/12), and the qubit-pair tail exponent is exactly 1/2 (the previously measured 0.39 is the finite-window slope of this law). The dichotomy: pairs containing a d >= 3 party measure exponents 2.08 to 3.69 because higher-dimensional operation pairs carry many local invariants that must all match: freedom helps the certifier. Engineering: heterogeneous dimension profiles tame the tail; qubit-pair presence splits all measured geometries into two clean classes; screening is a five-minute two-party calculation. Pre-registered; two entry gates that caught wrong conventions and all deaths ledgered.