Native first-order arithmetic
Trace every dependency, inspect every tactic, and move between exact formulas and readable defined notation. No proof assistant installation is required.
Reciprocity law
Read the complete independently kernel-checked proof through 40 linked mathematical definitions, or descend to its exact fully expanded PA formulas and separate Lean verification.
See its reciprocity research family · Locate the proved milestone
Prime existence
Follow the complete independently kernel- and Lean-verified constructive prime-existence proof through linked definitions for primes, binomial coefficients, primorials, and valuations.
See its prime-distribution family · Locate the proved anchor
Current Alpha v34 release
131 newly admitted results extend Alpha to 4,223 checked-use entries. Stable remains the unchanged 432-theorem default. The actual 493-node polynomial bundle and 215-node congruence bundle have fresh original HA and same-byte compiled Lean checks, with nineteen ordinary principal certificates.
Polynomial gcd/Bézout existence, greatestness and normalized uniqueness are proved, including zero inputs. Non-coprime congruences have explicit bounded solution parametrizations. The first-layer foundations remain complete; full G091 remains open. Definition arrows remain notation, never extra proof premises.
Alpha v34 checked use · 119 independently proved theorems
Follow shift/scalar laws, associativity, length alignment and Euclidean backward transport through degree descent to an actual zero-or-monic gcd with Bézout coefficients. Prove greatestness and uniqueness up to formal coefficient equivalence.
Ten conservative definitions organize the construction. Empty and all-zero polynomials are included; raw beta codes and non-unique Bézout coefficients are never equated.
Recursive normalized gcd/Bézout proved · full G091 remains open; not Stable
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v34 · not Stable.
Campaign connections: Euclidean division · G091: the larger finite-field goal
Alpha v34 checked use · 12 independently proved theorems
Cancel a coefficient at the gcd-reduced modulus, describe every solution class and construct a reduced representative. Bounded solutions are in explicit bijection with t<g through x=r+M*t: exactly g solutions when the gcd divides the target.
Modulus zero and one have separate exact contracts. Fermat's theorem covers all natural inputs, including zero and prime multiples. No quotient or cardinality oracle is assumed.
Exact non-coprime classes and bounded solution bijections proved; not Stable
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v34 · not Stable.
Campaign connections: Generalized CRT · Euler's theorem · G012
First admitted in Alpha v33
The v33 release added121 results to reach4,092 checked-use entries; those first admissions remain available in Alpha v34. Stable remains the unchanged 432-theorem default. The actual 377-node artifact has fresh original HA and same-byte compiled Lean verification, with eight independently replayed ordinary HA principal certificates.
General Euclidean execution, its coefficient identity, remainder-degree bound and execution uniqueness are proved. The separate shift/scalar → associativity → gcd/Bézout campaign is now proved; full G091 remains open. Neither raw beta-code equality nor equality of evaluations replaces formal coefficient equivalence.
G091: division and normalized gcd/Bézout accomplished; finite fields next
Alpha v34 checked use · 121 independently proved theorems
Construct actual triangular quotient executions for every canonical nonzero divisor, form the residual, trim its leading zeros and prove the coefficient identity and strict remainder bound. Decoded execution uniqueness and formal coefficient equivalence handle different beta encodings and representation lengths.
Seven conservative definitions organize quotient steps, execution, left padding and formal equivalence. Addition, subtraction and convolution respect representation equivalence, including empty and leading-zero cases.
General division proved · normalized gcd/Bézout is now proved in its separate chapter; not Stable
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v33 · not Stable.
Uniqueness concerns actual executions on the same annotated input; arbitrary formal-identity quotient/remainder uniqueness is a later theorem. No degree is assigned to the zero polynomial.
Campaign connections: Division prerequisites · Convolution and degree · G091
First admitted in Alpha v32
The v32 release added 90 multiplicative-convolution results and 85 polynomial-division prerequisites to its 3,796-entry v31 parent. These 175 first admissions remain checked use in Alpha v34. Stable remains the separate, unchanged 432-theorem default library.
G009 is closed for its finite signed arithmetic-table contract, including multiplicative closure. G091 remains open: polynomial division prerequisites do not construct every prime-power field. Current membership, first admission, historical proof evidence and still-open goals are distinct.
G009: completed finite signed Dirichlet theory · G091: polynomial prerequisites and the open field construction
Alpha v34 checked use · 90 independently proved theorems
Construct actual coprime divisor pairs, finite Cartesian sums and support-sensitive reindexing, then prove that convolution preserves multiplicativity on nonempty finite signed prefixes. Normalization is F(1)=+1, signed code 2, not an arbitrary signed unit. Coprime products must lie in the inclusive prefix; zeroth values remain unrestricted.
G009 complete · independently kernel and Lean verified; not Stable
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v32 · not Stable.
The inherited convolution, associativity, delta and inverse theorems retain their original first-admission evidence.
Campaign connections: G009
Alpha v34 checked use · 85 independently proved theorems
Follow 26 coefficient negation/subtraction results, 22 actual leading-zero trimming results, 20 monic-normalization results and 17 Horner/synthetic-division results. Highest-degree-first beta prefixes carry explicit lengths; uniqueness compares decoded coefficients, not code numbers. Synthetic executions have actual quotient traces, coefficient laws and evaluation remainders.
G091 prerequisites proved · full G091 remains open; not Stable
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v32 · not Stable.
General polynomial division remains admitted in polynomial-euclidean-division. The new polynomial-gcd-bezout family proves shift/scalar laws, associativity, recursive normalized gcd/Bézout existence, greatestness and formal uniqueness. Irreducible-polynomial existence in every positive degree and general prime-power fields remain open. The zero polynomial has no represented natural-number degree.
Campaign connections: G091
Completed lower-layer constructions
Euler’s theorem for units, prime-order fields, finite signed sums, polynomial data, Dirichlet convolution and full finite Möbius inversion were first admitted in Alpha v31 and remain checked use in Alpha v34. All 19 complete dependency bundles passed the original HA kernel and the independently compiled Lean checker; all 52 principal ordinary certificates were checked separately.
Alpha v34 has 4,223 checked-use entries. Stable remains the separate, unchanged 432-theorem library. General finite signed Dirichlet inverse existence is proved. Full finite signed G009 is now closed, including multiplicative closure; general prime-power fields in G091 remain open. Historical checkpoint receipts and first-admission records retain their original meaning.
G007: complete finite Möbius inversion · G009: complete finite signed convolution and multiplicative closure
Alpha v34 checked use · 32 independently proved theorems
The exact G014 theorem covers m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem handles m=1 by congruence, not by asserting that one is a canonical remainder. Multiplicative-order and RSA statements are not claimed.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G014
Alpha v34 checked use · 87 independently proved theorems
This checkpoint constructs prime-order fields (k=1), with genuine finite arithmetic tables, cardinality, and characteristic. Inversion is proved only for nonzero elements; the table's zero entry is a zero-to-zero convention. G091 for every prime power p^k, with an irreducible polynomial of degree k, remains open. No extension-field construction or G091 closure is claimed.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G091
Alpha v34 checked use · 21 independently proved theorems
Mobius(n,z) is positive-domain only, independently defined from squarefreeness and actual prime-factor parity. Signed codes 0, 2 and 1 represent zero, +1 and -1. This family proves values and prime-adjunction laws; the separate Möbius-inversion family supplies the complete G007 endpoint.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 30 independently proved theorems
These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 37 independently proved theorems
A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 40 independently proved theorems
Operation tables contain actual beta-coded entries and compare represented signed values, not encodings. The strict sum window is i<l and the separately certified endpoint i=l is unused. Rectangular Fubini and full finite signed Möbius inversion are separate, now-admitted families.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 49 independently proved theorems
Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G091
Alpha v34 checked use · 12 independently proved theorems
The complementary quotient is witnessed by n=d*q at positive divisors. The actual permutation covers indices zero through n, fixing zero and nondivisors. This is the involution foundation for the separate cancellation and full G007 inversion proofs, not an assumed divisor bijection.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 28 independently proved theorems
The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 32 independently proved theorems
Every slice, row table, column table and signed sum is an actual beta-coded witness. Entries are F((o+s*i)+t*j), for i<m and j<n. Zero dimensions and zero strides are allowed; separately certified endpoints are unused. Table uniqueness concerns values, not codes. No infinite-sum assertion is made.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 53 independently proved theorems
Coefficients are highest-degree-first and every representation carries its explicit length. Empty inputs give an empty product; zero extension does not constrain unrelated beta entries past the prefix. Represented degree requires a decoded nonzero leading coefficient and does not assign a degree to zero. This checkpoint claims coefficient convolution and degree addition, not polynomial division, gcd, irreducible search, an evaluation-product identity, or general prime-power extension fields; full G091 remains open.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G091
Alpha v34 checked use · 8 independently proved theorems
The zero window is half-open and its order hypothesis is essential. All folds retain actual beta-coded traces. These are support lemmas for the separately verified full inversion endpoint.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 40 independently proved theorems
Each retained summand has a witnessed n=d*q and actual signed multiplication. Zero and nondivisors contribute zero. Input and output values at zero are unrestricted; uniqueness is for positive represented values. The separate inverse family proves the unit-at-one criterion. The separately admitted multiplicative-convolution family completes finite signed G009.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G009
Alpha v34 checked use · 32 independently proved theorems
Every grid, slice, row sum and intermediate table is constructed. Retained cells have witnessed n=(a*e)*c and value F(a)*(H(e)*G(c)). The flat endpoint is unused. Table associativity includes N=0 and compares only positive values, not encodings. Together with the separately admitted multiplicative-convolution family, the finite signed G009 contract is complete.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Alpha v34 checked use · 25 independently proved theorems
Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; the new multiplicative-convolution family supplies the remaining finite signed G009 closure.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Alpha v34 checked use · 8 independently proved theorems
The full finite signed G007 theorem includes the reverse equivalence and actual witnesses at N=0. The divisor-transform premise covers every required positive quotient. F(0), G(0) and H(0) are unrestricted; only the historical Möbius witness retains its separate zero convention. Finite signed G009, including multiplicative closure, is now proved; general G091 prime-power fields remain open.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G007
Alpha v34 checked use · 9 independently proved theorems
Canonical signed +1 is code 2 and -1 is code 1. The two-case unit graph does not assume an inverse or cancellation law: its actual product characterization and affine existence and uniqueness are proved. These scalar lemmas support the separately checked finite inverse criterion; the separately admitted multiplicative-convolution family completes finite signed G009.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G009
Alpha v34 checked use · 10 independently proved theorems
The strict remainder is an actual inclusive prefix through k with an S k-entry fold; the future input at S k is excluded. A genuine table extension supplies the endpoint. The at-one identity inspects or constructs the real two-entry masked sum. No recurrence, inverse, or omitted summand value is assumed as a conclusion-bearing premise.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G009
Alpha v34 checked use · 21 independently proved theorems
For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative closure on nonempty normalized prefixes is proved in its separate family, completing finite signed G009.
Explore the proof mapOriginal HA and compiled Lean verification · first admitted v31 · not Stable.
Campaign connections: G009
The complete constructive research atlas
Explore twelve mathematical families, sixteen shared tools, eight proof anchors, 407 reviewed conservative definitions with 884 actual expansion arrows, and 13,816 theorem dependencies. The 120 major goals remain organized by prerequisites and mathematical scale. Alpha v34 has 4,223 checked-use entries: 432 unchanged Stable theorems and 3,791 additional Alpha-closed theorems. The 131 first admissions in v34 extend the 4,092-entry v33 parent without rewriting historical evidence. Definition arrows, proof dependencies and still-open research goals remain distinct.
Choose a mathematical scale: start with the complete landscape, open a research family, then select a milestone to follow its actual prerequisites, conservative definitions, checked proof, or still-open frontier.
Research families: congruences · prime distribution · binomial and p-adic arithmetic · reciprocity · sums of squares · Diophantine equations · certified algorithms · matrices and lattices.
Completed first-wave milestones: complete positive primitive Pythagorean classification · the unconditional Fermat fourth-power theorem. The preserved Alpha-v26 58-theorem tranche constructs the actual inverse parametrization and strictly decreasing counterexample witnesses.
Previously completed milestones: infinitely many primes 3 modulo 4 · logarithmic Euclidean GCD · complete logarithmic binary modular exponentiation.
Seven completed second-wave targets: arbitrary-dimensional determinants, rectangular rank, and integer column spans · simple-root Hensel lifting at every positive prime power · complete finite pairwise-compatible generalized CRT · multinomial Kummer · effective Chebyshev prime-count bounds · Cauchy–Davenport · Cornacchia for prime sums of two squares. These 422 new theorems have complete original-kernel and independent Lean verification.
New lower-layer endpoints: unique division · canonical signed Bézout · coprime cancellation · actual prime factor lists · unordered factorization with a witnessed permutation · prime unboundedness · the first primes and an effective bound · Gaussian Euclidean division · Eisenstein Euclidean division. Four established arithmetic interfaces and prime unboundedness are now explicitly indexed; the factorization witness and both ring constructions expose their exact algorithms.
Five newly completed priorities: convergent best approximation · Euler’s totient product · squarefree kernels and perfect powers · odd-prime exponent lifting · Gaussian unique prime factorization. Their complete dependency closures are independently checked by both the original HA kernel and Lean.
Where the programme goes next: Jacobi-symbol reciprocity · cubic reciprocity · three squares. These are research targets, not claims of completed proofs.
Download the complete 557-node quadratic-reciprocity proof certificate · Read its verification receipt
Download the complete 438-node supplementary-laws proof certificate · Read its Python-kernel and Lean verification receipt
Lucas: complete 213-node constructive proof certificate · Verification receipt
Kummer: complete 281-node constructive proof certificate · Verification receipt
Bertrand: complete 544-node constructive proof certificate · Verification receipt
Four squares: complete 390-node constructive proof certificate · Verification receipt
Two squares: complete 517-node constructive proof certificate · Verification receipt
Complete legacy closure: 475-node constructive proof certificate · Verification receipt
New constructive campaigns: 545-node proof certificate · Verification receipt
Four next-layer campaigns: complete kernel- and Lean-verified 590-node proof certificate · Original-kernel verification receipt
Matrices and certified algorithms: compact kernel- and Lean-verified 209-node proof certificate · Original-kernel and independent Lean verification receipt
Binary length and certified algorithm execution: complete kernel- and Lean-verified 240-node proof certificate · Original-kernel and independent Lean verification receipt
Three complete constructive milestones: kernel- and Lean-verified 617-node proof certificate · Original-kernel and independent Lean verification receipt
Arbitrary signed minors, formal derivatives, and finite CRT: kernel- and Lean-verified 203-node proof certificate · Original-kernel and independent Lean verification receipt
Complete cofactor families, actual Hensel lifts, and non-coprime CRT: kernel- and Lean-verified 302-node proof certificate · Original-kernel and independent Lean verification receipt
Complete primitive Pythagorean classification and unconditional Fermat four: kernel- and Lean-verified 216-node proof certificate · Original-kernel and independent Lean verification receipt
Seven complete second-wave campaigns: kernel- and Lean-verified 1,224-node proof certificate · Original-kernel and independent Lean verification receipt
Arithmetic, prime enumeration, and quadratic integer division: complete kernel- and Lean-verified 862-node proof certificate · Exact lower-layer verification receipt and scope boundaries
Best approximation, totient products, squarefree kernels, and odd-prime LTE: complete 566-node proof certificate · Exact priority-layer HA and Lean verification receipt
Gaussian prime factorization with witnessed uniqueness: complete 453-node proof certificate · Exact Gaussian-factorization HA and Lean verification receipt
Constructive research frontier
The following interactive maps switch between byte-exact first-order formulas and reviewed, linked mathematical definitions with checked AST-equivalence receipts. Together with the original quadratic-reciprocity and Bertrand anchors, these 44 established proof families preserve the same canonical reading surfaces. Inspect tactic scripts, dependency neighborhoods, printable maps, and constructive numerical examples. The current Alpha library retains every earlier first-admission record and connects the completed priority goals to arithmetic foundations, finite prime support, continued fractions, valuations, and actual Gaussian Euclidean division. The two quadratic rings share one canonical signed-pair carrier and addition, with separately defined multiplication and norms. Edition labels preserve each theorem’s historical first enrollment; proved components never imply stronger unproved results.
Evidence is stated separately for every family: Alpha-closed checked use never implies Stable membership; body-only candidates have no checked-use authority.
Alpha v34 checked use · 83 independently proved theorems
Build the actual quotient-matrix convergents and prove the second-kind bound against every strictly smaller positive denominator, including signed competitor numerators.
G072 complete · independently kernel and Lean verified; not Stable
Explore the proof mapThe genuine initial 0/1 and exact terminal convergent are included. Approximation is a conclusion, not a premise hidden inside the definition.
Alpha v34 checked use · 84 independently proved theorems
Count actual coprime residue bits, prove multiplicativity and prime-power counts, then identify the count with the independently defined finite Euler product over complete distinct prime support.
G006 complete · independently kernel and Lean verified; not Stable
Explore the proof mapFor every positive n, the proof constructs the factorization and product witnesses. The empty product gives φ(1)=1; zero is excluded.
Alpha v34 checked use · 53 independently proved theorems
Construct the unique positive decomposition n=r·s² with squarefree r, and an actual encoded perfect-power profile classifying every positive root degree by the gcd of the prime exponents.
G010 complete · independently kernel and Lean verified; not Stable
Explore the proof mapA separate uniform unit case handles n=1. The root table contains actual witnesses; this is not the unrelated polynomial squarefree-decomposition predicate.
Alpha v34 checked use · 38 independently proved theorems
Prove the prime step, coprime-exponent step, and full formula vₚ(xⁿ−yⁿ)=vₚ(x−y)+vₚ(n) from actual power and valuation witnesses.
G036 complete · independently kernel and Lean verified; not Stable
Explore the proof mapThe exact guards remain: odd prime p, x>y>0, n>0, p divides x−y and does not divide xy. The p=2 variant is a separate target.
Alpha v34 checked use · 180 independently proved theorems
From actual Gaussian Euclidean division, develop gcd and Bézout, finite norm-bounded factor search, prime-factor existence, and uniqueness with a constructed bounded bijection and an actual unit at each match.
G082 complete · independently kernel and Lean verified; not Stable
Explore the proof mapEvery nonzero Gaussian integer is covered, including units and repeated factors. Sorted primary representatives and prime classification are not claimed.
Alpha v34 checked use · 20 independently proved theorems
Construct complete distinct prime support with actual valuations, factor powers, and unit cofactors. Follow the shared finite data used by totient products, squarefree kernels and exponent lifting.
T09 shared tools · independently kernel and Lean verified; not Stable
Explore the proof mapThis is shared foundational machinery, not an additional major-goal claim. The definitions expand back to the exact original arithmetic formulas.
Alpha v34 checked use · 27 independently proved theorems
Unique quotient and remainder, canonical signed Bézout including (0,0), coprime cancellation, and actual prime factor lists. Construct a bounded, injective, surjective index map between arbitrary unordered factorizations, including repeated prime occurrences.
G001–G005 exact endpoints · independently kernel and Lean verified; not Stable
Explore the arithmetic foundation mapNo sorting or supplied canonicalization is assumed. The empty prime factor list represents one.
Factorization family · Closed witnessed-permutation milestone G005
Alpha v34 checked use · 19 independently proved theorems
Construct the globally least prime above any input, build the actual first k primes, prove strict increase and no omission, and obtain the witnessed bound pₖ < 2^(2^k) for every k > 0.
G021 and G022 exact endpoints · independently kernel and Lean verified; not Stable
Explore the first-primes proof mapThis is not a sparse Bertrand chain. Both power witnesses and the complete prime list are constructed.
Prime-distribution family · Closed effective-bound milestone G022
Alpha v34 checked use · 93 independently proved theorems
For every a,b in ℤ[i] with b ≠ 0, construct canonical q,r with a=bq+r and N(r)<N(b). Follow genuine signed floor division, nearest square-lattice rounding, and the proved multiplicative norm a²+b².
G081 complete · independently kernel and Lean verified; not Stable
Explore the Gaussian proof mapThe shared integer carrier and every norm witness are explicit. Gcd and unique factorization are proved in the new Gaussian factorization chapter; prime classification remains separate.
Quadratic integer rings · Closed Gaussian division milestone G081
Alpha v34 checked use · 65 independently proved theorems
For every a,b in ℤ[ω] with b ≠ 0, construct canonical q,r with a=bq+r and N(r)<N(b). The same signed-pair carrier supports ω²+ω+1=0 and the separately proved multiplicative norm a²−ab+b².
G084 complete · independently kernel and Lean verified; not Stable
Explore the Eisenstein proof mapA fundamental-parallelogram floor quotient gives strict decrease; global nearest-point optimality is not asserted. Eisenstein factorization and prime classification remain open.
Quadratic integer rings · Closed Eisenstein division milestone G084
Alpha v34 checked use · 182 independently proved theorems
Construct actual arbitrary-dimensional recursive determinants, unique rectangular ranks from genuine nonzero minors, and integer column-span witnesses closed under zero, addition, and negation. Equivalent signed representatives give the same determinant and rank.
T13 finite substrate complete · independently kernel and Lean verified; not Stable
Explore the integer linear-algebra proof mapSquare matrices with positive absolute-determinant data have full rank. Lattice index equals determinant, determinant multiplicativity, Smith and Hermite normal forms, and lattice reduction are not claimed.
Matrices and lattices family · Closed finite-tool milestone T13
Alpha v34 checked use · 40 independently proved theorems
For actual signed integer polynomials, construct the derivative inverse from nonvanishing modulo a prime and obtain the unique canonical root lift at every positive prime-power precision.
G095 complete · independently kernel and Lean verified; not Stable
Explore the prime-power lifting proof mapArbitrary natural root representatives are included. Singular roots and p-adic completion are separate targets.
Alpha v34 checked use · 24 independently proved theorems
Prove that pairwise gcd compatibility is exactly simultaneous solvability for arbitrary finite congruence lists, construct the full LCM solution class, and prove unique normalized representatives.
G011 complete · independently kernel and Lean verified; not Stable
Explore the complete generalized-CRT proof mapEmpty lists and zero moduli are included; a zero LCM uses exact equality, not an impossible bound below zero.
Alpha v34 checked use · 19 independently proved theorems
Construct arbitrary finite multinomial coefficients and identify their exact prime valuations with the total actual column carries in successive addition of the parts.
G035 complete · independently kernel and Lean verified; not Stable
Explore the multinomial carry proof mapEmpty lists and zero parts are included. The carry relation is built from quotient columns and carry bits, independently of the valuation conclusion.
Binomial and p-adic arithmetic family · Closed milestone G035
Alpha v34 checked use · 55 independently proved theorems
Count every prime through N with complete finite prime masks and prove the explicit integer bounds N ≤ 8kℓ and kℓ ≤ 8N for every N ≥ 2, where k counts the primes through N and ℓ is the binary length of N.
G027 complete · independently kernel and Lean verified; not Stable
Explore the effective prime-count proof mapThe constants are explicit; no prime number theorem, real logarithms, or asymptotic oracle is assumed.
Alpha v34 checked use · 30 independently proved theorems
Construct a square root of −1 modulo each prime p ≡ 1 (mod 4), follow a genuine Euclidean quotient/remainder trace, and prove that its first square-bounded stopping point yields p = R² + T².
G107 complete · independently kernel and Lean verified; not Stable
Explore the certified Cornacchia proof mapThe representation is proved from the execution, not assumed in its definition. This is not a general x² + d y² solver.
Alpha v34 checked use · 72 independently proved theorems
Construct actual finite prime-field sets and sumsets, then prove |A + B| ≥ min(p, |A| + |B| − 1) for nonempty A and B using a witnessed cardinality-preserving transform and strict descent.
G051 complete · independently kernel and Lean verified; not Stable
Explore the additive-combinatorics proof mapComplete characteristic-bit codes carry the actual cardinalities; no finite-choice oracle or supplied sumset bound is assumed.
Alpha v34 checked use · 29 independently proved theorems
Construct every genuine signed first-row minor of an arbitrary-dimensional matrix in one beta-coded family, then prove exact parity-adjusted alternating Laplace folds and their unique signed components.
Historical genuine minor families and alternating folds; arbitrary-dimensional determinants, rank, and integer spans are now proved in the second wave
Explore the complete cofactor-family proof mapClosed finite-tool milestone T13 · Reviewed first-row cofactor-fold definition
Alpha v34 checked use · 19 independently proved theorems
Produce actual quadratic Taylor-remainder witnesses for arbitrary beta-coded polynomials, compute the unique bounded modular derivative correction, and perform a genuine one-step simple-root divisibility lift.
Historical exact Taylor remainder and one-step lift; complete simple-root prime-power lifting is now proved in the second wave
Explore the genuine Hensel-lifting proof mapClosed full Hensel milestone G095 · Reviewed exact Taylor-remainder definition
Alpha v34 checked use · 24 independently proved theorems
Solve every genuinely non-coprime finite congruence system satisfying exact successive-LCM/gcd merge compatibility and construct its unique canonical solution below the actual modulus-list LCM.
Historical merge-compatible and dominating-last cases; arbitrary finite pairwise-compatible CRT is now proved in the second wave
Explore the non-coprime CRT proof mapClosed generalized CRT milestone G011 · Reviewed exact merge-compatibility definition
Alpha v34 checked use · 17 independently proved theorems
Delete arbitrary rows and columns from arbitrary-dimensional signed beta-coded matrices, construct the exact cofactor minor, and verify genuinely signed four-by-four determinants.
Historical arbitrary signed minors and signed 4×4 determinants; unrestricted recursive determinants and rank are now proved in the second wave
Explore the signed-minor proof mapClosed finite-tool milestone T13 and its historical components · Reviewed signed-minor definition
Alpha v34 checked use · 15 independently proved theorems
Follow coupled beta-coded Horner traces computing every finite polynomial and its exact formal derivative, including the genuine successor rule and unique simultaneous output.
Historical unique polynomial value and derivative; complete simple-root prime-power lifting is now proved in the second wave
Explore the formal-derivative proof mapClosed Hensel-lifting milestone G095 · Reviewed formal-derivative definition
Alpha v34 checked use · 27 independently proved theorems
Construct the unique universal-property LCM even for non-coprime or zero moduli, then prove the exact bounded canonical solution for every finite positive pairwise-coprime congruence system.
Historical pairwise-coprime CRT and arbitrary-list LCM; complete compatible non-coprime CRT is now proved in the second wave
Explore the finite-CRT proof mapClosed generalized CRT milestone G011 · Reviewed universal-property LCM definition
Alpha v34 checked use · 17 independently proved theorems
Follow genuine beta-coded Euclidean division histories to their certified terminal gcd, then derive the exact constructive logarithmic step bound from binary length and two-step remainder halving.
Complete G101: actual terminal gcd and steps ≤ 2 · BitLen(b) + 1
Explore the complete Euclidean proofClosed milestone G101 · Exact logarithmic-execution definition
Alpha v34 checked use · 24 independently proved theorems
Construct the canonical beta-coded binary digits of every exponent, execute genuine modular square-and-multiply transitions, and prove that their unique terminal result is the exact modular power.
Complete G102: arbitrary exponents and operations ≤ 3 · BitLen(e) + 2
Explore the complete binary proofAlpha v34 checked use · 18 independently proved theorems
Build a genuine constructive Euclid witness, extract a prime divisor congruent to 3 modulo 4, and prove that it exceeds any prescribed natural bound.
Complete G025: ∀ n, ∃ p > n, Prime(p) ∧ p ≡ 3 (mod 4)
Explore the complete prime proofAlpha v34 checked use · first closed v17 · enrolled v15
Inspect both constructive laws for the quadratic characters of −1 and 2, with explicit modulo-four and modulo-eight witnesses.
Alpha v30 checked-use · independently kernel and Lean verified; not Stable
Explore Alpha proof mapAlpha v34 checked use · first enrolled v14
Follow the exact constructive identification of a binomial valuation with its base-p addition carries.
Alpha v30 checked-use · independently kernel and Lean verified; not Stable
Explore Alpha proof mapAlpha v34 checked use · exact prime iff added v19
Explore the complete all-natural two-square criterion, including explicit witnesses, even prime valuations, constructive descent, and the zero boundary.
Alpha v30 checked-use · independently kernel and Lean verified; not Stable
Explore Alpha proof mapAlpha v34 checked use · first enrolled v13
Explore the complete proof that every natural number is a sum of four squares, including bounded prime seeds, both quaternion identities, all signed cases, and constructive descent.
Alpha v30 checked-use · independently kernel and Lean verified; not Stable
Explore Alpha proof mapAlpha v34 checked use · first enrolled v13
Explore the complete unconditional digitwise binomial congruence, terminating beta-coded expansions, exact prime-block recurrences, and constructive product witnesses.
Alpha v30 checked-use · independently kernel and Lean verified; not Stable
Explore Alpha proof mapAlpha v34 checked use · 102 independently proved theorems
Read both orientations of the complete positive primitive Pythagorean classification, follow the actual strictly decreasing counterexample construction, and inspect the unconditional fourth-power theorem with every natural zero-coordinate boundary included.
G077 and G078 complete · independently kernel and Lean verified; not Stable
Explore the complete proof map44 historical foundations and 58 new square-factor, inverse-parametrization, and descent theorems retain their exact first-admission evidence.
Primitive classification · Actual strict descent · Positive fourth-power sums are never squares · Complete natural solution classification
Diophantine family · Closed forward-construction anchor · Closed classification milestone G077 · Closed Fermat milestone G078
Alpha v34 checked use · 7 independently proved theorems
Follow finite beta-coded coefficient lists through constructive Horner traces, existence, uniqueness, the empty polynomial, and exact successor decomposition.
Complete natural-coefficient evaluation; arbitrary rings remain downstream
Explore Alpha proof mapClosed foundational milestone T12 · Inspect its shared definition
Alpha v34 checked use · 10 proved foundation theorems
Inspect beta-coded matrix cells, finite dot-product existence and uniqueness, commutativity, and witnessed signed two-by-two determinants.
Historical matrix components; arbitrary signed multiplication is now proved in the advanced matrix campaign
Explore checked component mapClosed finite-tool milestone T13 and its historical components
Alpha v34 checked use · 13 independently proved theorems
Strengthen Bertrand’s theorem to central-binomial prime divisors of exact valuation one and construct arbitrary finite chains of strict prime-window witnesses.
Both exact strengthened prime milestones independently kernel checked
Explore Alpha proof mapClosed valuation milestone G023 · Closed chain milestone G024
Alpha v34 checked use · 9 independently proved theorems
Construct genuine quotient lists and beta-coded execution histories from positive rational inputs using exact Euclidean division and strict terminating descent.
Complete positive-input finite expansion; no unbounded search oracle
Explore Alpha proof mapDiophantine approximation family · Closed foundational milestone G071
Alpha v34 checked use · 23 independently proved theorems
Multiply arbitrary finite natural and signed matrices, construct unique signed dot products, and inspect exact genuinely signed two- and three-dimensional determinant witnesses.
Historical arbitrary signed multiplication; arbitrary-dimensional determinants, rank, and integer column spans are now proved in the second wave
Explore the signed matrix proof mapClosed finite-tool milestone T13 · Shared signed-matrix definition
Alpha v34 checked use · 15 independently proved theorems
Inspect complete beta-coded Euclidean histories, independently witnessed relational gcds, linear termination bounds, and the genuine strict two-step halving lemma.
Historical checked histories and halving; terminal identification and the complete G101 logarithmic bound are proved in subsequent campaigns
Explore the Euclidean proof mapClosed complexity milestone G101 · Two-step halving definition
Alpha v34 checked use · 16 independently proved theorems
Follow binary exponent splitting, doubled and odd power identities, checked modular square-and-multiply steps, and the uniquely bounded modular-power output.
Historical verified step proofs and executable certificates; the complete formal G102 BitLen execution bound is proved in Alpha v23
Explore the repeated-squaring proof mapClosed algorithm milestone G102 · Shared modular-power definition
Alpha v34 checked use · 21 independently proved theorems
Prove totality and uniqueness of the genuine first-order BitLen relation, exact binary digit decomposition, strict powers of two, and the correct zero-length convention.
Full unique BitLen existence independently kernel- and Lean-verified; no host arithmetic oracle
Explore the binary-length proof mapReviewed first-order BitLen definition · Shared Euclidean complexity substrate
Alpha v34 checked use · 20 independently proved theorems
Transport divisibility and greatest-common-divisor invariants through every genuine beta-coded Euclidean division, then prove that the actual terminal state equals the certified gcd.
Historical terminal-state/gcd identification and linear termination; Alpha v23 also proves the complete G101 logarithmic bound
Explore the terminal-gcd proof mapComplete checked G101 complexity milestone · Anchored execution definition
Alpha v34 checked use · 19 independently proved theorems
Construct real beta-coded square-and-multiply accumulator histories, prove their exact base-two Horner/modular-power invariant, and identify the unique terminal result.
Historical supplied-digit execution; Alpha v23 also constructs arbitrary-exponent canonical digits and proves the complete G102 logarithmic bound
Explore the coded execution proof mapComplete checked G102 algorithm milestone · Shared execution-trace definition
What you can inspect
Each explorer is a static, reproducible reading surface generated from exact theorem specifications. Every definition expands conservatively into the original first-order language: definition-to-definition arrows describe notation, while theorem-to-theorem arrows certify actual proof prerequisites. Search by theorem, open its definition-aware neighborhood, inspect the exact proof line by line, then zoom back out to its research family and the complete campaign.
The current library contains 68 proof families. Earlier non-admitting research snapshots remain available as dated evidence, not as the current admission catalogue: the 170-proof checkpoint and the 126-proof checkpoint.
Current v34 public-delivery inventory · V34 verification record. Delivery metadata and saved records do not grant proof or admission authority.
Historical v33 public-delivery inventory · V33 verification record. Delivery metadata and stored records do not themselves grant proof or admission authority.
Historical v32 public-delivery inventory · V32 verification record. Delivery metadata and stored records do not themselves grant proof or admission authority.
Exact public-delivery inventory · Fresh v31 verification record