The quadratic-reciprocity campaign#
Quadratic reciprocity is the next flagship theorem for the native arithmetic library. It is not being imported from Lean, assumed as an axiom, or encoded as a trusted Legendre-symbol function. The endpoint, all intermediate finite constructions, and the final certificate remain ordinary first-order PA.
Current immutable Alpha v16 status (2026-08-25)
All 316 Alpha-only QR specifications are now alpha_closed with genuine
checked-use authority: one earlier QR/HA overlap was already closed, and
immutable Alpha v16 promotes exactly 314 formerly body-only ancestors plus
the formerly pending final root after checking their actual complete proofs.
The full QR graph has 241 Stable prerequisites and 316 Alpha-closed
theorems; none of those 316 has been promoted to Stable. Older phrases such as
“body-green,” “unregistered,” “unadmitted,” or “private” below describe
historical checkpoints or the still-unchanged Stable/public boundary, not the
current Alpha evidence ledger. See
Alpha and Stable library editions.
The exact native theorem#
Balanced congruence lets us express “\(a\) is a square modulo \(p\)” without subtraction:
For distinct odd primes \(p,q\), write \(Q_{pq}=\operatorname{QRes}(p,q)\) and \(Q_{qp}=\operatorname{QRes}(q,p)\). The exact constructive capstone surface is:
The checked surface prototype expands the combined statement completely. It
uses 1,520 source characters—well below the 8,192-character input limit—and
contains no primitive occurrence of Prime, Odd, QRes, %, an integer
sign, or exponentiation.
The same, opposite, and combined statements now have actual empty-context proofs independently accepted by the unchanged original kernel. The combined ordinary certificate contains 54,870 structural proof nodes, 35,052 proof objects, and depth 129; a complete 557-node self-contained proof bundle is also independently accepted by the separately verified Lean companion. Immutable Alpha v16 grants these QR results checked use without making them Stable. The former recursively expanded closure remains a measured historical baseline. Throughout historical portions of this chapter, “body-green” names the intermediate evidence level that preceded the final evidence promotion.
Open permanent tag
PA00FW for quadratic_reciprocity_combined.
From there, every numbered tactic line and linked dependency opens its own
stable theorem page; the candidate/public status remains visible throughout.
The parallel
definition-aware
PA00FW page renders the same formula with linked conservative names and an
exact native replay line. Both explorer editions separately display current
alpha_closed evidence and historical candidate-source provenance;
readability itself does not constitute admission.
Constructive meaning
Peano Lab is intuitionistic by default. The final same/opposite disjunctions therefore depend on an explicit bounded decision theorem for quadratic residues. A bare use of double-negation elimination would not be an acceptable substitute.
The mathematical route#
The selected proof is the Gauss–Eisenstein lattice-count proof. For \(m=(p-1)/2\) and \(n=(q-1)/2\), its combinatorial center is
The two sums count the lattice points on opposite sides of the line \(qi=pj\) in an \(m\times n\) rectangle. Equality cannot occur for distinct primes. Taking parity and applying Gauss’s lemma gives the reciprocity sign.
This route matches the native language well: floors become quotient/remainder witnesses, finite sums and counts become β-coded traces, and signs become even/odd bits. A Gauss-sum proof would require finite fields, characters and roots of unity, none of which are needed here.
The route is also cross-checked against existing formal developments. The Isabelle/HOL quadratic-reciprocity theory builds on its checked Gauss theory and records Gauss’s fifth proof as its mathematical source. An earlier Mathlib Gauss–Eisenstein development exposes Euler’s criterion, Gauss’s lemma and Eisenstein’s lemma as separate interfaces. These are design references only: no certificate or theorem from either system is trusted by Peano Lab.
Checked entrance layer#
The first QR-0 tranche supplies fully expanded theorems for:
constructive even-or-odd decomposition and exclusivity;
successor, addition and multiplication parity;
existence and uniqueness of the half of an odd number;
the exhaustive \(1\) or \(3\pmod4\) classification of odd naturals;
incompatibility of the two modulo-\(4\) cases;
oddness of every prime other than \(2\);
constructive congruence decision at nonzero modulus;
bounded root search and a constructive decision of quadratic-residue status.
The QR-0 examples are complete rather than illustrative: checked canonical equivalences classify the square residues as \(\{0,1\}\) modulo \(3\), \(\{0,1,4\}\) modulo \(5\), and \(\{0,1,2,4\}\) modulo \(7\). Nine positive entries carry explicit balanced-congruence witnesses, and six complementary entries are constructively proved nonresidues by bounded-root enumeration. The largest of these 24 certificates has 6,761 structural occurrences, 4,333 distinct objects, and depth 95.
Open the theorem atlas at
parity_cases,
odd_mod4_cases, or
mod_eq_decidable_nonzero
to inspect the exact expanded statement, every dependency, the complete tactic
recipe, and certificate metrics.
Body-green parity transport#
Four isolated tranches now package parity in the exact shapes consumed by the Gauss–Eisenstein endpoint:
Tranche |
Readable endpoint |
Body nodes/depth |
|---|---|---|
sum classification |
an even sum has equal summand parity; an odd sum has opposite parity, in both directions |
|
modulo two |
even is congruence to zero, odd is congruence to one, and congruence preserves both |
|
odd multiplication/division |
for odd |
|
odd half versus modulo four |
from |
|
All four focused modules pass together at 16/16 in 1.24 seconds under the
60-second cap. Their predicates are fully expanded existential equations in
native PA; the candidates are dependency-curried, unregistered, and
unadmitted. The linked Obsidian concept
parity transport records the
exact client ladder and source links.
Checked prime-unit bridge#
The prime-field entrance is no longer merely planned. Eight checked certificates now prove:
a prime is constructively coprime to a natural or divides it;
nondivisibility by a prime implies coprimality;
distinct primes are coprime;
balanced Bézout coefficients produce a subtraction-free modular inverse;
a nonzero modulus converts that balanced inverse into an ordinary natural inverse witness; and
multiplication by a coprime value cancels in balanced congruence.
At the readable level, the inverse endpoint is
The exact expanded cards are
distinct_primes_coprime,
coprime_mod_inverse, and
prime_mod_cancel.
They use the existing relational gcd, balanced Bézout, and congruence API; no
field or inverse function was added to the PA language.
Finite objects without new language primitives#
The next layer uses relational folds rather than adding functions:
Expository relation |
Native representation |
|---|---|
|
a β-coded constant factor prefix plus its checked |
|
a second β-code whose successive values satisfy \(s_{i+1}=s_i+a_i\) |
|
a |
|
decoded entry \(i\) is \(s+i\) for every \(i<l\) |
These names are documentation abbreviations. The language-and-trust contract requires complete expansion before parsing and kernel checking.
This checkpoint checks beta_range_exists,
beta_range_transport_entry, beta_sum_exists_unique, and
beta_sum_succ_decompose. It also closes the bit-count and congruence gates:
bit_count_exists, bit_count_functional, bit_count_bounded,
beta_product_pointwise_mod_congruent, and
beta_sum_pointwise_mod_congruent are independently kernel checked. Thus a
later Gauss argument may count a coded \(0/1\) indicator prefix, while Wilson
and Fermat may replace pointwise-congruent factor prefixes without adding a
finite-set primitive. Their atlas cards expose the complete native scripts
and certificate metrics.
The outer-sum algebra needed by the Eisenstein route is now explicit too.
beta_sum_pointwise_add combines three exact equal-length Sum traces: if
the third decoded entry is the sum of the first two at every bounded index,
then their endpoints satisfy n+m=q. Its constructive 127-command body is
195/57 nodes/depth, with no object reuse. Constant right-hand sides are
handled by beta_repeat_sum_exact and beta_repeat_sum_exists_exact, which
evaluate and construct the exact sum l*a of a length-\(l\) Repeat(a) prefix
at 85/32 and 33/21. The focused audits pass 3/3 and 4/4; all remain
unregistered and unadmitted.
pointwise-add source
· pointwise-add test
· constant-sum source
· constant-sum test
The isolated finite-fold laboratory now has an exact complement identity as
well. complementary_bit_counts_add_length takes two length-\(l\) native
BitCount prefixes whose decoded entries are pointwise exactly \((0,1)\) or
\((1,0)\) and concludes
It depends only on bit_count_zero, bit_count_succ_decompose, le_succ,
le_refl, and add_succ_left. Its 112-command dependency-curried body has
220 nodes at depth 46, 211 objects, 219 edges, and 9 reused objects;
the focused no-DNE audit passes 3/3 in 1.47 seconds. See the
source
and test.
The theorem is unregistered and unadmitted. It is a one-dimensional
same-index count identity, not a theorem exchanging the two folds of a nested
rectangle.
Checked QR-2 bridges#
The first residue-system bridges are also native now. Factorial(n,z) is an
authoring abbreviation for the checked product of a β-coded range
\(1,2,\ldots,n\); the library proves its existence, functionality, zero value,
and successor decomposition. Separately, the power layer proves the first
power law, a predecessor/successor multiplication bridge, and
for relational powers. In the exact theorem this display contains neither a
power function nor a congruence predicate: both sides expand to β-coded
products and balanced natural equations. The largest new power-congruence
certificate has 10,671 structural occurrences, 1,748 distinct objects, and
depth 68. factorial_exists has 59,841 occurrences but only 4,907 objects,
comfortably inside the dual resource policy.
The power algebra now also includes checked square, exponent-addition and exponent-multiplication laws. In readable notation the largest says
but its public contract is a 7,127-character composition of three expanded
relational Pow graphs. Its certificate has 70,463 structural occurrences,
only 5,786 distinct objects, and depth 91. This is direct evidence that the
larger occurrence budget is admitting shared mathematics rather than an
unbounded object graph.
The first Gauss-sign bridge is checked as well. If \(p=S r\), then balanced
congruence proves \(r^2\equiv1\pmod p\) with uniform natural witnesses. One
conjunction induction then proves that every relational power of \(r\) is
congruent to \(1\) for an even exponent and to \(r\) for an odd exponent. This is
the subtraction-free native replacement for \((-1)^k\). The capstone
pow_predecessor_parity_mod uses 9,249 occurrences, 1,758 objects, and depth
67, with no classical step.
The positive half-system has a checked native foundation too. For
\(p=2h+1\), entries of the β-coded range \(1,\ldots,h\) are nonzero and strictly
below \(p\); equality of decoded values forces equality of indices; and balanced
congruence modulo \(p\) forces equality both at the value and index levels.
beta_half_range_mod_injective is the strongest current endpoint at 4,001
occurrences, 1,052 objects, and depth 63. The remaining Gauss step must still
construct signed representatives of multiplied half-range entries.
Finite permutation completeness is now checked constructively. The library first recodes a β prefix while replacing one entry, then swaps an arbitrary interior entry with the final entry and proves forward and reverse pointwise transport. Those contracts preserve boundedness, injectivity and surjectivity. Ordinary induction then proves
with both finite sets represented only by expanded bounds and BetaAt
relations. The exact endpoint finite_bounded_injective_surjective has 42,463
structural occurrences, 6,399 distinct objects and depth 89. It cold-replays
deterministically, checks from the empty context, and contains no DNE.
The first product-transport layer is checked too. For one β-coded replacement,
beta_product_replace_balance proves the cancellation-free balance law
where the old length-\(k\) product is \(p\), the new product is \(q\), and the
factor at the selected position changes from \(x\) to \(y\). Specializing this to
an interior/final transposition gives
beta_product_swap_last_invariant: exchanging those two decoded factors
preserves the exact product, \(p=q\). The proof uses ordinary induction,
successor-product decomposition, pointwise prefix transport, product
functionality, and semiring associativity/commutativity. Its exact certificate
has 7,439 structural occurrences, 1,685 distinct objects and depth 67; both
cold replays pass with no DNE.
This is deliberately not yet labeled invariance under an arbitrary finite
permutation. The next checked gate must induct from bounded injective
reindexings to a sequence of last-position reductions, using the swap theorem
at each successor step. The detailed
fixed-last and simultaneous-swap design
records the exact conservative statement, sublemmas, and admission gates.
The active proof laboratory#
The campaign uses three deliberately different labels. Checked means that the exact expanded target has a closed certificate accepted by the independent kernel from the empty context. Isolated candidate means that source and an adversarial audit exist, but the theorem is absent from the public registry. Planned means that only its contract and dependency route are fixed. A Slurm job, a source hash, or a plausible tactic script never upgrades one status into another.
The immediate route to Fermat is now explicit:
order |
native theorem |
present status |
purpose |
|---|---|---|---|
prerequisite |
|
isolated candidate |
remove the final factor under a fixed-last reindexing |
prerequisite |
|
isolated candidate |
exact products are invariant under a bounded injective reindexing |
1 |
|
isolated candidate |
identify range entry \(i\) with \(S i\) |
2 |
|
isolated candidate |
fold pointwise coprimality through an exact product |
3 |
|
isolated candidate |
make the nonzero-residue product cancellable modulo a prime |
4 |
|
isolated candidate |
recode every decoded map value by successor |
5 |
|
isolated candidate |
construct canonical nonzero multiplication remainders |
6 |
|
isolated candidate |
package the residue permutation and both alignments |
7 |
|
isolated candidate |
extract the common scale from a finite product modulo \(p\) |
8 |
|
isolated candidate |
prove \(a^{p-1}F\equiv F\pmod p\) before cancellation |
endpoint A |
|
isolated candidate |
cancel the coprime residue product and obtain \(a^{p-1}\equiv1\pmod p\) |
endpoint B |
|
isolated candidate |
constructively cover coprime and divisible inputs and obtain \(a^p\equiv a\pmod p\) |
The full contracts, hygienic expansions, Wilson branch, and the later
Euler–Gauss–Eisenstein spine are recorded in the
Fermat/Wilson tranche.
The cheap finite-product plus Fermat preflight now succeeds for all 21
candidate bodies. It caught a missing second rewrite in
beta_successor_range_reindex_aligned and an invalid locally repackaged
hprojection in prime_mul_residue_product_balance; both are fixed.
candidate |
body nodes/depth |
|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
Nine bounded structural gates pass across the reindex, balance, and endpoint
suites. Original zero-CPU jobs 172769, 172770, and 172837 were cancelled
stale. Corrected snapshot
73d2863a0138c8dce1f8a7f2793bcd96f543e389c0c4af6cce75cc13005ac3d9
backs jobs 172988 (fermat-reindex, 16 GiB/2 hours), 172989
(fermat-balance, 16 GiB/2 hours), and 172990 (fermat-endpoints,
32 GiB/4 hours); all were pending at submission.
These numbers come from
peano_lab.library.candidate_validation.replay_candidate_bodies. The reusable
helper kernel-checks dependency-curried scripts without replaying or closing
their dependencies and returns structural/identity metrics; its three unit
tests pass. It is a defect-finding preflight, never an admission receipt. WMI
replay and a later receipt-pinned admission are still required.
Why the first proof is shown before admission
The following is the exact authored tactic recipe currently under audit, not a theorem claim. It is useful as a readable proof object and as an LLM training example; the WMI discovery replay may still expose a parser, witness, or dependency mismatch that requires changing it.
Candidate proof: a decoded entry of 1,...,l is S i
intro b
intro c
intro l
intro i
intro x
intro hrange
intro hi
intro hx
have hraw : x = 1 + i
specialize beta_range_entry_eq b
specialize beta_range_entry_eq c
specialize beta_range_entry_eq 1
specialize beta_range_entry_eq l
specialize beta_range_entry_eq i
specialize beta_range_entry_eq x
apply beta_range_entry_eq
exact hrange
exact hi
exact hx
have hone : 1 + i = S i
trans S (0 + i)
specialize add_succ_left 0
specialize add_succ_left i
exact add_succ_left
congr
specialize zero_add i
exact zero_add
trans 1 + i
exact hraw
exact hone
The candidate scripts and every expanded formula are split across the
range/product,
residue-map,
residue-reindex,
scale-product,
product-balance,
and endpoints
modules. They remain deliberately unimported.
The predecessor endpoint depends directly on exact factorial existence, rung 8, coprimality of the prime residue product, prime nonzeroness, and checked coprime modular cancellation, plus multiplication normalization. The all-input wrapper then uses prime nonzeroness, successor-power decomposition, the constructive prime coprime-or-divides alternative, congruence scaling, and explicit divisibility transport. Neither source candidate is a checked Fermat theorem yet.
The first Wilson-specific arithmetic gate is now also an isolated
candidate. prime_bounded_square_one_cases states constructively that, for
p = S n prime and 0 < x < p, a balanced witness for
\(x^2\equiv1\pmod p\) implies x = 1 \/ x = n. It introduces no subtraction:
write x = S t, normalize
[ x,x = 1+t(t+2), ]
use the congruence witnesses and additive cancellation to extract
\(p\mid t(t+2)\), then apply native Euclid. In the first branch, \(p\mid t\) and
\(t<p\) force \(t=0\). In the second, \(p\mid(t+2)\) and the two bounds force
\(p=t+2\), hence x = n. This is the PA replacement for factoring
\((x-1)(x+1)\), and it uses neither classical case analysis nor an integer type.
The candidate no longer invokes the UI-only ring tactic. The normalization
above is now an explicit native equality/rewrite proof, and its exact ordered
direct-dependency tuple has 16 entries:
ne_zero_of_one_le, nonzero_is_succ, mul_succ_left, add_assoc, add_comm,
add_left_cancel, factor_difference, euclid_prime_dvd_product,
le_succ_self, lt_of_le_of_lt, zero_or_succ, divisor_le_nonzero,
lt_not_le, succ_ne_zero, le_antisymm, succ_injective
The source is the unimported
Wilson square-one candidate.
Its five-gate wilson-square-one WMI suite was submitted as discovery job
172855 from snapshot
396af02c5aa4fdf62d4c3484f8a2c711b03c489cad498c121d0402ce3ee79981
on cpu_idle with 1 CPU, 16384 MiB, and 02:00:00; that stale job was later
cancelled after consuming zero CPU. A body-only laptop replay of the corrected
candidate measured 182 nodes/depth 48, and its three bounded structural gates
passed. Replacement job 172966, from exact snapshot
9a59e7a590223d4852f02dde19633b21bfcc4fb92491705d4aade022a116265a,
is PENDING (Priority) with zero CPU. The body receipt and structural checks
are not closed-certificate admission: there is no WMI pass or new theorem.
The inverse map is zero-based#
The next seven Wilson candidates remain isolated source artifacts under queued
WMI discovery. For p = S n, index i<n represents residue S i, while a
decoded value j<n represents its inverse residue S j. Their exact
documentation surface is
[ \operatorname{InvIdx}(p,n,i,j);\Longleftrightarrow; i<n\land j<n\land \exists u,v.;(S i)(S j)+pu=1+pv, ]
where each strict inequality expands to a gap witness, for example \(i<n\Longleftrightarrow\exists g.\;g+S i=n\). The β-prefix is
[ \operatorname{InvPrefix}(p,n,b,c,\ell);\Longleftrightarrow; \forall i<\ell.;\exists j.; \operatorname{At}(b,c,i,j)\land\operatorname{InvIdx}(p,n,i,j), ]
and At itself expands to
[ (\exists h.;h+S j=S((S i)c))\land (\exists q.;b=q,S((S i)c)+j). ]
Nothing here is a new kernel symbol: InvIdx, InvPrefix, <, and At are
all expanded before the native PA parser sees the statement.
layer |
isolated candidate |
exact direct dependencies |
|---|---|---|
point |
|
|
point |
|
|
point |
|
|
point |
|
|
prefix |
|
|
prefix |
|
|
prefix |
|
|
The pointwise candidates establish mate existence, raw bounded uniqueness,
index uniqueness, and symmetry. Prefix extension appends the new mate with
beta_prefix_extend and splits i<S l into the new position or an old one;
induction then constructs every l≤n, including the full n-entry map.
See the unimported
pointwise source
and
prefix source.
Their five-gate wilson-inverse-prefix suite closes the seven-candidate stack
recursively. Discovery job 172899, snapshot
1a11442b18dd6c40b49975e16f0b2062be57fade347acca20d87dba27e6adffc,
was cancelled after zero CPU when cheap body replay caught two existential-
binder errors. Both are fixed in exact snapshot
6d32a5ba65b2268dc3fd6c027726a86c5054788bbeb5edacd6d6cbec3373403e;
replacement job 172975 is pending at submission. There is no replay result,
pinned metric set, pass, or admission. A second isolated layer now composes
β-value functionality, inverse-index uniqueness, and symmetry; its own WMI
discovery remains pending.
From inverse data to an involution#
Six isolated candidates expose the full extensional API:
candidate |
mathematical role |
exact direct dependencies |
|---|---|---|
|
every decoded covered entry satisfies |
|
|
every valid mate is the decoded entry |
|
|
decoding the mate again returns the source |
|
|
equal decoded mates have equal source indices |
|
|
every bounded value is decoded somewhere |
|
|
a fixed index is an endpoint |
|
The generalization boundary is intentional. The first five statements do not
assume primality. Entry soundness is valid for arbitrary parameters; the next
four use only p = S n, which makes bounded modular representatives unique.
Only the sixth theorem assumes Prime(p), and its exact zero-based conclusion
is
[ i=0;\lor;S i=n. ]
The proof first recovers InvIdx from β uniqueness, obtains extensionality
from bounded inverse-index uniqueness, and combines symmetry with
extensionality to decode back from j to i. Injectivity and surjectivity are
then constructive consequences of that involution. A fixed entry gives
\((S i)^2\equiv1\pmod p\), so the isolated square-one classifier yields the two
displayed cases.
The unimported source is
wilson_inverse_involution_candidate.py.
Its five-gate wilson-inverse-involution suite recursively closes 14 specs.
Discovery job 172920, snapshot
cfa4eea18d4a746a49a2d7579f217dbd65a27a79df61c76e8dba49079ba1aaa4,
was cancelled after consuming zero CPU. First replacement job 172967, from
snapshot 9a59e7a590223d4852f02dde19633b21bfcc4fb92491705d4aade022a116265a,
was also cancelled after zero CPU when the prefix source changed. Corrected
job 172976, from snapshot
6d32a5ba65b2268dc3fd6c027726a86c5054788bbeb5edacd6d6cbec3373403e,
is pending at submission. No report, pinned metrics, pass, or admission is
claimed.
The fixed entries are now explicit candidates#
The next isolated layer turns the fixed-point classification into actual decoded endpoint entries:
candidate |
exact role |
exact direct dependencies |
|---|---|---|
|
from |
|
|
under the same shape, decode |
|
|
package |
|
The contract deliberately does not say that 0 and k are distinct. For
prime 2, k=0 and the two entry facts coincide; for prime 3, k=1 and
they are distinct. The source remains unimported:
wilson_inverse_endpoints_candidate.py.
Its focused five-gate wilson-inverse-endpoints suite recursively closes all
17 Wilson square-one, point, prefix, involution, and endpoint specs. Discovery
job 172927, exact snapshot
7083e3876cc54daa782153aa6e1a2554aa75fa5a40cce3d6cf6b5971979dc35d,
was cancelled after consuming zero CPU. First replacement job 172968, exact
snapshot 9a59e7a590223d4852f02dde19633b21bfcc4fb92491705d4aade022a116265a,
was also cancelled after zero CPU when the prefix source changed. Corrected
job 172977, snapshot
6d32a5ba65b2268dc3fd6c027726a86c5054788bbeb5edacd6d6cbec3373403e,
is pending at submission.
Only syntax and the first three bounded cheap gates were run locally, and they
passed. The two cold recursive replays, proof/RSS profiling, no-DNE/capacity
checks, and adversarial mutations remain WMI-only. This is discovery only:
there is no report, pass, pinned metric receipt, or theorem admission.
Nonendpoint inverse orbits are now explicit candidates#
The next isolated layer begins the pairing argument without pretending that the fixed endpoints are distinct:
candidate |
exact role |
exact direct dependencies |
|---|---|---|
|
from |
|
|
prove |
the preceding nonfixed theorem, |
The second proof decodes back by involution. If the mate were either endpoint,
β uniqueness against that endpoint’s fixed entry would force i=j,
contradicting the first theorem. The argument is constructive. At prime 2
the two endpoint descriptions still coincide and no nonendpoint bounded index
is asserted to exist, so the theorem is scoped without a hidden p>=3
assumption.
The unimported source is
wilson_inverse_orbit_candidate.py.
Its focused five-gate wilson-inverse-orbit suite recursively closes all 19
square-one, point, prefix, involution, endpoint, and orbit specs. Local syntax
and the first three cheap gates passed. The two cold recursive replays,
proof/RSS profiling, no-DNE/capacity checks, and adversarial mutations remain
WMI-only. Cheap body replay caught and fixed an apply-to-negation error in the
orbit source. Discovery job 172932, exact snapshot
5463565294da6d757356985a0e8d353ad2e0e16ca1b21b99d2aa5cfa6bb5c6f6,
was cancelled after consuming zero CPU. First replacement job 172970, exact
snapshot 9a59e7a590223d4852f02dde19633b21bfcc4fb92491705d4aade022a116265a,
was also cancelled after zero CPU. Corrected job 172978, snapshot
6d32a5ba65b2268dc3fd6c027726a86c5054788bbeb5edacd6d6cbec3373403e,
is pending at submission.
There is no report, pass, pinned metric receipt, or theorem admission.
The complete Wilson body stack now replays cheaply#
The bounded body replay succeeds for all 19 isolated Wilson candidates. It is also where the two prefix binder defects and the orbit apply-to-negation defect were found before expensive cluster work began.
layer |
body nodes/depth in source order |
|---|---|
square one |
|
pointwise inverse |
|
inverse prefix |
|
inverse involution |
|
inverse endpoints |
|
inverse orbit |
|
The prefix, involution, endpoint, and orbit suites also pass twelve bounded structural gates—contract/dependency, hygiene/native/witness, and graph/core/source isolation for each suite. These measurements check theorem bodies and bounded structure only; they do not recursively close the Cut graph, do not constitute closed-certificate admission, and admit no theorem.
Adjacent inverse pairs now have a generic product fold#
Two isolated candidates cover the arithmetic once the inverse factors have been laid out in adjacent pairs:
candidate |
exact role |
exact direct dependencies |
|---|---|---|
|
split a product of length |
|
|
from |
the preceding decomposition, |
The proof is constructive induction on m: decompose the final two factors,
apply the induction hypothesis to the prefix, multiply the two congruences,
and reassociate. It is intentionally generic; a later certificate must still
reindex the nonendpoint Wilson orbits into this adjacent layout and restore
the fixed endpoint factors.
Bounded replay caught two separate missing third-occurrence length rewrites in
successive snapshots. Jobs 172936 and 172943 were cancelled before start
as superseded known-broken jobs and supply no evidence. After both corrections,
all five focused gates passed locally in 5.4 seconds, including two cold passes:
candidate |
nodes |
depth |
distinct objects |
|---|---|---|---|
|
1,317 |
63 |
844 |
|
4,372 |
64 |
1,290 |
The graph hash is
622496753bd474f9f64d5d3001424d3c4513d43d6a5256022cd5a172167959ec;
the source hash is
193fe015b32ffde4d93e00720c9fef510a804228e24f19f5cc6c97e8ad5fa724.
The corrected unimported source is
wilson_pair_product_candidate.py.
Authoritative WMI job 172946, exact snapshot
9d890542b964d40580ad2f8f77fa83455de3b9af0f8ca905a37f6a6ee278e296,
is queued/pending on cpu_idle with 1 CPU, 16384 MiB, and 02:00:00.
Its independent five-gate replay remains the required admission receipt; the
local pass alone does not admit either theorem, and no WMI pass is claimed.
At this historical checkpoint Wilson still needed a beta-coded adjacent ordering and removal of its explicit endpoints. The later PairOrder tranche below now discharges iteration, adjacency, terminal coverage and canonical nonendpoint product transport. The current gap is endpoint restoration, the prime-two branch and the final factorial-product bridge.
PairOrder can append one fresh inverse orbit#
The isolated Wilson PairOrder layer now constructs one honest extension step. Its generic core appends two decoded entries and reflects the resulting prefix, while the Wilson specialization uses finite omission to choose a fresh nonendpoint inverse orbit. It preserves orbit closure, the nonendpoint range invariant and—through a separate reusable theorem—decoded-prefix injectivity.
candidate |
exact role |
body nodes/depth |
|---|---|---|
|
append two entries and preserve the old prefix |
|
|
classify every entry of the extended prefix |
|
|
choose an omitted bounded value distinct from both endpoints |
|
|
extract the fresh inverse mate and its two directed edges |
|
|
prove the mate is omitted from an orbit-closed old prefix |
|
|
preserve orbit closure |
|
|
preserve the nonendpoint range |
|
|
preserve decoded injectivity |
|
|
package one Wilson choose-and-append step |
|
These are hard-60-second dependency-curried body receipts, not recursively
closed certificates. Later isolated modules now discharge full iteration,
terminal coverage, successor-lifting and canonical nonendpoint product
transport, as summarized below. The complete encoding and its generic reuse
for Euler are in the
PairOrder design.
Focused job 173017, from exact snapshot
8c9c4ae067b0dc202684e410bee563cd592a67080cb7c9939440ae8b44d4bccd,
is pending with zero CPU; no replay result or admission is claimed.
The scaled inverse supplies Euler’s pointwise involution#
For a prime modulus, a nonzero bounded target a, and a nonzero bounded
residue x, the Euler entrance layer constructs the unique bounded y with
x*y == a (mod p). Symmetry and uniqueness make this relation involutive;
its fixed points are exactly the square roots of a, so ~QRes(p,a) makes it
fixed-point-free constructively.
candidate |
body nodes/depth |
|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The expanded contracts and finite-prefix boundary are documented in the
Euler scaled-inverse ladder.
The scripts remain isolated. Focused job 173015, from the same exact
snapshot, is pending with zero CPU and is not a theorem-admission receipt.
The finite map now exists as well. The isolated prefix layer stores, at
zero-based position i, an actual residue y satisfying
(S i)*y == a (mod p). Its extension, bounded-existence, and full-predecessor
existence bodies measure 105/36, 81/33, and 40/23; the focused capped
audit passes 4/4. At that map-existence checkpoint, decoded extensionality
and a fixed-point-free two-cycle order were the next boundaries.
Decoded extensionality is now body-green too. Five follow-on theorems prove
entry soundness, uniqueness-based extensionality, nonresidue fixed-point
freedom, bounded predecessor extraction for every positive mate, and decoded
involution at 58/25, 54/26, 36/27, 67/36, and 91/39. Their focused
audit passes 4/4. At that checkpoint, the finite two-cycle order and its
product comparison were both still open.
The algebraic half of that product comparison is now generic and body-green.
beta_adjacent_target_pairs_product_power turns m adjacent pairs whose
products are each congruent to a into an exact 2m-factor product congruent
to relational a^m. Its 118-command body measures 171/47, contains no DNE,
and passes a 4/4 focused audit in 1.71 seconds. At this algebraic checkpoint,
the remaining Euler gap was the fixed-point-free scaled-prefix reordering into
adjacent orbits. This receipt is dependency-curried only; recursive closure
and admission remain on WMI.
The quadratic-residue half of Euler’s criterion can bypass that ordering. A
new reusable body proves that congruence to zero modulo a nonzero natural
produces an explicit divisibility witness (48/18). From a square root
r^2 == a, the candidate constructs relational powers, identifies
(r^2)^h=r^(2h), invokes Fermat at p-1=2h, and transports congruence to
derive
[ QRes(p,a)\quad\Longrightarrow\quad a^h\equiv1\pmod p ]
under p=2h+1, primality and p not dividing a. The main 136-command body
measures 148/39; the two-spec no-DNE audit passes 4/4 in 2.11 seconds.
The later orbit-order and endpoint tranches now prove the bounded nonresidue
implication through Wilson. The bounded package and arbitrary-representative
transport below now expose the final equivalence. These are dependency-curried
results, not admitted library theorems.
That orbit order now has a sound one-step entrance. A scaled-prefix entry is
an actual mate S j, whereas Wilson’s generic closure expected the
zero-based j; the new Euler relation records this shift explicitly. Four
constructive bodies transfer omission across an involutive back edge, preserve
shifted closure under a two-entry append, choose an omitted distinct orbit
under ~QRes, and append it while preserving closure and injectivity. Their
nodes/depth are 34/20, 184/40, 107/38, and 190/52; the no-DNE audit
passes 3/3 in 2.78 seconds. No endpoints are excluded.
Balanced iteration through all n=2h sources is now body-green as well. The
state retains shifted closure, boundedness and decoded injectivity, while its
history records each adjacent pair together with the raw edge
At(scaled,i,S j) needed for later factor lifting.
isolated candidate |
exact role |
body nodes/depth |
|---|---|---|
|
empty shifted closure |
|
|
empty adjacent history |
|
|
preserve history across a two-entry append |
|
|
empty iterable state |
|
|
append one orbit and preserve state plus history |
|
|
rebalance stored and remaining pairs |
|
|
derive the strict-prefix witness |
|
|
iterate one orbit per stored pair |
|
|
specialize to |
|
|
derive full zero-based source coverage |
|
The exact focused audit passes 4/4 in 4.72 seconds with a separate
60-second CPU cap per body. All certificates are constructive and contain no
DNE. This remains dependency-curried, unregistered body evidence: recursive
closure and admission are still open; the endpoint tranche below now closes
successor-lift/product alignment and the bounded nonresidue implication. See the
iteration source
and
focused test.
Euler’s bounded nonresidue endpoint#
The terminal product/sign branch is now body-green. Five isolated candidates successor-lift the terminal scaled history, connect it to the generic adjacent-target fold, identify its exact product with the predecessor factorial, and invoke Wilson:
isolated candidate |
exact role |
deps |
body nodes/depth |
commands |
|---|---|---|---|---|
|
every lifted adjacent pair has product congruent to |
|
|
|
|
lifted terminal product equals the predecessor factorial |
|
|
|
|
adjacent power comparison plus Wilson gives |
|
|
|
|
package a full nonresidue scaled-prefix terminal endpoint |
|
|
|
|
construct the prefix and expose the bounded public endpoint |
|
|
|
In readable notation, the strongest theorem is
[ p=S n,\quad \operatorname{Prime}(p),\quad n=h+h,\quad 0<a<p, \quad \neg QRes(p,a),\quad Pow(a,h,A) \Longrightarrow A\equiv n=p-1\pmod p. ]
The exact focused audit passes 4/4 in 4.39 seconds; the endpoint plus its
related prerequisite stack passes 16/16 in 12.19 seconds. Every contract is
fully expanded constructive first-order PA, every certificate is free of
DNE, and all five candidates remain unregistered and unadmitted. See the
source
and test.
The bounded equivalence is now packaged as well:
isolated candidate |
role |
body nodes/depth |
|---|---|---|
|
derive the unit premise from |
|
|
exclude a doubled predecessor equal to one |
|
|
separate the canonical residues |
|
|
construct the matching endpoint |
|
|
|
|
|
|
|
|
expose both iff statements together |
|
For prime p=S n, n=h+h, reduced 0<a<p, and Pow(a,h,A), the final
package proves
[ QRes(p,a)\Longleftrightarrow A\equiv1\pmod p, \qquad \neg QRes(p,a)\Longleftrightarrow A\equiv n=p-1\pmod p. ]
The focused audit passes 4/4 in 1.67 seconds and the combined bounded Euler
run passes 12/12 in 7.62 seconds. All seven bodies are constructive,
unregistered, and unadmitted. See the
source
and test.
Euler’s criterion for arbitrary representatives#
The bounded theorem is now transported to every representative a for which
p does not divide a. The isolated implementation does not add %, /, a
power function, or a quotient function to PA. It uses division with remainder
to choose a canonical nonzero r<p, proves that QRes is invariant under
balanced congruence, and combines pow_exists with the already checked
pow_mod_congruent bridge.
isolated candidate |
exact contract or role |
deps |
commands |
body nodes/depth |
objects/edges/reuse |
|---|---|---|---|---|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
congruent bases and |
|
|
|
|
|
transport the residue iff to |
|
|
|
|
|
transport the nonresidue iff to |
|
|
|
|
|
expose both transported equivalences together |
|
|
|
|
The first three contracts are reusable outside Euler. In readable notation, the final theorem is
[ \begin{gathered} p=S n,\quad \operatorname{Prime}(p),\quad p\nmid a,\quad n=h+h, \quad Pow(a,h,A)\ \Longrightarrow \bigl(QRes(p,a)\Longleftrightarrow A\equiv1\pmod p\bigr) \land \bigl(\neg QRes(p,a)\Longleftrightarrow A\equiv n=p-1\pmod p\bigr). \end{gathered} ]
The focused audit pins all six expanded statement hashes, exact dependencies,
native syntax, registry isolation, and the receipts above. It passes 4/4 in
2.04 seconds under the 60-second CPU cap. The combined residue, nonresidue,
bounded, and arbitrary Euler selection passes 16/16 in 9.96 seconds. No
script uses DNE, classical reasoning, sorry, auto, or ring; none of
the six candidates is registered, recursively closed, or admitted. See the
source
and
test.
flowchart LR
T[terminal scaled PairOrder coverage] --> L[successor-lift adjacent targets]
L --> F[lifted product equals predecessor factorial]
L --> P[adjacent product equals half-power A]
F --> W[Wilson factorial congruence]
P --> N[bounded nonresidue endpoint A equals p-1]
W --> N
R[bounded residue endpoint A equals 1] --> E[complete bounded Euler equivalence]
N --> E
D[division with remainder under p not dividing a] --> K[nonzero canonical remainder r]
K --> Q[QRes congruence-class transport]
K --> PT[Pow base and result transport]
E --> U[complete arbitrary-representative Euler criterion]
Q --> U
PT --> U
U --> C[WMI closure mutations and admission]
Thus the terminal product/sign, bounded-equivalence, and arbitrary- representative gaps are body-green. The remaining Euler work is recursive WMI closure, mutation testing, and a separate admission replay.
The second frozen checkpoint reaches finite coverage#
The eleven-spec
magnitude-permutation endpoint
now proves range, collision control, magnitude injectivity, predecessor
recoding and finite surjectivity. Body nodes/depth are 39/25, 48/24,
96/34, 169/50, 626/70, 157/45, 31/25, 87/30, 48/20,
60/31, and 39/21. Focused job 173021, exact snapshot
fd129d34bf4a31a131a28d55bc6a16153984e0d37ac24dcefe7c2735cfb058d1,
is pending with zero CPU.
The corrected PairOrder state adds a bounded-into-domain invariant. Fifteen
follow-on candidates preserve that four-part state, construct its empty case,
manage pair-count arithmetic and prove terminal coverage of every bounded
nonendpoint. Their body nodes/depth are 95/40, 19/12, 69/27, 90/42,
23/19, 18/14, 20/16, 22/18, 64/19, 8/8, 12/9, 266/44,
33/20, 72/37, and 51/36; see the
PairOrder design.
Focused job 173022, from the same exact snapshot, is pending with zero CPU.
Three magnitude product-alignment bodies pass at 51/28, 127/39, and
72/34; two sign-product/power bodies pass at 35/24 and 259/46.
The next laptop-safe authoring pass also completed sign-factor recoding,
generic pointwise-product recoding, the signed pointwise congruence, and the
constructive prime-product cancellation boundary. The composed endpoint now
has a dependency-curried kernel receipt for
[ a^h P\equiv P(p-1)^e\pmod p \quad\Longrightarrow\quad a^h\equiv(p-1)^e\pmod p. ]
Its balance and cancellation bodies measure 148/70 and 156/87
nodes/depth. The cancellation uses positivity of 1,...,h, finite-product
coprimality, and balanced Bézout; it does not assume a field or classical
inverse. A follow-on existential endpoint now constructs every signed code,
product, count and power witness and exposes only e,A,R with
[ A=a^h,\qquad R=(2h)^e,\qquad A\equiv R\pmod p. ]
That body has 193 commands, 258 nodes and depth 83, with no DNE. The next
composition now reaches actual quadratic-residue status. For p=2*h+1, a
prime p, 0<a<p, and the canonical half range,
bounded_gauss_lemma_complete retains the signed-prefix and BitCount(e)
provenance and proves
[ \operatorname{QRes}(p,a)\leftrightarrow\operatorname{Even}(e),\qquad \neg\operatorname{QRes}(p,a)\leftrightarrow\operatorname{Odd}(e). ]
Its pinned direct receipt is 11 dependencies, 204 commands, 597 nodes, depth
53, 559 objects, 596 edges, and 38 reused objects. The arbitrary wrapper
replaces 0<a<p by p not dividing a and invokes arbitrary-representative
Euler; its receipt is 9 dependencies, 188 commands, 547 nodes, depth 49, 513
objects, 546 edges, and 34 reused objects. Their focused modules pass together
at 9/9 in 13.64 seconds.
The arbitrary recipe is fail-closed source-shared from the bounded classification tail, then replayed independently against its own expanded contract. Neither source sharing nor a body receipt grants theorem authority: both endpoints remain dependency-curried, registry-isolated, and unadmitted.
flowchart LR
S[signed half prefix] --> M[magnitude product P]
S --> B[reflection count e]
B --> R[sign product = p-1 to e]
M --> C[a to h times P = P times R mod p]
R --> C
U[positive factors below prime] --> K[P coprime to p]
K --> X[cancel P]
C --> X
X --> G[a to h = p-1 to e mod p]
G --> L[bounded actual-QRes Gauss classification]
EB[complete bounded Euler] --> L
PB[predecessor-power parity] --> L
L --> QE[QRes iff e even]
L --> QO[not QRes iff e odd]
G --> A[arbitrary prime-unit Gauss classification]
EA[arbitrary Euler] --> A
On the Wilson side, full pair-count iteration now retains an explicit
PairedInverseWitness; successor lifting turns each zero-based inverse pair
into two actual residue factors, and the resulting 2m-factor product is
congruent to one. The four lift/product bodies measure 17/11, 124/38,
41/31, and 65/32. Four further bodies extract the exact terminal magnitude
range, align its predecessor map with the successor-lifted order, transport
the product to the canonical nonendpoint range, and package both products;
they measure 80/30, 152/42, 79/39, and 188/65. The remaining Wilson
endpoint is now body-green too. Seven restoration bodies supply the leading
unit, restore p-1, connect to relational factorial, split prime 2 from the
odd shape, and prove
[ p=Sn\land\operatorname{Prime}(p)\land\operatorname{Factorial}(n,F) \Longrightarrow F\equiv n\pmod p. ]
Their nodes/depth are 30/15, 258/45, 63/29, 21/16, 104/30,
94/35, and 110/31; the focused no-DNE audit passes 3/3. The prime-two
branch never invokes the odd PairOrder. Recursive WMI closure and admission
remain separate.
Native division prefixes for Eisenstein sums#
The first Eisenstein layer is now concrete. For every decoded source value
x at i<l, DivisionPrefix constructs aligned beta entries q,r with
[ x=pq+r,\qquad r<p. ]
beta_division_prefix_extend appends one pair (132/41 nodes/depth, 94
commands), and beta_division_prefix_exists iterates the construction over
any finite source (71/30, 62 commands). The focused capped audit passes
4/4. A follow-on exact-value layer combines a constant prefix with the
canonical half range, pointwise-multiplies them, divides every a*(1+i), and
constructs the quotient sum. Its three bodies measure 34/24, 71/40, and
52/28, with another 4/4 capped audit. This remains a candidate layer: the
equality between quotient sums and lattice counts, the two-orientation
partition, and WMI closure are still required. See the
division-prefix design.
The smallest arithmetic threshold connecting those quotients to a row is now
body-green. nonzero_remainder_division_positive_multiple_threshold proves
[ n=pq+r,\quad r\ne0,\quad r<p \quad\Longrightarrow\quad \bigl(p(j+1)<n\iff j+1\le q\bigr) ]
using only witness-defined natural order. Its body has 92 nodes, depth 30,
and 67 commands; the exact no-DNE audit passes 4/4 in 0.30 seconds under
the 60-second CPU cap. This is an isolated dependency-curried body, not a
recursively closed, registered, or admitted theorem.
The scaled-remainder premise is now discharged by three isolated bodies:
isolated candidate |
exact role |
body nodes/depth |
|---|---|---|
|
|
|
|
distinct primality supplies |
|
|
|
|
No remainder-bound premise such as r<p is needed for nonvanishing. The
focused exact-contract audit passes 4/4 in 0.40 seconds and finds no DNE;
the bodies remain dependency-curried, unregistered, and neither recursively
closed nor admitted. See the
remainder-nonzero source
and its
focused test.
The divisor-own-half condition is essential. The proposed cross-half variant
p=2*k+1, q=2*h+1, i<h is false: with p=3, q=7, and i=2, one has
[ q(Si)=7\cdot3=3\cdot7+0. ]
The corrected wrapper instead assumes i<k, where k is the half belonging
to the divisor p.
Both former arithmetic application gaps are now body-green. The odd-half quotient module proves the explicit gap
[ (2k+1)h<(2h+1)(k+1) ]
and uses it to derive d<=k from p=2*h+1, q=2*k+1, i<h, and
q*S i=p*d+r. The bodies measure 160/45 and 67/29 nodes/depth, with
13 and 62 commands. Neither primality nor a remainder condition is
needed. Its combined focused run with the sound remainder suite passes 8/8
in 0.54 seconds. See the
source
and test.
The generic initial-segment module constructs a beta-coded bit prefix whose
entry at j is 1 exactly when S j<=q and 0 when q<S j, then proves
that any native BitCount of the prefix equals q whenever q<=k.
isolated candidate |
exact role |
body nodes/depth |
commands |
|---|---|---|---|
|
choose one exact threshold bit |
|
|
|
append one threshold bit |
|
|
|
construct the finite prefix |
|
|
|
derive |
|
|
|
recover decoded threshold semantics |
|
|
|
count an all-one prefix |
|
|
|
identify any bounded-prefix count with |
|
|
|
package the exact |
|
|
The exact-contract audit passes 11/11 in 2.09 seconds, pins all eight
receipts, and finds no DNE. See the
source
and test.
These results are dependency-curried, unregistered, unadmitted, and not yet
recursively WMI-closed.
The client-specific row bridge is body-green too:
isolated candidate |
exact bridge |
deps |
body nodes/depth |
commands |
|---|---|---|---|---|
|
threshold semantics to the exact initial-segment relation |
|
|
|
|
semantic |
|
|
|
|
row count to the aligned decoded quotient |
|
|
|
|
existing outer semantic row witness to the decoded quotient |
|
|
|
The focused audit passes 4/4 in 3.40 seconds; the four bodies together with
their explicit prerequisite stack pass 27/27 in 5.86 seconds. They use no
DNE, auto, or ring, and remain unregistered and unadmitted. See the
source
and test.
This closes pointwise row-count identification, but not the outer-sum
endpoint equality.
The generic outer-fold transport is body-green as well.
beta_sum_transport_prefix reuses an existing relational partial-sum trace
when a second beta prefix decodes pointwise to the same bounded entries. It
has no theorem dependencies and measures 59/29 nodes/depth, 59 objects,
58 edges, no reuse, and 44 commands. Its focused audit passes 3/3; the
combined initial-segment and transport run passes 14/14 in 2.20 seconds.
The proof contains no DNE and does not identify raw beta codes. See the
source
and test.
This candidate is likewise unregistered and unadmitted.
The concrete outer transport and endpoint bridge is now body-green:
isolated candidate |
exact bridge |
deps |
body nodes/depth |
commands |
|---|---|---|---|---|
|
decoded quotient entry equals its semantic outer row count |
|
|
|
|
transport the quotient |
|
|
|
|
identify the exposed |
|
|
|
The focused audit passes 4/4 in 4.92 seconds; the bridge with its related
prerequisites passes 19/19 in 10.71 seconds. The bodies contain no DNE,
auto, or ring and remain unregistered and unadmitted. See the
source
and test.
This proves quotient Sum = semantic rectangle total for one orientation,
and the uniformly quantified theorem applies again after swapping the two
primes and their halves.
The first-orientation floor/quotient sum is therefore identified with its semantic total, and the swapped orientation has the same bridge. The next body-green layer performs the two-dimensional relation between those nested semantic totals across the transposed indexing.
The diagonal arithmetic is already settled constructively. For distinct odd
primes and bounded half-range indices, a hypothetical
q*(S i)=p*(S j) contradicts Euclid’s lemma, prime rigidity and the strict
half bound. The resulting noncollision, exclusive-cell orientation and
universal-rectangle bodies measure 72/30, 77/34, and 53/34; their audit
passes 4/4. Thus no remaining counting step needs to decide which side of
the diagonal a cell occupies.
The row encoding is now body-green. For each fixed i, a beta-coded bit row
over j<k records exact orientation semantics and a native BitCount gives
the row total. Its seven bodies measure 46/29, 71/27, 58/23, 53/34,
27/16, 43/23, and 63/29; the focused audit passes 4/4. These semantic
row-count witnesses are the inputs to the outer representation.
That outer representation is now body-green as well. It deliberately keeps one existential inner row code at each outer position; equality of raw beta codes is not used as equality of represented rows. The eight exact bodies are:
isolated candidate |
exact role |
body nodes/depth |
|---|---|---|
|
one semantic count choice for a bounded row |
|
|
append one count and preserve earlier row semantics |
|
|
outer-prefix existence by ordinary induction |
|
|
choices for every |
|
|
encode a bounded initial set of rows |
|
|
encode all |
|
|
recover the inner row and |
|
|
attach the native beta |
|
Their exact-contract, no-DNE audit passes 4/4 in 2.22 seconds under a
60-second CPU cap. This is dependency-curried body evidence only: the module
proves existence of a nested rectangle total. The separate outer-sum bridge
now identifies it with the orientation’s quotient/floor sum. The later
column endpoint proves one fixed row/column partition, and the Fubini layer
below aggregates those partitions into the exact two-orientation identity.
None of these candidates is recursively WMI-closed, registered, or admitted.
The one-dimensional complement identity described above applies once two same-length row prefixes have been aligned pointwise. It gives the exact local equation “left count + right count = row length.” It does not itself transpose the nested row-major encoding; the dedicated Fubini induction below uses these local equations and the provenance-carrying columns to do so.
The transposed cell semantics and their nested exposure are now body-green:
isolated candidate |
exact bridge |
deps |
body nodes/depth |
commands |
|---|---|---|---|---|
|
decoded |
|
|
|
|
open both existential inner rows and package the complementary decoded cells |
|
|
|
Their combined focused audit passes 6/6 in 2.08 seconds. Both bodies are
constructive, contain no DNE, and remain unregistered and unadmitted. See
the
cell source,
cell test,
outer-cell source,
and
outer-cell test.
These witnesses expose every local complement fact but do not sum the
row-major and column-major nested folds.
The next six body-green isolated candidates construct the complete transposed column for one fixed original-row index:
isolated candidate |
exact bridge |
deps |
commands |
nodes/depth |
objects/edges/reused |
|---|---|---|---|---|---|
|
select the fixed-index cell from every swapped row |
|
|
|
|
|
append one provenance-carrying column entry |
|
|
|
|
|
beta-code all |
|
|
|
|
|
prove that the constructed column is a bit prefix |
|
|
|
|
|
align original-row and constructed-column bits |
|
|
|
|
|
attach the column count |
|
|
|
|
Here provenance is part of the mathematics, not bookkeeping. At every
j<k, a stored column bit retains the decoded entry of the swapped outer
count prefix; an existential inner row code and scale with the exact swapped
row semantics; that row’s BitCount witness; and the decoded inner cell at
the fixed i<h. Prefix extension preserves the whole package. Consequently,
the endpoint cannot be satisfied by an unrelated beta code that happens to
contain the same zeroes and ones.
In readable notation, the strongest endpoint consumes an original semantic
row R_i, its count n, the swapped semantic outer rectangle, and i<h, and
constructs z,e,m such that
[ \operatorname{TransposedColumn}(z,e,i,k);\land; \operatorname{BitCount}(z,e,k,m);\land;n+m=k. ]
The exact
column source
and
focused test
pass 5/5 in 5.05 seconds under the 60-second laptop cap. Besides replaying
all six bodies, the audit pins names, dependencies, statement hashes and the
receipts above; checks alpha-hygiene and fully expanded native PA; and rejects
auto, ring, DNE, by_contra, classical, and sorry. These remain
dependency-curried, unregistered and unadmitted candidates.
flowchart LR
D[decoded quotient and remainder] --> N[nonzero-remainder threshold]
D --> B[odd-half quotient bound]
N --> P[exact pointwise row predicate]
B --> P
P --> C[initial-segment BitCount equals quotient]
R[semantic row BitCount] --> I[row-count identification]
O[exclusive cell orientation] --> R
O --> X[complementary row BitCount]
C --> I
I --> U[beta_sum_transport_prefix]
U --> S[orientationwise quotient Sum equals rectangle total]
U --> S2[swapped-orientation quotient Sum equals rectangle total]
R --> K[complement counts add row length]
X --> K
O --> TC[decoded transposed cells complementary]
A[outer prefix for p q] --> W[outer complementary-cell witness]
Z[outer prefix for q p] --> W
TC --> W
Z --> H[fixed-index choices from swapped rows]
H --> J[provenance-carrying transposed column]
J --> M[column BitCount]
R --> E[row count plus column count equals k]
M --> E
S --> F[nested 2D transpose / Fubini body-green]
S2 --> F
K --> F
W --> F
E --> F
F --> I[exact quotient identity Q plus U equals h times k]
G[Gauss counts e and f] --> GP[pointwise and Sum parity]
GP --> GA[e equals Q and f equals U mod 2]
I --> GA
GA --> Q[exact same/opposite QR surfaces]
Every edge through S, TC, W, E, F, I, and GA is now body-green,
and S applies to both orientations by swapping the parameters. No equality
of raw beta codes substitutes for decoded-entry functionality along this
path.
Exact Fubini identity#
The nine-body Fubini follow-on constructs an outer beta prefix of the column
counts, retargets its semantic witnesses during induction on h, sums the
equations row_count_i+column_count_i=k, and identifies the constructed
column-count sum with the swapped row total. The central universal body is
264/65 nodes/depth; the final semantic endpoint
eisenstein_rectangle_floor_sum_identity is 65/37.
The exact quotient wrapper applies the orientationwise quotient/rectangle
bridge twice and eliminates the semantic totals while retaining all two
scaled prefixes, division prefixes, outer row-count prefixes, and Sum
traces:
[ Q+U=h k. ]
distinct_odd_prime_eisenstein_quotient_sum_identity has 3 dependencies,
123 commands, 145 nodes and depth 68. This closes the formerly open
rectangle-level mathematical gate at the dependency-curried body level.
Pointwise Gauss–Eisenstein parity and exact sums#
The exact finite-sum permutation ladder mirrors the product-permutation architecture:
Candidate |
Body nodes/depth |
|---|---|
|
|
|
|
|
|
|
|
For each decoded division a*(i+1)=p*q_i+r_i, the signed branch gives
s_i congruent q_i+m_i (mod 2). The beta-level endpoint
gauss_eisenstein_prefix_pointwise_mod_two proves that relation at every
bounded index while preserving every aligned code parameter. Its body is
250/61, and its expanded statement SHA-256 is
84b039612f162c0c0935ebf49e1ffadf0cdf8e660914f583b7f490744175884e.
Four generic sum-congruence/cancellation bodies measure 39/24, 42/19,
24/15, and 328/66. Three exact magnitude-sum permutation bodies measure
148/42, 72/34, and 90/43; the terminal fold, cancellation, and count
endpoint measure 83/54, 107/66, and 89/65. The strongest endpoint keeps
the half range, scaled/division prefixes, signed magnitude/sign prefixes,
BitCount, and exact quotient Sum, then proves
[ Q\equiv e\pmod2. ]
The pointwise and sum suites pass together at 12/12 in 17.47 seconds.
Two-prime package and exact reciprocity surfaces#
One existential constructor packages a single odd-prime orientation: its
division codes, Gauss count e, quotient sum Q, the two actual-QRes
equivalences, and e congruent Q (mod 2). Its direct receipt is
5/102/139/67 in dependencies/commands/nodes/depth order.
The two-prime constructor applies that package in both orientations and joins
it with Q+U=h*k. Its public witnesses are only e,f,Q,U; its receipt is
4/150/222/77. A six-body constructive truth-table layer transports parity
from the count sum to the half product and then translates half parity into
the modulo-four hypotheses. The two conditional wrappers are 49/31
nodes/depth each.
The final bodies are exactly the expanded public formulas introduced at the top of this chapter:
Exact endpoint |
Direct receipt |
|---|---|
|
|
|
|
|
|
Read the 65-line wrapper in the native PA proof explorer, then follow any highlighted lemma reference backward through the full closure, or draw its dependency paths.
The downstream data, parity, conditional, and final integration passes
20/20 in 27.25 seconds. The optimized combined body constructs the pair
data once and calls both conditional clients directly; its exact statement
and hash are unchanged. The exact dependency graph has 557 unique
specifications, 1,787 direct edges, 45 layers, 48 theorem roots, and root
depth 44. Recursively
expanding its theorem dependencies produces 191,648 theorem occurrences,
down from 382,882 for the superseded wrapper. That count is a static graph
result, not a closed-proof receipt.
Historically this was only a complete dependency-curried, body-green
mathematical route. The subsequent complete layered ordinary-Cut
construction now passes the unchanged kernel from the empty context, the
full modular proof bundle passes independent Lean verification, and immutable
Alpha v16 admits exactly the 315 newly closed results for checked use. None
is added to the default Stable/public registry, and fresh WMI replay remains
separate evidence rather than a prerequisite for claiming the already checked
local mathematical proof.
The first full 136-gate WMI attempt, job 187187, failed closed after 39
seconds at gate 5. Four scaled-inverse gates passed; the mutation audit then
found an unused succ_ne_zero dependency, so 131 gates were never reached.
That redundant edge was removed and the focused local suite passed; at that
historical checkpoint no complete quadratic-reciprocity admission receipt
existed. Corrected full
job 210714, from clean snapshot 989011c0…1757, subsequently failed closed
after 8 minutes 29 seconds at gate 15/136. Fourteen gates passed; the next
direct-edge mutation showed that replacing
odd_upper_remainder_reflection -> add_succ_left did not invalidate the
certificate, and 121 gates were unrun. This is a dependency-minimality
failure, not a kernel-soundness failure or a quadratic-reciprocity result.
pointwise source
· pointwise test
· sum source
· sum test
· Fubini source
· quotient identity
· data source
· data test
· final source
· final test
Closing the theorem DAG without changing the kernel#
The mathematical proof is no longer the capacity problem. The exact closure
graph is a moderately sized DAG whose shared ancestors are duplicated when
each theorem is recursively expanded into every later Cut branch:
Static graph quantity |
Exact value |
|---|---|
theorem specifications |
557 |
direct dependency edges |
1,787 |
dependency layers |
45 |
longest path |
44 edges |
theorem occurrences after recursive expansion |
191,648 |
That recursive tree cannot satisfy the current 500,000-node policy. Even
before charging a single apply, split, exists, equality, induction, or
rewrite constructor, it necessarily contains:
Forced contribution |
Proof-node occurrences |
|---|---|
at least one body node per theorem occurrence |
191,648 |
dependency |
191,647 |
recorded leading theorem-level |
348,128 |
rigorous lower bound |
731,423 |
The static hotspot audit derives these values directly from the frozen graph recurrence. Raising the limit would hide known tree-expansion duplication rather than pay for new mathematics.
The preferred compiler instead assigns every theorem to its dependency depth
and joins the formulas in each layer into a balanced conjunction. A theorem’s
dependency-curried body occurs exactly once. Its direct dependencies are
obtained from earlier packages by the existing AndElimL and AndElimR
rules, then supplied by ordinary implication elimination. One existing
contextual Cut introduces each layer package, so the full spine has 45 Cuts
rather than a 557-theorem sequential spine or a 191,648-occurrence recursive
tree.
The final artifact is still an ordinary Peano Lab Proof. Its only authority
is the unchanged kernel judgment
check((), certificate, QUADRATIC_RECIPROCITY_COMBINED)
No theorem name, graph hash, cached receipt, or new proof rule is trusted. A compiler mistake in the layer ordering, hypothesis index, conjunction path, or root projection therefore makes the existing checker reject the result. On a 20-node, eight-layer sharing fixture, both approaches check under that kernel, while the balanced bundle measures 274 nodes at depth 16 versus 3,643 nodes at depth 20 for recursive closure.
The exact QR topology has also been exercised without doing theorem replay.
A 557-body dummy scaffold exposes 13,148 fixed glue nodes and compiles to
13,705 nodes at depth 56, with 157,579 formula/term annotation occurrences,
combined proof-envelope depth 92, and package-formula cost 144,197/68; its
dummy proof is rejected by the kernel, as it must be. A second surrogate
retains all 557 nodes, 1,787 dependency edges, 45
layers, dependency orders, package projections, and context indices, while
assigning every node a unique shallow reflexive marker formula derived from
the bits of its local node ID. Each curried marker body also contains one
existing Cut per direct dependency: its lemma branch checks the dependency’s
exact marker target against the matching Hyp(k-1). This forces every real
package projection ID and direction, as well as declared dependency order, to
type-check. The unchanged kernel accepts the strong surrogate at 19,066 proof
nodes and depth 74; its annotations measure 142,134 occurrences at combined
envelope depth 84, and its package formulas measure 19,297 occurrences at
depth 18. The scanner covers all 25 exact kernel proof constructors and rejects
DNE, holes, metavariables, custom proof nodes, and malformed annotations.
Neither experiment proves QR: one is deliberately invalid, and the other
contains marker equalities rather than QR formulas.
Evidence boundary
The generic compiler, synthetic comparison, fixed-scaffold measurement, and distinct-target topology surrogate are green at their stated evidence levels. The complete 557-body certificate with the real QR targets and bodies has not yet been constructed and checked on WMI, profiled, mutation-tested, or replayed in Pyodide. Quadratic reciprocity is therefore still unregistered and unadmitted.
See the full layered construction and gate list. The closed-proof DAG design is retained only as a fallback if the ordinary layered certificate fails a measured object, formula, depth, memory, or browser gate.
generic compiler
· QR adapter
· production tests
· recursive comparison
· QR static tests
· WMI integration
Signed-half representatives and finite omission#
Two new isolated Gauss candidates begin the signed-half construction without
postulating a choice function. odd_upper_remainder_reflection reflects an
upper-half remainder across an odd modulus; the pointwise theorem
gauss_pointwise_signed_half_representative chooses either the least positive
remainder or its reflected representative. Their body-only laptop receipts
are 125 nodes/depth 34 and 116 nodes/depth 38. The source is
gauss_signed_half_candidate.py.
The pointwise layer is now lifted by a second isolated source into aligned
β-coded magnitude and sign prefixes:
flowchart LR
A[pointwise signed representative] --> B[explicit 0/1 signed choice]
B --> C[choices at every half-range index]
D[two beta-prefix extensions] --> E[generic aligned-prefix existence]
C --> F[full half-range signed prefix]
E --> F
F --> G[AllBits sign projection]
G --> H[relational BitCount existence]
new isolated candidate |
exact role |
body nodes/depth |
|---|---|---|
|
attach the decoded source and explicit sign bit |
|
|
construct choices at every index |
|
|
append one magnitude and sign simultaneously |
|
|
encode any bounded choice family |
|
|
specialize to the full interval |
|
|
project the sign code to canonical |
|
|
obtain the native relational count of upper-half signs |
|
A 60-second-capped dependency-curried kernel preflight accepted these seven
bodies and the two earlier candidates in about 1.8 seconds after exposing one
missing explicit negation binder. This is body-only evidence: dependencies
remain hypotheses, no closed certificate is produced, and no theorem is
admitted. The focused gauss-signed-prefix WMI suite now carries the recursive
closure, profiling, no-DNE/capacity, deterministic-hash, strengthened-contract,
and every-direct-Cut mutation gates. The full representation and exact next
boundary are documented in the
signed-prefix design.
The later magnitude, sign-factor, pointwise-product, cancellation, and
existential endpoint layers are summarized above. The bounded and arbitrary
actual-QRes classifications now close the mathematical bridge. What remains
for the focused Gauss suites is recursive WMI closure and mutation review; the
complete endpoint graph instead uses the layered closure described above.
Both paths still require separate pinned admission receipts.
The finite-omission candidate supplies the reusable finite combinatorics needed for deletion and reindexing. Its eight theorem bodies have these bounded local receipts:
candidate |
body nodes |
body depth |
|---|---|---|
|
73 |
22 |
|
69 |
27 |
|
58 |
23 |
|
21 |
15 |
|
89 |
31 |
|
149 |
43 |
|
24 |
16 |
|
27 |
18 |
See
finite_omission_candidate.py.
For wilson-square-one, gauss-signed-half, and finite-omission, the three
bounded structural gates passed locally: exact contract/dependency checks,
helper hygiene/native/witness checks, and graph/core/source isolation. These
are body-only or structural observations, not closed recursive replay and not
closed-certificate admission. No new theorem has been admitted.
The two new focused suites were submitted from common exact snapshot
9a59e7a590223d4852f02dde19633b21bfcc4fb92491705d4aade022a116265a:
job 172964 runs gauss-signed-half, and job 172965 runs
finite-omission. Both are PENDING (Priority) with zero CPU.
The later focused gauss-signed-prefix job 173016 uses exact snapshot
8c9c4ae067b0dc202684e410bee563cd592a67080cb7c9939440ae8b44d4bccd
and is likewise pending with zero CPU.
Cluster-only experimental gate#
The authoring laptop may run static gates and dependency-curried body
preflight only, with a hard 60-second cap. Recursive closure, certificate
profiling, mutation checking, full-ladder regression, and book builds for this
tranche run on WMI.
The separate static-clean procedure is documented in the
WMI Jupyter Book build harness;
its independent static audit findings have been remediated. Test-only
scheduler validation succeeded for frozen snapshot
6feb5ebcdb9f59e6d94b71acd3fb2bce06d45b3a3885ad95aa8e9c02d61a3bcb
with content-manifest SHA-256
c09064eb67906761c357626df4ee9e0cf387a89b7593654c8c5bf74baf836c24.
Real Book job 173024 was last observed PENDING (Priority) with zero CPU, so
no Book-build or integrity result is claimed.
Each dirty worktree is archived first; the archive SHA-256 names an immutable
remote directory, and the Slurm report binds that hash, the local commit,
dirty-state flag, job identifier, selected gates, host, Python version,
duration, peak memory, and final status.
The 2026-07-30 submission ledger, including superseded provenance, is:
job |
immutable snapshot |
experiment |
status at submission |
|---|---|---|---|
|
|
22-gate product-reindex, bounded-unit, capacity, mutation, and full-ladder replay |
user-held, not cancelled |
|
|
the same integration suite preceded by three cold Fermat-candidate gates |
user-held, not cancelled |
|
|
two successor-recoding and canonical multiplication-map candidates, then all earlier gates |
user-held, not cancelled |
|
|
pointwise scale-product transport plus all earlier candidate and integration gates |
user-held, not cancelled |
|
|
original focused residue-reindex discovery |
cancelled stale job; zero CPU |
|
|
original focused product-balance discovery |
cancelled stale job; zero CPU |
|
|
original focused |
cancelled stale job; zero CPU |
|
|
original focused |
cancelled stale job; zero CPU |
|
|
original |
cancelled stale job; zero CPU |
|
|
original |
cancelled stale job; zero CPU |
|
|
original |
cancelled stale job; zero CPU |
|
|
original |
cancelled stale job; zero CPU |
|
|
stale pair-product snapshot with a missing third rewrite |
cancelled before start; superseded |
|
|
second stale pair-product snapshot with a separate missing third rewrite |
cancelled before start; superseded |
|
|
authoritative focused five-gate |
queued/pending on |
|
|
focused |
|
|
|
focused |
|
|
|
corrected |
|
|
|
first replacement |
cancelled stale job; zero CPU |
|
|
first replacement |
cancelled stale job; zero CPU |
|
|
first replacement |
cancelled stale job; zero CPU |
|
|
corrected |
pending at submission |
|
|
corrected |
pending at submission |
|
|
corrected |
pending at submission |
|
|
corrected |
pending at submission |
|
|
corrected |
pending at submission |
|
|
corrected |
pending at submission |
|
|
corrected |
pending at submission |
|
|
focused |
pending, zero CPU |
|
|
focused |
pending, zero CPU |
|
|
focused |
pending, zero CPU |
|
|
focused |
pending, zero CPU |
|
|
focused |
pending, zero CPU |
This table is an experiment log, not a success receipt. Admission requires a
completed JSON report whose hash matches the Slurm log, followed by a second
snapshot with the discovered statement hashes and certificate metrics pinned
as exact expectations. The complete operational contract is the
WMI replay policy.
The corrected five-gate Fermat jobs are 172988–172990. Their pending
scheduler state is not a pass, and no theorem is admitted. Report validation,
exact metric/hash pinning, and a distinct admission replay remain future gates.
All heavy replay, profiling, and mutation work remains WMI-only.
The holds on jobs 172707, 172716, 172722, and 172737 are reversible
queue prioritization, not cancellation. They are to be released after focused
results settle.
All three test-only validations for snapshot 8c9c4ae0... returned exit zero
after the transport changed from bash -l -s to bash -s. The former login
shell ran a WMI logout hook that overwrote an otherwise successful status with
local exit 1; this was a transport defect, not a failed Slurm validation.
The first frozen Euler/signed-prefix/PairOrder checkpoint exposed 14 focused
five-gate suites and 101 full gates across 22 test sources. With magnitude
permutation and bounded PairOrder induction included, the live runner exposes
16 focused five-gate suites and a 111-gate full audit across 24 test sources.
These counts describe the selected test surface, not successful theorem
results.
An earlier scale-product snapshot (3d3f1916..., job 172734) was cancelled
while still pending after static review found reusable-helper hygiene that
could be strengthened. It consumed zero CPU time and is not an admission
artifact; the immutable remote archive remains available for provenance.
Capacity policy#
The campaign does not solve certificate pressure by removing checks. Live composition has three independent gates:
at most 500,000 structural proof occurrences;
at most 100,000 distinct in-memory proof objects;
depth at most 256.
FTA provided the first measurement: 73,767 structural occurrences but only 8,701 distinct proof objects, a sharing ratio of 8.478. The higher structural ceiling therefore admits real shared certificates while preserving the former worst-case object count.
The QR hotspot audit now adds a decisive negative result for the old compiler:
its 191,648 recursively expanded theorem occurrences force at least 731,423
proof nodes, already beyond the structural ceiling. The limit should not be
raised to accommodate this duplication. The first-choice admission artifact
is the 45-layer balanced-conjunction bundle described above; its exact final
node/object/depth/formula/RSS measurements remain WMI gates. See the research
capacity decision
for the profiler and exact gates, the
hotspot audit
for the lower bound, and the
layered design
for the unchanged-kernel compiler. The linked admission design originally
froze the pre-overlap 317-candidate state. The strict-HA campaign has since
admitted the exact Wilson bounded_mod_inverse_unique specification, so the
live QR partition is 241 public / 316 candidate and the remaining enrollment
was historically described as 315 proper candidate ancestors plus the root.
In the immutable historical Alpha-v15 ledger all 316 were enrolled: 314 were
body-only, mod_eq_add_cancel_left was Alpha-closed through the HA receipt,
and the root remained pending. Current Alpha v16 preserves every historical
artifact but promotes those 314 ancestors and their root after independently
checking the complete genuine proof, so all 316 are now Alpha-closed and the
root has checked-use authority without Stable membership. The separate
public-admission design
specifies how to enroll that remaining order without an
import cycle, recursive fallback, or theorem-name authority. The companion
test-migration audit
retains the historical 317-enrolled/29-omitted partition and identifies every
candidate test whose pre-admission absence assumption must change in the full
enrollment commit. The live factory partition is
\(346=316+1+29\): remaining candidates, the public migration, and omitted
non-ancestors.
Campaign checkpoints#
Gate |
Mathematical deliverable |
Status |
|---|---|---|
QR-0 |
parity, modulo \(4\), quadratic-residue decision |
all graph prerequisites have independently checked Stable or Alpha-v16 closed proofs; historical body-only labels remain source provenance |
QR-1 |
|
the complete dependency slice is closed and available for independently checked Alpha-v16 use |
QR-2 |
modular units, bijections, Wilson, Fermat, Euler |
the complete factorial, bounded-product, and representative-transport dependency slice is independently closed in immutable Alpha v16 |
QR-3 |
Gauss’s lemma |
bounded and arbitrary actual- |
QR-4 |
Eisenstein identity and reciprocity |
the exact combined endpoint has a 54,870-node unchanged-kernel empty-context proof; all 557 proof bodies also pass independent Lean verification and the root is |
QR-5 |
supplementary laws and extensions |
first and second supplements remain separately scoped after admission of the main graph |
Every gate ends with cold replay, false-target mutation tests, exact structural/identity metrics, browser replay, synchronized catalog entries, Obsidian notes and an updated version of this chapter.