Verification, limitations and reproducibility

Verification, limitations and reproducibility

Mathematical and computational evidence. The general source–readout results are proved in the text. The verification package also includes exact-arithmetic and finite-model checks of the formulas used by the reconstruction. The retained arithmetic suite records 28 passing checks: angular moments and the pole coefficient; the stress stencil moments; the free Hessian and third derivative, detector tables and conserved combination; the differentiated covariance; the Laplacian and regularized fundamental solution; the rotation idempotents; the exponent systems and activity rates; the beacon fourth difference; calendar plateaus; and shooting coefficients. Its script and receipt are verification/check_lift_numbers.py and the corresponding result record.

The retained structure suite records nine passing checks. It tests frame equivariance and fibre transitivity on the symmetric group on three letters over a triangle, the automorphism/stabilizer and holonomy-centralizer identifications, the fibre law, fan automorphisms and the single-axis exterior-division identity. Its script is verification/check_lift_structure.py. The focused amendment suite separately checks the ordered noncommutative residual, distinct base and varied Gaussian covariances, the two-sided shooting band, geometric radius matching, principal predictor cancellation and the Gaussian normalization. Records distinguish retained results from executions made for this release. Finite computations support these specific calculations; the general proofs are the displayed arguments.

Scope. The reconstruction takes the expanded translation of OpenAI’s underlying Lean construction as its mathematical input; it does not re-execute or independently certify that formal development. The recovered conclusions retain the supplied hypotheses and comparison classes, and do not assert a positive mass gap. The group, dimension, Wilson action and physical preparation remain realization inputs. Native admission establishes the supporting structure, while the specific operators, estimates and choices give the Yang–Mills realization described in the body.

Several recovery statements have essential local qualifications. On gauge-invariant quantities the frame reader is an identity encoding; its larger role is to organize compatible non-invariant charts and the interfaces of Table 2. The label-reader inverse is bounded at each fixed level,

rather than uniformly in the level (Theorem 16.3). Beacon constants belong to the fixed reference tori. Scaling maps retain their selected radius sequences (Theorem 23.2), and calibrated-history uniqueness is within the fixed recipe (Theorem 14.29). The proof of the full trace limit uses the stronger universal subsequence property on the same table and phase. These qualifications are retained in the respective mathematical statements.

Reproducibility. The shared release contains both complete editable LTEX trees, the unchanged expanded source, source coverage and amendment records, the focused checks and the retained arithmetic and structure suites with their receipts. Build instructions identify the toolchain and commands, and output hashes bind the resulting files. The PDFs are compiled with resolved references and inspected in rendered form. The source–readout definitions and essential proofs are included in this article; no private methodological file is required to read or reproduce its mathematical presentation.