Frozen generative grammar → energy-defined target → measurable exclusion gap → prospective prediction → machine-checked certificate · finite square spin ice as the test environment
The ice rule is the instrument. UNNS predictability is the subject. The study tests whether a frozen generative description can predict, in advance and quantitatively, where its own physical sufficiency ends — demonstrated here for one finite model; cross-domain transfer is the next test.
MANUSCRIPT v011 · FROZEN4×4 GAP · CERTIFIED (LEAN 4)1 kBT WINDOW · NOT PRESERVEDPREDICTION · PROSPECTIVE, BROAD INTERVALADDITIVE RECORDS · OUTSIDE LEANCROSS-DOMAIN TRANSFER · UNTESTEDcommits 4e759d38 · 7610fe5d
01
What the investigation tests
The central proposition: a generative structural description can identify an admissible region of a large nominal state space and predict a measurable boundary between that region and the physically relevant configurations. Four connected questions, and three levels of achievement kept strictly apart.
The exclusion-gap equivalence is an exact criterion for physical sufficiency; it is not by itself an algorithm for predicting an unknown gap. The predictive achievement lies in the UNNS-motivated procedure: grammar frozen, quantitative prediction registered from smaller systems before the larger instance was evaluated, then independently tested and formally certified for the specified finite model.
02
Generative contraction
The two-in/two-out grammar is constructed blind to energy and frozen. It removes almost the whole nominal space — a property of the constraint, not a discovery.
NOMINAL VS ADMISSIBLE CONFIGURATIONS
Log scale. Free-boundary square spin ice, n = 2L(L+1) spins.
4×4: THE ADDITIVE EXACT COUNT
193,662 of 240 configurations satisfy the ice rule — computed from the frozen vertex table only (verified three independent ways).
A count, not a constructive run: no 4×4 generator was executed and the count is not Lean-checked. Recorded in SCR_MS_GRAMMAR_COUNT_4X4_v001.
03
The exclusion gap
For a finite model whose grammar excludes at least one configuration: S_T(W) ⊆ S_G ⇔ W < Δ¬G, where Δ¬G is the energy of the cheapest grammar-excluded configuration above the global ground state. Sufficiency for every window is decided by one number.
NORMALIZED GAP δL = Δ¬G / kBT
All four sizes lie below 1: exact preservation of the 1 kBT window fails at every size studied. Band: the interval frozen for the 4×4 value.
3×3 PRESERVATION AT W = 1 kBT
Preregistered test. The target holds 26 states; the grammar contains 10 and excludes 16 — exactly predicted by the first excluded level at 0.943 kBT.
Window chosen with the 1×1 and 2×2 gaps known; blindness was to the 3×3 low-energy outcome only.
WINDOW EXPLORER · 4×4 MODEL
Drag the window W. Bars: energy above the certified ground witness of each of the 40 single-island reversals (sorted). Every one leaves the grammar. The first lies exactly at the certified gap Δ¬G = 0.9459 kBT.
These 40 values are single reversals of one certified ground witness: an exact calculation, not an optimization over all bulk defects and not the full spectrum. Lowest tier: 8 islands touching a single corner vertex (spread 8562/270 A ≈ 7×10−16 of the gap). Evidence: SCR_MS_SUPPLEMENT_v001, outside the Lean certificate.
04
Prediction, certification and the exact correction
A gap prediction was frozen from the 1×1–3×3 evidence, evaluated numerically, then fixed exactly by a Lean 4 proof that does not trust the numerical optimizer.
CHRONOLOGY OF THE 4×4 PREDICTION
CERTIFIED EXACT VALUES (UNITS 2−70 A)
Certificates fix minimum values, not minimizer sets; the corner defect is a verified witness and uniqueness is not claimed. Statements concern the encoded dyadic model.
THE 928 CORRECTION
The certificate generator's own assertion failed on the frozen excluded-state value; a diagnostic found the true minimum. The frozen value lies 928/270 A above it — a relative 7.7×10−17 of the gap. No verdict changed.
LEAN 4 PROOF ARCHITECTURE
LEAN Principal theorems (names at commit 4e759d38)
Axioms limited to propext, Classical.choice, Quot.sound; no sorry; no native_decide. An independent re-run of the batches in the author's environment was waived (disclosed).
05
Four axes, reported separately
G constructive contraction · P physical preservation (false negatives = 0) · T independent transfer · C charged computational consequence. A favourable contraction cannot compensate for a failed sufficiency test, and the reverse.
06
Sensitivity of the gap to the Hamiltonian
Proposition (proved in the text, not in Lean): |Δ′ − Δ| ≤ 2ε, ε = max|H′ − H|. Applied to the frozen couplings it is mostly uninformative — and the manuscript says so.
WORST-CASE 2ε / Δ (BOUND INFORMATIVE ONLY BELOW 1)
Dimension scaled by (1+p). Rows ≥ 1 cannot exclude a gap change as large as the gap itself.
INPUTS AND PERSISTENCE
Width or height scaled by (1+p) is an exact rescaling by (1+p)², so the scale-separated residual is 0. No perturbed model was solved.
07
Provenance and evidence layers
Two archival layers, kept apart. The research freeze is anchored to commit 4e759d38; the additive manuscript records live in a separate commit and change nothing frozen.
SHA-256 OF THE ADDITIVE RECORDS (MATCH THE FILES AT COMMIT 7610fe5d)
Reproduce from inside each package directory (frozen inputs are read-only; outputs reproduce byte for byte): python3 grammar_count_4x4_v001.py ../.. python3 supplement_analysis_v001.py ../..
REGISTER Disclosure register — 14 items
08
The next scientific test: cross-domain predictive transfer
Domain independence is the ambition of the UNNS methodology, not something a single spin-ice case establishes. A proposal — no result — of what a transfer test would need:
A prediction fulfilled in an unrelated domain would be the first evidence the relation is not specific to spin ice; a failure would locate the limit of the methodology and be recorded as the unfavourable result here was.
The program’s foundational-scope archive: 42 files — 26 PDF manuscripts, 15 interactive HTML analytics and one proposed-manuscript note. The foundation document frames the program's universal admissibility inequality, stratified occupation and operator-selective activation (structural regime theory; falsification-first, preregistered). SCR asks a different, complementary question: whether a generative admissibility description can predict a physical boundary in advance.
Grouping is by title only, for navigation; it is not a claim about each document's findings.
unns.tech · UNNS Substrate Research Program · 2026 Every figure on this page is taken from manuscript v011 or from the two verified record files; nothing is estimated.