This package exercises bounded observer-like patches with twelve local port loads, seam repair, readback and finite records. It distinguishes a readout of the supplied, fixed chart geometry from load and local-drive diagnostics. The latter are not identified as physical volume or curvature.
From the repository root:
python3 code/native_geometric_source/build.py --write
python3 code/native_geometric_source/verify.py --write
python3 -W error -m pytest -q code/native_geometric_source
cd Lean
lake env lean Geometry/NativeGeometricSourceIdentification.leanThe producer uses the frozen native source in
evidence/observer_dynamics_20260925/oph-physics-sim/ and propagates 79
polynomial features. The independent verifier enumerates the fixed-occupancy
configurations using bit masks and lazy transpositions,
checks all separated-position and coarse-block covariance entries, and replays
the retained load traces. A separate process checks their native geometry,
preparation seeds and seam schedules. No external data or sibling checkout is
needed. NumPy and the existing native archive's SciPy dependency are required.
The tests read original seam incidence for a separate twelve-port linear transition oracle and a full two-occupant transition kernel for nonlinear mismatch. They compare complete covariance matrices through lag eighteen, both record strides, complementary fillings and density projections. Independent pairwise-difference centering checks retain large original integer values and offsets before any producer conversion.
Inputs and small outputs are under
evidence/native_geometric_source_20260925/. spec.json declares both source
preparations, clocks, readouts, native source hashes and finite refinement
comparison. receipt.json is generated by build.py;
verification_receipt.json is generated by verify.py. These are finite
controls, not a large-run replay, statistical continuum limit, or physical
metric identification. The geometry-only zero-covariance statement is proved
for all finite schedules in the Lean module; the twelve-port rational
covariances are independently enumerated, while the Lean separated-position
witness uses the four-cycle.
The finite stationary calculation uses the actual internal thirty-seam graph of
one native twelve-port carrier, equivalently one component of the declared
isolated federation control. Its covariances are not the full port_pair
federation covariances. The four small geometry traces do use port_pair
routing. Filling, stationary centering and trace-normalizing gains are
declared inputs; coarse blocks are within one carrier.
Exact finite reduction. Let n be a binary twelve-port configuration with
exactly r occupied ports, uniformly distributed over C(12,r) configurations.
For each subset S of size at most two, use the feature
h_S(n) = product(n_i for i in S), including h_empty = 1. There are
1 + 12 + 66 = 79 features. A fair endpoint coin on a binary seam gives an
unchanged configuration or its endpoint transposition, each with probability
one half. Equal endpoint loads give the same result in both cases. Thus one
uniform seam attempt acts on features by
[ K=\frac{30I+\sum_{e\in E}R_e}{60},\qquad (R_e h)S=h{e(S)}. ]
Swaps preserve the degree and occupancy, so this family is closed at every finite lag. Each swap is a bijection of the fixed-occupancy configurations; their uniform law is stationary. The exact original-law moments are
[ m_S=\mathbb E[h_S]=\frac{\binom{12-|S|}{r-|S|}}{\binom{12}{r}},\qquad H_{ST}=\mathbb E[h_Sh_T]=m_{S\cup T}, ]
where an impossible binomial choice is zero. Products use set union because
n_i^2 = n_i; moments through degree four suffice. The features form a
spanning family, not an independent basis on a fixed-occupancy slice:
sum(n_i) = r, and all pair features vanish when r = 1. No moment-matrix
inverse or independence assumption is needed.
Write a readout as f(n) = h(n)^T A/d. The integer numerator readouts are
x_i = 12*n_i-r, drive = x @ L, and
mismatch_i = sum(n_i+n_j-2*n_i*n_j for j adjacent to i);
their denominators are 12, 12, and 1. With D = 60*K, the full
stationary lag covariance is the closed finite identity
[ C_t=\frac{A^{\mathsf T}(H-mm^{\mathsf T})D^t A}{d^2 60^t}. ]
This retains every configuration's contribution without enumerating states
in the producer. Record averages sum these full covariance matrices with
their exact multiplicities; a record stride of two uses C_(2*t).
Numerical contract. The nontrivial density projection has integer
occupancy 1 <= r <= 11, positive integer record counts and the supplied
thirty-seam graph. Load, drive and mismatch are dimensionless; one tick is
one seam attempt. All stationary means, centered covariances, density
projections and coarse-block products are exact rational values, with no
roundoff tolerance. Integer coefficients, propagated numerators and products
must use Python integers before multiplication or summation. Converting an
already overflowed NumPy integer to Fraction cannot recover its value.
Off-diagonal covariances may be negative; they must not be clipped. The
separate chart-volume replay uses floating arithmetic and its explicit
geometric tolerances.
Repair and artifact impact. Five records at stride two require lag eight,
beyond the supplied [1,2,4] record counts. At half filling, the local-drive
lag-eight diagonal is exactly 90750535351/26730000000. Fixed-width
propagation and contraction previously returned
63700095795517/682015950000000. At occupancy three, the five-record
stride-two drive covariance also acquired a negative all-ones quadratic
form, although the drive sums to zero in every original configuration.
These are errors in valid finite covariance calculations.
At reviewed main 7521d5c3, the first twelve controls in
test_exact_moments.py produced nine failures and three passes; they were
retained before the repair in b38cf9d6. The original short-window checks
and the complement identity passed despite the longer-window corruption.
The repaired controls include all occupancies 1..11 through lag 18,
original-input linear and nonlinear oracles, large shifted integer data,
and a detached verifier with the producer absent. Isolated mutations of
centering, moments, lazy weight, clock/covariance validation, input handling
and fixed-width propagation are rejected; these controls are not a claim
of mutation completeness.
The follow-up audit of a04620a7 found that an outer list or tuple could
hide a masked NumPy row: array conversion discarded its mask before the
integer check. For rows 1 and a masked 999, this admitted covariance
249001 from an unobserved sample. The retained original-container tests
first produced 13 failures and seven passes. Missingness is now checked
inside the original containers before conversion; complete signed,
unsigned and arbitrarily large integer rows remain accepted exactly.
The mathematical follow-up checks the feature-transition identity against
both original endpoint-coin operations on all 4,096 binary configurations.
Direct original-state checks reproduce projection residuals and coarse
covariances for every nontrivial occupancy. The retained native path-sum
controls also verify record averages at both clock strides without using
the covariance-lag multiplicity formula.
The existing [1,2,4] controls end at lag six. All rational matrices, native
states and events, source geometry and the source-identification decision
remain unchanged. Canonical regeneration on Windows and Linux agrees, but
changes forty floating reference-volume entries relative to the previous
receipt, by at most two ULPs (1/72057594037927936, about 1.39e-17). These
last-bit chart-volume differences remain within the geometric replay
tolerance. The live producer and verification receipts bind the changed
code and regenerated data; producer, verifier and receipt hashes change. The
frozen native archive and its manifest remain inputs. The claim registry
and observation ledger reference these live artifacts by path; the numerical
correction changes no physical claim or observation status. The paper's
finite covariance identities and the Lean fixed-geometry theorem have the
same scope.