OMEGA NAUGHT — Integration Proofs Proofs of the stated OMEGA integration interfaces, not a certificate for the entire OpenAI mathematics release and not an assertion of all proposed applications. Execution: Python ran. Julia and Rust source was supplied but not compiled or executed here. See evidence/execution_status.json. Conventions The coefficient field in the executable algebra is Q(phi), with phi=(1+sqrt(5))/2 and phi^2=phi+1. Canonical s=sin(pi/1296000) is not silently replaced by a rational auxiliary seed. Contents • P00 — Meaning and soundness of the algebraic certificates • G01 — Whole-geometry similarity and invariant selected readouts • G02 — Exact conjugacy between scale and the affine contraction • G03 — Canonical algebraic landmarks • G04 — Transcendental readouts and nonvanishing real residuals • G05 — Gram equality, intrinsic dimension, and Hilbert embedding • C01 — Six-point polynomial code and exact error/erasure correction • C02 — Five weighted interval measurements form a polynomial code • C03 — Analog noise conditioning and invisible profiles • A01 — Exact finite certificate for real/rational floor agreement • A02 — Ordered Euclidean witnesses give exact integer-history reconstruction • A03 — First-residue inversion on the canonical interval • A04 — Exact separation of geometric, slope, and quantization errors • V01 — Intrinsic convex bodies and exact polar-volume products • T01 — Tensor-product reconstruction in multiple coordinates • H01 — Positive cubature gives harmonic reconstruction and a noise bound • H02 — Exact 12-node icosahedral instance and its first moment obstruction • O01 — The center-relative moment ellipse and its family inverse • O02 — Affine metric recovery and the feet-outside-ellipse correction • O03 — Constructive numerical-range representation of the ellipse • O04 — Exact operator norms and an elementary polynomial bound • O05 — Two infinite-dimensional operator extensions with different behavior • O06 — A quantitative nonlinear solvability class • S01 — Correct symplectic normalization • I01 — Finite probes measure a compression, not an arbitrary whole operator • I02 — What a six-port series-chain impedance measurement can recover • I03 — A dense-probe limit and its conditional inverse-problem consequence • I04 — Finite-compression transfer of a uniform operator bound • M01 — A local OMEGA placement on a smooth manifold and its exact metric contract • F01 — Similarity covariance of forced incompressible Navier-Stokes and observers • B01 — Exact reversible quantization of full-rank integer linear layers • B02 — Boolean implementation and reversible gate embedding • B03 — Byte towers, retained length, and information costs • U01 — A composable geometric-to-computational reconstruction theorem Theorems and proofs P00 — Meaning and soundness of the algebraic certificates Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: CHECKER_SEMANTICS_ARGUMENT. Assumptions 1. The coefficient phi denotes (1+sqrt(5))/2. Rational operations are exact. Polynomial variables are commuting indeterminates. 2. Trust the supplied interpreter implementation and the language arithmetic libraries; no separate formal verification of that software is asserted. Statement. A successful eq check proves the displayed polynomial identity for every real specialization of its indeterminates. A successful positive_constant check proves a strict inequality for the displayed exact constant. Proof. 1. The polynomial X^2-X-1 has irrational roots, so the representation a+bphi with rational a,b is unique. Its multiplication law is (a+bphi)(c+d*phi)=(ac+bd)+(ad+bc+bd)*phi. 2. An expression denotes a finite map from monomial exponent vectors to coefficients. Addition combines equal exponents, multiplication convolves exponents and multiplies coefficients, and zero coefficients are removed. These operations follow distributivity. 3. Structural induction over the instruction DAG proves that each register contains the polynomial denoted by its instruction. The power instruction uses repeated multiplication. The derivative instruction implements the exact monomial power rule. 4. Two identical coefficient maps denote the same polynomial. Thus a zero difference proves an identity for all substitutions, rather than agreement on finitely many sampled inputs. Conversely a nonzero polynomial need not be nonzero at every substitution; the checker therefore permits numerical inequality claims only when the difference has no variables. 5. For a constant a+b*phi, rewrite it as (a+b/2)+(b/2)*sqrt(5). Equal-sign summands have that sign. Opposite-sign summands are compared by a rational squared-magnitude comparison. Irrationality of sqrt(5) prevents an unintended nonzero rational equality. Dependencies: None inside this ledger. Executable evidence: Written argument; no finite computation substitutes for this proof. Source records: New derivation in this bundle. Limits • The checker does not prove analytical limits, universal statements about arbitrary functions, or positivity under variable assumptions simply by normalizing a polynomial. Those require the written proofs below. • A JSON statement or a status field is not itself a proof. The executable instructions, derivations, hypotheses, and evidence have separate roles. • The source code and mathematical arguments were produced in one assistance workflow. Three language implementations are not three independent research reviews. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. G01 — Whole-geometry similarity and invariant selected readouts Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Fix the OMEGA unit-circle-derived curve K, its six labels, and its distinguished center. Let a>0, k>0, m be a center, and J be a real linear isometry of its construction plane into a real Hilbert space. 2. Use K_a=m+a*J(K), with the same opening angle, labels, and golden extensions at every scale. 3. The selected readouts are G(a)=aphi and C(a)=api. C is a selected path readout, not the retained major-arc length. Statement. H_k(K_a)=K_(ka) and H_k(P_i(a))=P_i(ka), where H_k(x)=m+k(x-m). Moreover G(a)/(G(a)+C(a))=lambda=phi/(phi+pi), independently of a. Proof. 1. Every point of K_a is m+aJ(u), u in K. Applying H_k gives m+kaJ(u), exactly the corresponding point of K_(ka). This proves a statement about the entire retained arc and both feet, not only six samples. 2. Linear similarity multiplies every chord length by k. Curve length is the supremum of sums of chord lengths over partitions, so every rectifiable selected path length also scales by k. 3. The readout ratio is aphi/[a(phi+pi)]. Since a>0 and phi+pi>0, cancellation yields lambda. Angles and normalized pairwise distances are unchanged by the real isometry and positive homothety. Dependencies: P00. Executable evidence: G01_SIMILARITY. Source records: SOURCE_INTEGRATION_2026_10_07, SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • The iteration k=lambda must be specified. The unit circle by itself does not logically select a unique contraction factor or iterative dynamics. • A general affine shear is not a Euclidean similarity. Its metric must be treated separately. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. G02 — Exact conjugacy between scale and the affine contraction Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Fix a_ref>0 and define v(a)=1+a/a_ref for a>=0. Define the scale update a_next=lambda*a. 2. lambda=phi/(phi+pi), so 02, giving real-subfield degree 345600. Dependencies: P00. Executable evidence: RUNTIME_CYCLOTOMIC. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • The degree is an ambient-field degree, not a minimal-degree claim for each coordinate. • Arbitrary real translations, orientations, and scales need not have algebraic coordinates. The claim concerns normalized coordinates in the declared frame. • Q(phi)-based executable fixtures with rational s are explicit auxiliary instances. They do not replace the canonical sine with a rational number. The large canonical cyclotomic field is not expanded by the programs. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. G04 — Transcendental readouts and nonvanishing real residuals Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Use the classical theorem that pi is transcendental, and closure of algebraic numbers under field operations. 2. phi is a nonzero algebraic number; Omega0=phi+pi and lambda=phi/(phi+pi). Statement. Omega0 and lambda are transcendental. In particular lambda differs from every rational q, and lambdad-floor(q0d) is nonzero for every positive integer d and every rational q0. Proof. 1. If Omega0 were algebraic, pi=Omega0-phi would be algebraic, a contradiction. 2. If lambda were algebraic, lambda>0 and pi=phi*(1-lambda)/lambda would be algebraic, also a contradiction. 3. If lambdad-floor(q0d)=0 for d>0, then lambda=floor(q0*d)/d would be rational. Therefore this residual cannot vanish. 4. When floor(q0d)=floor(lambdad), the residual equals the fractional part of lambda*d and lies strictly between zero and one. Outside that agreement domain the nonzero conclusion remains, but the upper bound one is not guaranteed. Dependencies: G03. Executable evidence: Written argument; no finite computation substitutes for this proof. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • Pi transcendence is a stated classical dependency, not newly reproved or kernel-checked here. • This does not transfer an irrationality exponent for rational approximations of pi to lambda. The inverse approximation target phi*(1-r)/r is generally algebraic irrational, not rational. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. G05 — Gram equality, intrinsic dimension, and Hilbert embedding Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Let (x_i) and (y_i) be finite families in real Hilbert spaces. 2. For OMEGA, a>0, 00, and p_i=a*(z_i,c). Statement. Equal Gram matrices are equivalent to a linear isometry between the generated spans sending x_i to y_i. The six marks alone have a one-dimensional distance realization; adjoining the circle center requires dimension two. A plane isometry into a larger Hilbert space preserves the entire curve but creates no new intrinsic degrees of freedom. Proof. 1. An isometry preserves inner products, giving one direction. Conversely define J(sum b_ix_i)=sum b_iy_i. Equality of Gram matrices gives equality of the squared norms of both sums and of differences of coefficient representations. Thus J is well-defined, linear, onto the target span, and isometric. 2. For the six marks, ||p_i-p_j||=a*|z_i-z_j|, so p_i mapped to az_i realizes all pairwise distances on a line. However the determinant of the two center-relative seed vectors (-as,ac) and (as,ac) is -2a^2sc, which is nonzero. Thus the center-augmented span is two-dimensional. 3. A real plane isometry preserves every chord. Taking the supremum over partition chord sums preserves rectifiable curve length. Its image remains in a translated two-dimensional plane even when the ambient Hilbert space is infinite-dimensional. 4. Finite landmark agreement without a restrictive map class is insufficient: F(x,y)=(x,y+ky(y-ac)) fixes the center and the entire mark line y=ac, but changes the retained bottom point (0,-a) for k!=0. Dependencies: None inside this ledger. Executable evidence: G02_GRAM_AND_DIMENSION. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • In a complex Hilbert space use the adjoint J*, not a transpose. The matrix [[5/4,3i/4],[-3i/4,5/4]] satisfies J^T J=I but ||Je1||^2=17/8, so a transpose test is not a complex-isometry test. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. C01 — Six-point polynomial code and exact error/erasure correction Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. z_1,…,z_6 are distinct labeled real nodes. Polynomials have degree at most d, 0<=d<=5. 2. Samples are exact. An error may replace an arbitrary labeled sample; an erasure has a known missing label. Statement. Evaluation E_d(p)=(p(z_i)) is a length-six linear code of dimension d+1 and minimum Hamming distance 6-d. Unique correction is guaranteed whenever 2e+r<=5-d. For affine fields d=1, this is 2e+r<=4. Proof. 1. A nonzero polynomial of degree at most d has at most d distinct real roots. Therefore any nonzero codeword has at least 6-d nonzero entries. This also proves injectivity and full rank of every selected (d+1)-row Vandermonde submatrix. 2. The polynomial product_(i in I)(x-z_i), with |I|=d, has zeros at exactly those d chosen nodes and nowhere else among the six. Hence the distance lower bound is attained. 3. Suppose two codewords could explain the same observed data with at most e errors and r labeled erasures. Their differences would be confined to at most 2e+r positions. If 2e+r<=5-d<6-d, this contradicts the minimum distance. 4. A finite decoder enumerates (d+1)-subsets of the nonerased labels, interpolates each, and retains a unique codeword within the declared discrepancy budget. Existence follows when the input truly has the stated corruption bound. Dependencies: None inside this ledger. Executable evidence: C01_SYMBOLIC_INTERPOLATION, C02_EXACT_DECODERS, C03_CODE_DISTANCE_MINORS. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • Exact-symbol corruption is not small analog noise. Sample quantization and numerical conditioning require their own bounds. • The generic verifiers check polynomial and inverse certificates. A callable exhaustive interval decoder is also included in the historical Python reference; no claim of a production decoder API in every language is made. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. C02 — Five weighted interval measurements form a polynomial code Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. t_1<…0 on [t_1,t_6]. 2. For 0<=d<=4, define I_d(p)j=integral from t_j to t(j+1) of w(t)*p(t) dt. Statement. The interval code has length five, dimension d+1, and minimum distance 5-d. Unique correction is guaranteed by 2e+r<=4-d. With w=1, det(B)=det(V)/120, where B_jk=(t_(j+1)^(k+1)-t_j^(k+1))/(k+1), k=0..4, and V is the six-node degree-five Vandermonde matrix. Proof. 1. If a nonzero p has zero weighted integral on an interval, it must vanish at an interior point. Otherwise continuity and positivity of w give a strict constant sign and a nonzero integral. Distinct disjoint open intervals supply distinct roots. At most d interval outputs can therefore vanish. 2. Any d+1 interval functionals have zero common kernel on the (d+1)-dimensional polynomial space, so they are independent. Impose zero values on any d functionals. There is a nonzero kernel polynomial, and it cannot vanish on another interval functional. Thus distance 5-d is attained. 3. The Hamming-distance argument of C01 yields the correction guarantee. At d=4 the distance is one: five quartic interval data have no redundant reading for error detection. 4. For the determinant formula, form the six-by-six antiderivative matrix whose columns are 1,t,t^2/2,…,t^5/5. Its determinant is det(V)/120. Apply the invertible row transformation that retains the first row and replaces each following row by its original row minus the preceding original row. This transformation has determinant one. The first column becomes (1,0,…,0)^T, and the remaining lower five-by-five block is B. Expansion in the first column gives the formula. Dependencies: C01. Executable evidence: C01_SYMBOLIC_INTERPOLATION, C02_EXACT_DECODERS, C03_CODE_DISTANCE_MINORS. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • A bad voltage tap can affect two neighboring differences. Counting bad taps is not the same as counting bad interval measurements. • Positive weight, known coupling, labeled intervals, and the polynomial model are essential. Trace reconstruction from unknown deletion positions is a different problem. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. C03 — Analog noise conditioning and invisible profiles Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Two labeled marks z_i=0) (-1)^k*x^(2k+1)/(2k+1) has its value strictly between adjacent partial sums. The programs use 50 terms for x=1/5 and 18 for x=1/239 to obtain exact bounds pi_l=0, and a finite horizon N>=0. 2. At each step d_(k+1)=floor(Qd_k/S) and rho_k=Qd_k-S*d_(k+1). Retain terminal d_N, ordered residues, Q,S,N. Statement. Each residue satisfies 0<=rho_k=0. Statement. x_N-d_N=(lambda^N-q^N)*d_0+sum_(k=0)^(N-1) q^(N-1-k)*e_k. For N>0 the quantization contribution is at least zero and strictly below (1-q^N)/(1-q). Proof. 1. Induction on N in the affine recurrence gives d_N=q^N*d_0-sum q^(N-1-k)*e_k. 2. Subtract this from x_N=lambda^N*d_0 to obtain the exact formula. It displays the slope-approximation term separately from the accumulated floor remainder term. 3. All powers q^j are positive and 0<=e_k<1. The geometric-series sum bounds the accumulated term by 0<=sum q^j*e0. Floor agreement further places it below one. Dependencies: A01, A02, G02. Executable evidence: A01_TELESCOPING_SYMBOLIC. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • Logging rho preserves the integer history exactly. It does not make geometric scaling, rational scaling, and flooring identical operations. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. V01 — Intrinsic convex bodies and exact polar-volume products Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. U=ac>0 and V=a(s+phi^2)>0. Use planar intrinsic area. 2. The center-augmented hull has vertices (0,0),(U,-V),(U,V); symmetrizing the center-relative landmarks gives [-U,U] x [-V,V]. 3. For a convex body containing the origin in its interior, Kpolar={y: x dot y<=1 for all x in K}. Statement. The triangle translated to its centroid has area product 27/4 with its polar. The symmetrized rectangle has area product 8. A product box in n independently supplied dimensions has polar-volume product 4^n/n!. These products are invariant under invertible linear maps. Proof. 1. The triangle has area U*V and centroid (2U/3,0). Its centered vertices are (-2U/3,0),(U/3,-V),(U/3,V). Intersecting the three defining half-planes of the polar gives vertices (-3/(2U),-3/(2V)),(3/U,0),(-3/(2U),3/(2V)). Their area is 27/(4UV); multiplying gives 27/4. 2. The rectangle has area 4UV. Its polar is U*|xi|+V*|eta|<=1, a diamond of area 2/(UV). Their product is eight. 3. For K=product_j[-w_j,w_j], volume(K)=2^nproduct w_j. The polar is sum_j w_j|xi_j|<=1. In each of 2^n orthants it is a simplex of volume 1/(n!*product w_j). Multiplication gives 4^n/n!. 4. For an invertible linear map A, (AK)polar=A^(-T)Kpolar. The volume factors |det A| and |det A|^(-1) cancel. Dependencies: None inside this ledger. Executable evidence: V01_CONVEX_POLARS. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • These are exact computations for these bodies, not proofs of a Mahler inequality for arbitrary convex bodies. • Taking the polar of a planar body in all of R^3 gives an unbounded normal direction. Use its intrinsic plane. • Independent extra axes are added constructions; they do not arise from merely embedding the same planar curve in a larger ambient space. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. T01 — Tensor-product reconstruction in multiple coordinates Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Use n explicit coordinate axes, with six distinct OMEGA nodes on each axis. Samples occupy the full product grid. 2. The field is a polynomial of degree at most five in each coordinate separately. Statement. The 6^n grid samples determine all 6^n coefficients uniquely. With two axes, Y=V_1CV_2^T and C=V_1^(-1)YV_2^(-T). Proof. 1. Each one-axis Vandermonde matrix V_j is invertible because its determinant is the nonzero product of node differences. 2. The product-grid evaluation matrix is the Kronecker product V_1 tensor … tensor V_n. Multiplying it by V_1^(-1) tensor … tensor V_n^(-1) gives the identity, by the defining multiplication rule for Kronecker products. 3. For n=2, arranging coefficients and values as matrices gives the displayed formula. The certificate checks all 1296 entries of the resulting 36-dimensional identity through exact tensor-factor products. Dependencies: C01. Executable evidence: T01_TENSOR_RECONSTRUCTION. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • One six-mark baseline does not supply 36 samples. The full two-axis grid must actually be measured. • This proves injectivity for the stated polynomial space, not a new matrix multiplication exponent, a fast Fourier transform on nonuniform nodes, or good conditioning in every dimension. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. H01 — Positive cubature gives harmonic reconstruction and a noise bound Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. sigma is normalized surface measure on a sphere. Positive weights w_i sum to one and the nodes integrate every polynomial restriction of degree at most 2L exactly. 2. Y_alpha is a real orthonormal spherical-harmonic basis for degrees 0..L. Let M_i,alpha=Y_alpha(x_i) and W=diag(w_i). Statement. M^T W M=I. For a bandlimited field y=Mc, c=M^T Wy. If y is perturbed by e, the coefficient error obeys ||c_hat-c||_2<=sqrt(sum_i w_i*e_i^2). At least (L+1)^2 nodes are necessary. Proof. 1. Every product Y_alpha*Y_beta is a polynomial restriction of degree at most 2L. Applying cubature gives its exact spherical integral, which is delta_alpha,beta by orthonormality. This proves the Gram identity. 2. Multiplying y=M*c by M^T W gives c. The matrix A=W^(1/2) M has orthonormal columns, so ||A^T||_2=1. Therefore ||M^T W e||=||A^T W^(1/2)e||<=||W^(1/2)e||. 3. The Gram identity makes M have full column rank (L+1)^2. Its number of rows, the node count, cannot be smaller. Dependencies: None inside this ledger. Executable evidence: H01_ICOSAHEDRAL_CUBATURE. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • For a particular rule, positive weights, normalization, and exactness through 2L must be verified. A claimed target degree is not a certificate. • The bound does not cover node-position errors, unknown calibration, or a true field outside the bandlimited model. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. H02 — Exact 12-node icosahedral instance and its first moment obstruction Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Use all 12 points (0,+/-1,+/-phi),(+/-1,+/-phi,0),(+/-phi,0,+/-1), at squared radius R2=phi+2, with weight 1/12 each. 2. Normalized unit-sphere versions are obtained by dividing all coordinates by sqrt(phi+2). Statement. The equal-weight rule is exact through degree five. It gives exact degree-two harmonic reconstruction in nine modes. It is not degree-six exact. Proof. 1. The identity phi^2=phi+1 puts every vertex on the sphere of squared radius phi+2. Sign changes force every moment with an odd exponent to vanish. 2. For degrees at most five, the remaining monomials are the constant, second moments R2/3, fourth single-coordinate moments R2^2/5, and mixed fourth moments R2^2/15. Direct substitution verifies all 56 monomials. The continuous second and fourth moments follow from rotational symmetry and the uniform distribution of a single coordinate on a sphere, or equivalently elementary spherical integration. 3. For features 1,X,Y,Z,XY,XZ,YZ,X^2-Y^2,2Z^2-X^2-Y^2, the exact discrete Gram matrix is diagonal with entries 1; R2/3 three times; R2^2/15 three times; 4R2^2/15; 4R2^2/5. Every entry is positive. Its inverse times M^T W is therefore a left inverse, proving the nine-mode reconstruction. 4. The discrete X^6 moment is (1+phi^6)/3. The continuous value is (phi+2)^3/7. Their difference is -(4*phi+3)/21, which is nonzero. Thus degree-six exactness fails. Dependencies: H01. Executable evidence: H01_ICOSAHEDRAL_CUBATURE. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • The six baseline marks are not these 12 spherical nodes. A separate radial/icosahedral generator is required. • Higher-frequency class-I grids and higher-degree OMEGA certificates are not re-executed in this bundle. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. O01 — The center-relative moment ellipse and its family inverse Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Use X=a*[[z_1,…,z_6],[c,…,c]], c=sqrt(1-s^2), 0r>0. The ratio R/r uniquely determines s within this family, and r then determines a. Proof. 1. Symmetry gives sum z_i=0, so LL^T is diagonal. Expanding sum z_i^2/6 with phi^2=phi+1 yields the displayed R^2. The second diagonal entry is a^2*c^2=r^2. 2. The difference R^2-r^2=a^2*(2s^2+2(phi+2)*s/3+phi) is strictly positive. Thus LL^T is positive definite. 3. For a target y, the least-norm preimage is q=L^T*(LL^T)^(-1)y. Its squared norm is y^T*(LL^T)^(-1)y, and every other preimage adds an orthogonal kernel vector. Therefore E is exactly x^2/R^2+y^2/r^2<=1. 4. Let h=2*(phi+2)/3 and q=(R/r)^2. The family equation is (q+1)s^2+hs+phi^2-q=0. The derivative numerator of (s^2+hs+phi^2)/(1-s^2) is h+2(1+phi^2)s+hs^2>0. Its range on (0,1) is (phi^2,infinity), giving a unique s. 5. A numerically rearranged exact root formula is s=2*(q-phi^2)/[h+sqrt(h^2+4*(q+1)*(q-phi^2))], followed by a=r/sqrt(1-s^2). Dependencies: None inside this ledger. Executable evidence: O01_MOMENT_AND_PULLBACK. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • This is not centroid covariance: subtracting the mean of the six marks removes the constant row and leaves rank one. • Two semiaxes recover the specified shape and scale, not arbitrary labeled point sets or world pose. Column permutations preserve XX^T. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. O02 — Affine metric recovery and the feet-outside-ellipse correction Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Let D=diag(R/a,r/a), H=D^(-T)D^(-1), with positive a,R,r. 2. A foot point on the original geometry is a*(+/- (s+ell),c), with ell>0 and s^2+c^2=1. Statement. (Dx)^T H(Dy)=x^T y. Ordinary target Euclidean angles need not be preserved. Every positive-length foot point maps outside the derived ellipse E under D. Proof. 1. Substitute H into the bilinear form: D^T D^(-T)D^(-1)D=I. Thus the original inner products and angles are exactly recovered when measured using the pullback metric H. 2. For x=(1,1), y=(1,-1), the original dot product is zero but the ordinary dot product of Dx and Dy is (R^2-r^2)/a^2, nonzero when R>r. 3. For a transformed foot point the ellipse membership expression is ((s+ell)^2+c^2)=1+2sell+ell^2>1. Only ell=0, the seed endpoint, is on the boundary. Hence the numerical-range ellipse is a derived measurement object, not a container for the entire affine-transformed OMEGA curve. Dependencies: O01. Executable evidence: O01_MOMENT_AND_PULLBACK. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • A claim that all positive-length feet lie inside this ellipse is false; the bundle records the counterexample rather than marking that claim proved. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. O03 — Constructive numerical-range representation of the ellipse Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. R>r>0, d=sqrt(R^2-r^2), and T=[[d,2r],[0,-d]] acts on C^2 with the Hermitian inner product. 2. W(T)={v* T v: ||v||=1}. Statement. W(T) is exactly the filled ellipse {x+i*y: x^2/R^2+y^2/r^2<=1}. Proof. 1. For a unit vector v=(v1,v2), put U=2Re(conj(v1)v2), V=2Im(conj(v1)v2), Z=|v1|^2-|v2|^2. Expanding gives U^2+V^2+Z^2=1 and vTv=rU+dZ+ir*V. 2. The normalized real and imaginary rows (r/R,0,d/R) and (0,1,0) are orthonormal. Their image of the unit sphere lies in the closed unit disk; thus the numerical value lies in the ellipse. 3. Conversely for x+iy in the ellipse, put q0=(rx/R^2,y/r,d*x/R^2), n=(d/R,0,-r/R), and tau=x^2/R^2+y^2/r^2. Then ||q0||^2=tau, ||n||=1, q0 dot n=0, and the projection of n is zero. Hence q=q0+sqrt(1-tau)n is a unit preimage of x+iy. 4. Every unit q=(U,V,Z) has a spinor preimage: when Z>=0 take v1=sqrt((1+Z)/2) and v2=(U+iV)/(2v1); when Z<0 take v2=sqrt((1-Z)/2) and v1=(U-iV)/(2v2). The selected denominator is nonzero in each branch. Direct substitution proves its norm is one and its Bloch coordinates equal q. This proves surjectivity onto the whole filled ellipse. Dependencies: O01. Executable evidence: O02_OPERATOR_ALGEBRA, O03_BLOCH_ELLIPSE. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • The executable Bloch construction uses the exact auxiliary axes (R,r,d)=(5,3,4). The general result is the analytic argument, not extrapolation from that case. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. O04 — Exact operator norms and an elementary polynomial bound Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. T,R,r,d are as in O03, and P is a polynomial, possibly with fixed-size complex matrix coefficients. Statement. T^2=d^2I, ||T||=R+r, ||T^(-1)||=1/(R-r), and ||P[T]||<=kappamax_(z in E)||P(z)|| with kappa=sqrt((R+r)/(R-r)). Proof. 1. Direct multiplication gives T^2=d^2I. The positive matrix T T has trace 2R^2+2r^2 and determinant (R^2-r^2)^2, so its eigenvalues are (R+r)^2 and (R-r)^2. Their square roots give the norm and minimum singular value. 2. Set B=[[1,-r/R],[0,d/R]]. Then TB=Bdiag(d,-d). The eigenvalues of BB are 1+r/R and 1-r/R. Thus ||B||*||B^(-1)||=sqrt((R+r)/(R-r)). 3. Polynomial functional calculus gives P[T]=(I tensor B)P[diag(d,-d)](I tensor B^(-1)), with tensor order adjusted by a unitary flip if necessary. Submultiplicativity bounds its norm by kappa*max(||P(d)||,||P(-d)||). Since +/-d belong to E, the maximum is bounded by max_E ||P||. Dependencies: O03. Executable evidence: O02_OPERATOR_ALGEBRA. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • This self-contained bound has constant kappa, not an asserted universal constant two. It does not prove the family-325 Crouzeix headline theorem. • A numerical-range representation alone does not imply arbitrary neural-network performance or optimization guarantees. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. O05 — Two infinite-dimensional operator extensions with different behavior Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. H=ell^2(N;C^2), T is as in O03, and w_n=2^(1-n). 2. Define K=direct_sum_n(w_n*T) and C=direct_sum_n(T). Statement. W(K)=W(C)=E. K is compact, infinite-rank, injective, and not Fredholm at zero; ||K-K_N||=(R+r)2^(-N). C is boundedly invertible, noncompact, with inverse norm 1/(R-r). For nonzero zeta, zetaI+exp(ipsi)K is Fredholm of index zero and fails to be invertible exactly at zeta=-exp(ipsi)sigmaw_nd for some n and sigma=+/-1. Proof. 1. A unit vector distributed among the blocks produces a convex combination of block numerical values. Since each w_n*E lies in the closed convex set E and the first block realizes every point of E, both direct sums have numerical range E. 2. The norm of a block-diagonal operator is the supremum of its block norms. Therefore omitting all blocks after N leaves exact error (R+r)*w_(N+1)=(R+r)*2^(-N). Finite-rank approximation proves compactness of K. Every block is invertible, so K is injective with infinite rank and its range contains every finitely supported vector. 3. Unit +d eigenvectors supported in later blocks have images of norm w_n*d tending to zero. An injective bounded operator with closed range is bounded below. Hence the dense range of K is not closed, so K is not Fredholm. 4. The constant direct sum of T^(-1) is a bounded inverse for C with norm 1/(R-r). Fixed unit vectors in distinct blocks have mutually orthogonal images of a fixed nonzero norm, excluding compactness. 5. Conjugation by the bounded block diagonalization from O04 reduces zetaI+exp(ipsi)K to diagonal scalars zeta+exp(ipsi)sigmaw_n*d. For zeta!=0 all sufficiently late scalars have modulus at least |zeta|/2. Only finitely many earlier coordinates can be exceptional, and at most one scalar vanishes. Kernel and cokernel then have equal dimension zero or one, proving the classification. Dependencies: O03, O04. Executable evidence: O02_OPERATOR_ALGEBRA. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • Finite matrix checks do not prove the infinite-dimensional conclusions; the compactness, norm-limit, and range arguments do. • For a translated ellipse, truncation must retain the scalar tail zeta*I. An unshifted zero tail can enlarge the numerical range. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. O06 — A quantitative nonlinear solvability class Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. C is the constant-block operator in O05, considered on its real underlying Hilbert space if needed. 2. N:H->H is globally Lipschitz with constant L_N=(R-r)||z|| gives (R-r-L_N)||x-x_tilde||<=||y-y_tilde||. Dependencies: O05. Executable evidence: O02_OPERATOR_ALGEBRA. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • A particular nonlinear neural layer must satisfy the stated global Lipschitz margin. It is not inferred merely from an ellipse drawing. • Fredholm properties by themselves do not give this contraction estimate, endpoint compactness, or a global continuation theorem. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. S01 — Correct symplectic normalization Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Use standard planar J2=[[0,1],[-1,0]] and an invertible real 2x2 matrix D with positive determinant. 2. For the ellipse chart D=diag(R/a,r/a), a,R,r are positive. Statement. D^T J2 D=det(D)J2. The original ellipse chart is symplectic exactly when Rr=a^2. D_sp=(det D)^(-1/2)*D=diag(sqrt(R/r),sqrt(r/R)) is symplectic. Proof. 1. Multiplying a general 2x2 matrix [[u,v],[w,z]] on both sides of J2 gives (uz-vw)*J2. Thus preservation of J2 is equivalent to determinant one in dimension two. 2. Multiplying D by the scalar (det D)^(-1/2) multiplies its determinant by (det D)^(-1), giving determinant one. The diagonal formula follows by cancellation. 3. For the canonical small opening, 05/2. Therefore (Rr/a^2)^2=[s^2+2(phi+2)s/3+phi^2](1-s^2)>(5/2)*(1-10^(-10))>1. So the unnormalized canonical ellipse chart is not symplectic. 4. Repeating a fixed bounded invertible D_sp on ell^2(N;R^2) preserves the continuous bilinear symplectic form obtained by summing the standard forms on each block. Cauchy-Schwarz guarantees convergence of the sum. Dependencies: O01. Executable evidence: S01_SYMPLECTIC, O01_MOMENT_AND_PULLBACK. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • Normalization changes the overall image size relative to D while preserving aspect ratio. • This linear preservation theorem is not a nonlinear symplectic embedding theorem and does not establish a ball-packing bound. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. I01 — Finite probes measure a compression, not an arbitrary whole operator Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. H is a real Hilbert space, Lambda is a bounded operator representing a declared response law, and P:R^m->H sends coefficients to specified probe profiles. 2. Let E=P* Lambda P. Suppose range(P) has nonzero orthogonal complement. Statement. E determines the complete bilinear response on the span of the selected profiles, but generally does not determine Lambda on H. Proof. 1. For coefficient vectors a,b, a^T E b=. Thus E records precisely the bilinear response restricted to the probe span. 2. Choose nonzero v orthogonal to range(P), and define D(x)=v. Then PDP=0 although D!=0. Consequently Lambda and Lambda+D have identical measured E. 3. The finite certificate uses P selecting the first two coordinates of R^3, Lambda1=diag(1,2,3), and Lambda2=diag(1,2,7). Both measured matrices equal diag(1,2), but the full operators differ. Dependencies: None inside this ledger. Executable evidence: I01_BOUNDARY_AND_COMPRESSION. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • The counterexample is for bounded operators. It does not assert that every invisible rank-one perturbation is realizable by a particular physical conductivity or Riemannian metric. • Physical uniqueness requires a separate structural theorem and satisfaction of its hypotheses. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. I02 — What a six-port series-chain impedance measurement can recover Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. There is a known five-edge series chain joining six nonloading labeled voltage taps. A known nonzero current I traverses every edge. 2. Edge resistances obey V_j-V_(j+1)=I*R_j. Statement. One complete voltage reading recovers all five resistances R_j=(V_j-V_(j+1))/I. A common additive voltage is unobservable. On a general reciprocal six-port response, the balanced-current/voltage-quotient space has dimension five and a symmetric response has at most 15 independent entries. Proof. 1. Kirchhoff current conservation in the known series topology forces the same current through every edge. Applying the stated edge law gives the inverse formula directly. 2. The five-by-six difference matrix annihilates the all-ones vector and has rank five, as its first five columns form an invertible triangular matrix. Thus only the common voltage offset is lost. 3. A general reciprocal six-port operator acts on the five-dimensional balanced-current space after fixing the voltage gauge. A symmetric five-by-five matrix has 5*(5+1)/2=15 independent entries. A single applied current produces one response vector, not this entire general response matrix. Dependencies: I01, C02. Executable evidence: I01_BOUNDARY_AND_COMPRESSION. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • Measuring a fabricated chain on a manifold need not identify properties of the underlying manifold. A host-coupling constitutive law must be specified and calibrated. • Unknown contact loading, topology, current, or coupling changes the inverse problem. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. I03 — A dense-probe limit and its conditional inverse-problem consequence Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. U_1 subset U_2 subset … are finite-dimensional subspaces with dense union in a real Hilbert space H. 2. B_1,B_2 are bounded bilinear forms that agree on every pair in each complete U_m. Statement. B_1=B_2 on H x H. If a separately valid physical uniqueness theorem applies to these full response forms and all its domain, regularity, boundary, bundle, and gauge hypotheses hold, its recovery conclusion then follows. Proof. 1. For u,v in H choose u_m,v_m in U_m with u_m->u and v_m->v. Boundedness gives |B_j(u_m,v_m)-B_j(u,v)|<=||B_j||(||u_m-u||||v_m||+||u||*||v_m-v||), which tends to zero. 2. Equality on U_m therefore passes to the limit. For symmetric real forms, cross terms can be recovered from B(u,v)=[B(u+v,u+v)-B(u-v,u-v)]/4. Complex Hermitian forms require the corresponding imaginary polarization information as well. 3. Equality of isolated per-placement blocks is not enough. For example I_2 and [[1,1/2],[1/2,1]] have equal restrictions to either coordinate axis but differ on cross terms. The assumption requires the complete increasing span, including cross-placement interactions. 4. Once full response forms are equal, a separately supplied uniqueness theorem may be applied. This last implication is conditional on that theorem and its hypotheses, not a proof of them. Dependencies: I01. Executable evidence: I01_BOUNDARY_AND_COMPRESSION. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • This is an infinite-data limit, not a finite-sample rate or a universal finite six-port manifold decoder. • No headline reconstruction theorem from release families 365 or 372 is certified by this implication. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. I04 — Finite-compression transfer of a uniform operator bound Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. A is bounded on a complex Hilbert space. P has degree d and fixed matrix size m. 2. Assume a dimension-independent bound ||P[B]||<=C0*sup_(z in W(B))||P(z)|| holds for every finite-dimensional B. Statement. The same bound holds for A. The correct compression uses spans of iterates, not arbitrary point sampling. Proof. 1. For a vector xi=sum_(j=1)^m xi_j tensor e_j, let V=span{A^k xi_j:0<=k<=d,1<=j<=m}, whose dimension is at most m*(d+1). Put A_V=projection_V*A restricted to V. 2. Induction gives A_V^k xi_j=A^k xi_j for k<=d: every required next iterate is already in V. Thus P[A_V]xi=P[A]xi after the natural inclusion. 3. For a unit v in V, =, so W(A_V) subset W(A). Apply the assumed finite bound to A_V and then take the supremum over unit xi. This proves the Hilbert-space bound. 4. The iterate condition matters: with A=[[0,1],[1,0]] and V=span(e1), A_V=0 but projection_V*A^2 restricted to V is the identity. Arbitrary compression does not commute with polynomial evaluation. Dependencies: None inside this ledger. Executable evidence: I01_BOUNDARY_AND_COMPRESSION. Source records: SOURCE_OPERATOR_AUDIT_2026_10_07. Limits • This proves the transfer conditional on a uniform finite bound. It does not supply the finite bound with C0=2. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. M01 — A local OMEGA placement on a smooth manifold and its exact metric contract Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. M is a smooth Riemannian manifold of dimension m>=2. K is the compact planar OMEGA curve and marks. 2. Choose a coordinate chart psi:U->V subset R^m, a point in V, and a rank-two linear inclusion J:R^2->R^m. Statement. A sufficiently small translated/scaled copy of K embeds in U through psi^(-1). Its measurement metric is the pullback g_pull=(DF)^TgDF. Coordinate placement alone does not preserve the original Euclidean lengths or identify the host geometry. Proof. 1. Because V is open, it contains a ball about the chosen point. Because K is compact, it is bounded. Choose a positive scale small enough that the translated J(a*K) lies in that ball. 2. The map F=psi^(-1) composed with this affine inclusion is injective on K, and extends smoothly with rank two on a neighborhood in the construction plane. It is thus a local embedded copy, with the topology of the compact curve preserved. 3. By the definition of pullback, the inner product of pushed-forward tangent vectors DFu and DFv is u^T*(DF)^TgDF*v. This proves the metric formula, and corresponding curve lengths follow by integrating sqrt(g_pull(dot gamma,dot gamma)). 4. Nothing in a coordinate chart guarantees g_pull=I. The measured host response also depends on the specified coupling law. Finite observations inherit the nonuniqueness limits of I01-I03. Dependencies: G05, I01. Executable evidence: I02_CHART_METRIC. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • The whole planar construction needs host dimension at least two for this local embedding statement. A baseline alone has a different dimension requirement. • Global embeddings, global isometry, and reconstruction of an arbitrary manifold do not follow from this local chart argument. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. F01 — Similarity covariance of forced incompressible Navier-Stokes and observers Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. Smooth U,p,f solve U_t+(U dot grad)U=-grad p+nu*Delta U+f and div U=0 on a specified domain, with nu>0. 2. a,kappa>0, R is orthogonal, b is a fixed translation. Set xprime=aRx+b, tprime=kappa*t. 3. All fields, domain, initial/boundary data, and observers are transformed by the stated inverse coordinate map. Statement. Uprime=(a/kappa)RU, pprime=(a^2/kappa^2)*p, fprime=(a/kappa^2)Rf, nuprime=(a^2/kappa)*nu solve the transformed equation. kappa=a^2 preserves the numerical viscosity. Particle trajectories and corresponding observer-entry events are transported exactly. Proof. 1. The chain rule gives partial_tprime=(1/kappa)*partial_t and spatial gradient (1/a)*R times the old gradient on scalars. Orthogonality gives Delta_prime=(1/a^2)*Delta. 2. The time derivative, convection, pressure-gradient term, viscosity term with nuprime, and forcing all acquire the same common vector factor (a/kappa^2)*R. The divergence acquires scalar factor 1/kappa, so incompressibility is preserved. 3. If xdot(t)=U(x(t),t), then xprime(tprime)=aRx(tprime/kappa)+b has derivative Uprime(xprime(tprime),tprime). For Oprime=aRO+b, x(t) in O iff xprime(kappa*t) in Oprime at every time. 4. The executable polynomial instance uses U=(y^2t,0,0), p=0, nu=3/2, f=(y^2-3t,0,0). After a=2,kappa=4, a quarter-turn in the xy plane and b=(1,-3,0), Uprime=(0,(xprime-1)^2tprime/32,0) and fprime=(0,((xprime-1)^2-3tprime)/32,0). Formal polynomial differentiation verifies the divergence and all three PDE components identically. Dependencies: G01. Executable evidence: F01_FORCED_FLOW. Source records: SOURCE_INTEGRATION_2026_10_07. Limits • A nonorthogonal affine change does not preserve the same isotropic-viscosity equation under these formulas. • The polynomial shear is a smooth local/manufactured example, not finite-energy global data on all of R^3. • This theorem transports a supplied computation/observer correspondence. It does not construct a universal machine, prove its reachability claims, prove Navier-Stokes regularity or blowup, or equate the scalar floor map with fluid dynamics. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. B01 — Exact reversible quantization of full-rank integer linear layers Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. x belongs to a declared subset D of Z^n. W is an integer m-by-n matrix, b is an integer vector, and S_layer is a positive integer. 2. Define y_j=floor((Wx+b)_j/S_layer), r=Wx+b-S_layer*y, retaining the entire ordered residue vector. Statement. The encoding x -> (y,r) is injective on D exactly when ker(W) intersects (D-D) only at zero. In particular full column rank over Q guarantees injectivity on all Z^n. With a rational left inverse L, recover x=L*(S_layer*y+r-b), then verify integrality and re-encoding. Proof. 1. Euclidean division gives 0<=r_j(a,b,c xor (a and b)) is self-inverse, as applying XOR by the same bit twice restores c. It can compute AND while retaining its inputs. More generally a finite classical Boolean function f can be embedded as (x,z)->(x,z xor f(x)), a bijection. A reversible realization must retain or uncompute its auxiliary state. 5. The programs check all eight full-adder and Toffoli rows, and 261 complete canonical floor-circuit examples, including the maximum 15-bit seed. The universal circuit justification is the invariant argument, not extrapolation from those 261 examples. Dependencies: A02. Executable evidence: RUNTIME_BINARY. Source records: New derivation in this bundle. Limits • This supplies logical realizability and executable gate-level arithmetic, not a synthesized chip, hardware timing proof, gate-count optimum, or thermodynamic claim. • A typed software if/loop describes a finite Boolean network after unrolling; the supplied programs are not HDL synthesis files. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. B03 — Byte towers, retained length, and information costs Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. A byte string b has known length L, with bytes 0..255. Use an explicit endianness. 2. A finite encoding adds witness values to an otherwise many-to-one map. Statement. Length plus either base-256 integer lift recovers the exact byte string, including zeros. Any fixed witness alphabet making a map injective must contain at least as many values as its largest fiber. Exact remainder preservation is not automatic compression. Proof. 1. For little endian, Y=sum_(i=0)^(L-1) b_i256^i; for big endian, Y=sum b_i256^(L-1-i). Repeated Euclidean division by 256 gives the digits uniquely. Continue exactly L steps, retaining zero digits, and reverse order for the big-endian convention. 2. Without L, the zero strings of lengths one and two both encode as the integer zero. The integer alone therefore cannot identify arbitrary finite byte strings. 3. If f has a fiber of K distinct inputs mapping to one output, an augmented record (f(x),w(x)) can distinguish those inputs only if w takes at least K distinct values on that fiber. A fixed b-bit witness has at most 2^b values, so b>=ceil(log2 K). 4. For the canonical S=10^15, a generic residue in [0,S) fits in 50 bits. A naive 23-residue fixed-width record spends 1150 residue bits before headers, compared with 15 input bits on the canonical domain. More economical encodings may exploit the restricted valid set, but no general compression gain follows from reversibility. 5. The programs round-trip six byte strings in both endian conventions, including empty, zero, mixed zero/255, and all 256 byte values. Dependencies: A02, A03. Executable evidence: RUNTIME_BINARY. Source records: New derivation in this bundle. Limits • Finite-width data cannot injectively encode an unrestricted continuum of analog profiles. Finite models, quantization rules, or tolerance contracts are necessary. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. U01 — A composable geometric-to-computational reconstruction theorem Status: PROVED_UNDER_STATED_ASSUMPTIONS. Proof type: DEDUCTIVE_ARGUMENT. Assumptions 1. A geometry/field model X has an injective labeled measurement map M on the declared domain. 2. Measurements are represented by an injective exact serialization E with framing, length, type, and scale metadata. 3. Each byte/limb is encoded by a valid finite ordered-witness map W as in A02. Every required coordinate chart, coupling, and model assumption is retained. Statement. W composed with E composed with M is injective. Its inverse on the valid image is M^(-1) composed with E^(-1) composed with W^(-1). OMEGA geometry, exact measurement codes, serialization, and integer witness histories can therefore be composed without losing information that these stages are required to retain. Proof. 1. Suppose two composed outputs agree. Apply W^(-1), whose existence and uniqueness on valid records follows from A02. The serialized measurements agree. Apply E^(-1) to obtain identical labeled measurements. Finally injectivity of M gives identical model states. 2. Alternatively, composing the stage inverses in reverse order gives a left inverse directly, and any map with a left inverse is injective. 3. The executable end-to-end example uses the explicitly auxiliary seed s=1/2, six exact Q(phi) nodes, and affine field p(z)=3-2*z. It serializes all six exact values as rational coefficient pairs with explicit separators, encodes every ASCII octet through a 23-step ledger, reverses those ledgers, parses the recovered measurements, and recovers slope -2 and intercept 3 from the outer labeled pair. The packet is 24 bytes in the specified grammar. 4. For the canonical sine-defined geometry, G03 supplies an exact algebraic representation in a larger field, or one may use symbolic descriptions with certified approximations. An appropriate exact serialization must be supplied; the Q(phi) fixture is not a claim that the canonical sine belongs to Q(phi). Dependencies: C01, A02, B03. Executable evidence: U01_COMPOSITION_EXAMPLE, RUNTIME_END_TO_END. Source records: New derivation in this bundle. Limits • If analog quantization before E is noninjective and its lost information is not retained, this theorem starts after that loss. It cannot reconstruct the original unrestricted analog state. • This proves a specified compositional interface. It is not a universal theory of all geometry, a proof of physical unification, or evidence of superior neural-network performance. Formal-kernel status: NOT_FORMALIZED_IN_THIS_BUNDLE. Claims not established, or explicitly refuted EXT_017 A claimed rational irrationality-exponent result for pi can be transferred directly to lambda. Status: NOT_ESTABLISHED. The transformed approximation target for pi is generally algebraic irrational. A separate approximation theorem is needed; G04 and A01 do not need this transfer. EXT_087 The all-body Mahler inequality and equality classifications follow from the OMEGA triangle and rectangle examples. Status: DOES_NOT_FOLLOW. V01 proves only explicit body formulas and linear invariance, not inequalities for arbitrary convex bodies. EXT_098 Embedding a single planar OMEGA in a Hilbert space gives independent infinite-dimensional geometry or a universal finite-dimensional reduction. Status: DOES_NOT_FOLLOW. G05 preserves intrinsic dimension. Independently varying product assemblies require extra data and are not encoded by one finite ellipse. EXT_107_130 The fixed tensor decoder proves a new matrix multiplication exponent or an FFT on the nonuniform OMEGA nodes. Status: NOT_ESTABLISHED. T01 proves exact reconstruction and the actual sample count. Arithmetic complexity and field/bit complexity require separate algorithms and proofs. EXT_122_140_229 The finite polynomial code proves the release results on trace reconstruction, learning-memory lower bounds, or broadcasting. Status: DOES_NOT_FOLLOW. Different observation and error models must retain their own hypotheses. C01-C03 are self-contained polynomial-code theorems. EXT_325 A universal Crouzeix matrix-polynomial bound with constant two has been proved and executed here. Status: NOT_VERIFIED_IN_THIS_BUNDLE. O04 proves a constructive kappa bound, and I04 proves a conditional finite-compression transfer. The global finite-dimensional bound two is not supplied. EXT_333_SYMPLECTIC A nonlinear symplectic embedding/ball-packing theorem follows from the ellipse chart or a Fredholm derivative. Status: NOT_ESTABLISHED. S01 proves normalized linear symplecticity. Nonlinear local surjectivity, compactness, boundary behavior, and global continuation require separate arguments. EXT_365_372 One finite six-port measurement identifies an arbitrary host metric, connection, conductivity, or manifold. Status: FALSE_WITHOUT_ADDITIONAL_HYPOTHESES. I01 gives explicit finite-operator ambiguity. I03 is an infinite-data limit and conditional uniqueness application; M01 is a local placement theorem. EXT_376 The OMEGA floor transition implements the released universal fluid computer or proves its reachability result. Status: NOT_ESTABLISHED. F01 proves similarity covariance and an exact manufactured forced solution. It neither constructs the machine nor proves the external computational correspondence. APP_NEURAL_PERFORMANCE The proposed remainder-preserving architecture improves training, accuracy, generalization, compression, energy use, or intelligence. Status: NOT_ESTABLISHED. B01 proves a precise reversible quantized-layer theorem. Performance claims require an architecture, implementation, baselines, datasets, and reproducible experiments. APP_PHYSICS The mathematical interfaces prove holography, quantum gravity, or physical unification. Status: NOT_ESTABLISHED. No physical model or experimental evidence establishing those claims is provided. CORRECTION_ELLIPSE The unnormalized canonical ellipse chart is symplectic and all mapped feet lie inside its numerical range. Status: REFUTED_FOR_THE_DECLARED_CHART. O02 proves positive-length feet lie outside; S01 proves the canonical determinant exceeds one. The normalized chart is a different map. Named classical dependencies not reproved • Transcendence of pi • Cyclotomic-field degree and its maximal real subfield degree • Polynomial root bound • Basic Euclidean division and real-number completeness • Finite-dimensional spectral theorem for Hermitian matrices • Elementary spherical integration and spherical-harmonic product degrees Sources SOURCE_INTEGRATION_2026_10_07 Kind: USER_LIBRARY_SOURCE. Status: READ_AND_RETAINED_UNMODIFIED. Retained file: provenance/OMEGA_Release_Integration_Proofs.txt. SHA-256: 2e278e5a54fce069886774faa4280d49cdcc9e7bb7cd280ffaecd3cc996633cc. Earlier project derivation or audit; not independent peer review. SOURCE_OPERATOR_AUDIT_2026_10_07 Kind: USER_LIBRARY_SOURCE. Status: READ_AND_RETAINED_UNMODIFIED. Retained file: provenance/OMEGA_Theorem_Audit_2026-10-07.tex. SHA-256: 619c75d75f367c60ccfaa1d287df5110a507b7f85730151e06261793891cc96d. Earlier project derivation or audit; not independent peer review. SOURCE_HISTORICAL_VERIFIER Kind: USER_LIBRARY_SOURCE. Status: READ_AND_RETAINED_UNMODIFIED. Retained file: provenance/verify_omega_release_bridges.py. SHA-256: 70fd5bd3040ef4b308d644ebc90feac326bfb85cbc1945e14ef1e052aabc40cb. Earlier project derivation or audit; not independent peer review. OPENAI_REPOSITORY Kind: OFFICIAL_PUBLIC_SOURCE. Status: README_RETRIEVED. Source locator: https://github.com/openai/math. Repository verification caveats and source navigation only. No headline theorem is imported as proved. OPENAI_ANNOUNCEMENT Kind: OFFICIAL_PUBLIC_SOURCE. Status: RETRIEVED. Source locator: https://openai.com/index/sharing-ai-progress-in-mathematics/. Release context only. JSON3_DOCUMENTATION Kind: PRIMARY_SOFTWARE_DOCUMENTATION. Status: RETRIEVED. Source locator: https://quinnj.github.io/JSON3.jl/stable/. JSON3_PROJECT Kind: PRIMARY_SOFTWARE_SOURCE. Status: RETRIEVED. Source locator: https://raw.githubusercontent.com/quinnj/JSON3.jl/master/Project.toml. RUST_BIGRATIONAL Kind: PRIMARY_SOFTWARE_DOCUMENTATION. Status: RETRIEVED. Source locator: https://docs.rs/num-rational/latest/num_rational/type.BigRational.html. RUST_BIGINT Kind: PRIMARY_SOFTWARE_DOCUMENTATION. Status: RETRIEVED. Source locator: https://docs.rs/num-bigint/latest/num_bigint/struct.BigInt.html. RUST_JSON Kind: PRIMARY_SOFTWARE_DOCUMENTATION. Status: RETRIEVED. Source locator: https://docs.rs/serde_json/latest/serde_json/. Source boundary Library sources were read and retained. The live OMEGA homepage did not load during this turn. No current website audit or new validation of Zenodo deposits is claimed. The historical family locators in the source note are not proof imports.