Bertrand’s postulate campaign

Bertrand’s postulate campaign#

This campaign aims to prove Bertrand’s postulate completely inside the unchanged intuitionistic arithmetic kernel. Its primary endpoint is

\[ \forall n\ne0\;\exists p\, \bigl(\operatorname{Prime}(p)\land n<p\land p\le 2n\bigr), \]

followed by the traditional strict corollary for \(1<n\):

\[ \exists p\, \bigl(\operatorname{Prime}(p)\land n<p<2n\bigr). \]

Current evidence boundary

Bertrand’s postulate is fully proved in the repository. The focused BP01 and BP02 audits kernel-check empty-context certificates for bertrand_closed_upper and bertrand_strict. Current Alpha v12 preserves the sealed 1,123-row Alpha-v11 parent and enrolls the complete 180-row dependency closure in nine exact twenty-row microbatches. Enrollment remains deliberately conservative: every v12 suffix row is body_checked, has no checked-use permission, and is unavailable through edition replay until a later promotion.

The binding statement, logic, validation, and release rules are frozen in RFC HA-R6-BERTRAND-1. Its threshold representation is amended by RFC HA-R6-BERTRAND-2: the mathematical cutoff 512 has canonical native carrier 16 * 32, public Bertrand surfaces retain n + n, and any move to an internal 2 * n helper requires a live checked equality rewrite. The amendment changes no endpoint, logical authority, or evidence status. The additive Choose/central-binomial tranche is separately bound by RFC HA-R6-BERTRAND-CB-1. The Alpha-v9 Primorial append is bound per source by the foundation RFC and membership RFC. The Alpha-v10 split append is bound by the interval-split RFC. The Alpha-v11 append is bound by the duplicate-free, Primorial/Choose interval, central-binomial upper, Primorial-four-power, and central-prime-support RFCs. The Alpha-v12 append is bound by the B6 release RFC and the seventeen B5, B7, B8, BP01, and BP02 tranche RFCs in the same research directory. It selects an integer-only Erdős–Tochiori central-binomial proof. No real numbers, logarithms, primitive binomial operation, classical axiom, or new kernel rule is permitted.

Open the complete interactive Bertrand proof map Read the final strict theorem · BT0127

The complete Bertrand proof explorer contains all 544 theorem nodes and 1,917 direct edges in the transitive closure of bertrand_strict.

Why the proof remains constructive#

The finite interval is decided before the contradiction argument begins:

bounded_prime_interval_search(l,u)
  |
  |-- witness p with Prime(p), l<p, p<=u  ---> return p
  `-- pointwise certificate excluding every such p
                                                |
                                                `-- refute by integer bounds
                                                    and use false.elim

Consequently, the negative branch is explicit data. The proof never turns \(\neg\neg\exists p\) into \(\exists p\).

Current Alpha v12 layer#

Alpha v12 is an additive child of the sealed 1,123-row Alpha v11 ledger. Alpha v8 remains the sealed Choose/central-binomial parent, v9 the sealed Primorial foundation and membership parent, v10 the sealed interval-split parent, and v11 the sealed B4-capstone/B5-support parent.

Quantity	Exact value
Alpha v12 specifications	1,303
Stable rows	432
Alpha-only rows	871
checked-use rows	570
direct dependency edges	4,302
dependency layers	45
first-round Bertrand rows	21
Round-2 Bertrand rows	42
`FactorialVal` rows	7
Alpha-v6 threshold / finite-sum / power / valuation rows	8 + 5 + 5 + 3
Alpha-v7 constructor / successor / total-power / base / recurrence / transport / equality rows	3 + 5 + 4 + 2 + 5 + 3 + 2
Alpha-v8 Choose / central baseline and recurrence / bridge / lower-bound rows	24 + 14
Alpha-v9 Primorial foundation / membership and monotonicity rows	10 + 11
Alpha-v10 Product split / Primorial interval rows	1 + 8
Alpha-v11 duplicate-free / Choose interval / central upper / B4 / B5-support rows	10 + 10 + 6 + 7 + 5
Alpha-v12 B6 support plus B5–BP02 completion rows	43 + 137

All 401 campaign additions are body_checked; checked use remains unchanged at 570. The current enrollment root is f763b9fc3717ad76c7e259d67c3beeadfdaca554bbaaeb3ecd2e55329edf937b. The full edition identity is bacd84f2db14bdd20c09b1ac862348fa14bca9c440099c066fc7e1201a192061. The ordered-specification, membership, evidence, and channel-pointer roots are 362da94c3c5e788f296f315b86b5d63534c1567ce00911dbb27227a66ab50e28, 726c6134461dace943f909a0073ca0a6cae95a54ff306f8aeefeb3d9a5151926, de8a6a57b828c2b3893c6fb31f2611d5180f8de4d1002a21a681739616b761b5, and 7ad0c942a2239532696f5d99ee1dc985e13302cf73b4637497b879871d05752c. The deterministic channel pointer is artifacts/peano-library/channels-v12.json; its catalog, metrics, and reduced graph are the matching catalog-v12.json, metrics-v12.json, and dependency-graph-v12.mmd. Their catalog, metrics, reduced-graph, and channel-pointer SHA-256 values are 825909e057492de87ef08208451c3475396ca009179c513457b05b57f7e2f109, 64da675a3144f4bb0875c2e0650064e72d5d3eb613542d217719280addfaacb4, 583d18473200097997fa6b8ef0b57ebef9da95f136555d97b24220f1abb356b8, and 0063b6d25f6f27869b00af0d7a31f53dda22d82e8d9c30779309939b46c60982. The sealed v7 catalog, metrics, reduced graph, and channels SHA-256 values remain 7676fc944b695d02a3aec05b428c012933258cb6cd9b465599318e690e0f6df4, c40f18bda0ec8feb9294cf445d08b51daf868e46b3931daf55bad91413d39e0d, 85a53bd719e227a31d5cff15fc25ff66abaa82d498030f5a918a7c40271abc9e, and fe9c11ec8a622eb759053a42ee6acb7c2bcb1d454fe0dc5fa4b729a07ffbbd30. The v12 evidence partition is exactly 432 stable_closed, 138 alpha_closed, 732 body_checked, and one pending_layered_closure row. No v12 row was promoted.

B0 — constructive interval search#

prime_strictly_above_decidable;
bounded_prime_interval_search;
prime_interval_exclusion_refutes_witness;
bounded_prime_interval_decidable.

The interval orientation is exactly \((l,u]\). The largest local closed certificate in this group has 2,896 structural nodes and depth 78.

B1 — quantitative powers and order#

mul_le_mul;
le_mul_of_one_le_right and le_mul_of_one_le_left;
pow_base_monotone;
one_le_pow;
pow_nonzero_of_one_le;
pow_exponent_monotone.

The largest local closure is pow_exponent_monotone, at 70,898 nodes and depth 89.

B2 — bounded prime-power valuation#

power_divides_decidable and power_divides_zero;
bounded_power_valuation_search and bounded_power_valuation_exists;
power_valuation_exists and power_valuation_functional;
the divisibility and maximality projections;
prime_power_valuation_exists and prime_power_valuation_functional.

The relation chooses the greatest \(e\le a\) for which \(p^e\) divides \(a\). The prime/nonzero wrapper excludes the intentionally degenerate \(p=0,1\) and \(a=0\) cases. The largest local closure is 125,485 nodes and depth 93.

Round 2 adds exponent antitonicity, exact cofactor extraction, prime nondivisibility across products, and the native theorem

\[ v_p(ab)=v_p(a)+v_p(b) \qquad(p\text{ prime},\ a,b\ne0). \]

The complete multiplication certificate has 297,211 nodes, depth 98, and zero DNE; every one of its 39 direct Cuts is independently corrupted and rejected by the focused gate.

Every direct dependency has a removal or Cut-mutation test, every displayed statement has an exact hash, and complete proof traversals find zero DNE. These local closures establish feasibility; the Alpha evidence remains body-only until the versioned two-process cold receipt is accepted.

Factorial valuations (part of binding gate B2)#

Sealed Alpha v5 enrolls seven rows at indices 965–971:

factorial_nonzero;
prime_power_valuation_one_zero;
factorial_valuation_exists and factorial_valuation_functional;
prime_factorial_valuation_zero;
prime_factorial_valuation_succ; and
prime_factorial_valuation_succ_invert.

The expanded FactorialVal(p,n,e) surface asserts that some \(F\) is the factorial of \(n\) and has selected \(p\)-valuation \(e\). The successor theorem is the exact recurrence

\[ v_p((n+1)!)=v_p(n!)+v_p(n+1), \]

stated entirely through relational factorial, power, divisibility, and valuation formulas. Its inverse recovers the valuation of the new factor from valuations of the two successive factorials. The largest local recursive closure has 432,090 nodes at depth 105 and zero DNE. This is feasibility and mutation evidence, not an empty-context Alpha admission: every one of the seven rows has checked_use=false, a null proof tag, and null closure metadata.

Round-2 integer infrastructure#

The following tranches are enrolled in Alpha v4 with body-only evidence.

The valuation bridge proves, under Prime(p) and \(a\ne0\), that the selected canonical exponent satisfies

\[ p^e\mid a\quad\text{and}\quad p^{e+1}\nmid a. \]

Its capstone power_valuation_selected_and_successor_not_divides closes at 7,632 nodes and depth 75. Exact multiplication is supplied by the later Round-2 valuation tranche described above.

The integer-envelope spike proves five reusable facts, culminating in

\[ (s+7)^{12}\le4^{s+5} \Longrightarrow (s+13)^{12}\le4^{s+11}. \]

That guard closes at 213,731 nodes and depth 100. It validates the key six-step mechanism but is not the complete B6 inequality.

The ceiling/square layer proves totality and uniqueness of \(\lceil x/6\rceil\), the exact shift

\[ \left\lceil\frac{(s+6)^2}{6}\right\rceil =\left\lceil\frac{s^2}{6}\right\rceil+2s+6, \]

and constructive totality, uniqueness, and monotonicity of \(\lfloor\sqrt{x}\rfloor\). The quotient-budget bridge then derives from \(2n=3q+r\) the witnesses

\[ q+c=n,\qquad 2n\le6c,\qquad \left\lceil\frac{s^2}{6}\right\rceil\le c, \qquad q+\left\lceil\frac{s^2}{6}\right\rceil\le n. \]

Its largest closure is 2,906 nodes. These facts remove the floor/ceiling representation risk; the remaining B6 risk is the exponential envelope.

Alpha v6 threshold, finite-sum, and bridge layer#

Alpha v6 enrolls the following twenty-one rows, in dependency-topological source order, over the byte-identical 972-row v5 prefix.

The eight-row threshold tranche proves the numeral bounds used by the \(n\ge2048\) split, transports \(64^2\le2n\) through FloorSqrt, derives \(42(s+1)\le s^2\) and \(7(s+1)\le\lceil s^2/6\rceil\) for \(s\ge64\), and packages the linear residue-window bounds for \(64\le s\le69\). Its largest local closure has 2,352 nodes. It was authored in commit f35b8ed and occupies v6 indices 972–979.

The five-row finite Legendre-sum interface supplies prime_power_quotient_prefix_exists, power_quotient_prefix_transport, prime_legendre_sum_exists, legendre_sum_functional, and legendre_sum_zero. A Gödel-β prefix stores the quotients \(\lfloor n/p^i\rfloor\), and the existing finite-sum relation accumulates them. The largest local closure has 124,078 nodes. This interface was pushed in commit 4df44c9, occupies indices 980–984, and does not yet prove Legendre’s equality

\[ v_p(n!)=\sum_{i\ge1}\left\lfloor\frac{n}{p^i}\right\rfloor. \]

The five-row relational-power bridge at indices 985–989 supplies pow_successor_compose, exact \(2^2\) and \(2^7\) witnesses, the bridge \(128^{12}=4^{42}\), and bertrand_guard_base_residue. The three valuation bridge rows at indices 990–992 show that the encoded quotient tail vanishes and connect prime-power divisibility bounds in both directions to the selected valuation exponent. They were authored in commits bb24543 and 2f41a97.

All twenty-one rows were published in Alpha v6 by 5b189f0. Their exact dependency-curried bodies replay in the intuitionistic kernel and mutations fail closed. Each nevertheless has evidence body_checked, checked_use=false, a null proof tag, and null empty-context closure metadata. The local closure measurements above are feasibility evidence and are not empty-context admission.

Alpha v7 recurrence, equality, and \(H/J\) layer#

Alpha v7 enrolls twenty-four rows over the byte-identical v6 prefix. The first three are optimized constructive initial-segment constructors: eisenstein_initial_segment_indicator_choice, eisenstein_initial_segment_prefix_extend, and eisenstein_initial_segment_prefix_exists.

The next five are the Legendre-successor ingredients originally authored in 5b9433a:

division_remainder_successor_cases;
division_successor_quotient_by_bit;
valuation_threshold_bit_decides_power_divides;
power_quotient_prefix_decoded_divrem; and
power_quotient_successor_pointwise_add.

They feed five finite-recurrence rows culminating in prime_legendre_sum_succ, authored in de58034. The recurrence is complete as dependency-curried body evidence.

The four capacity-shared PowTotal rows originally authored in b2035ce are pow_successor_compose_from_total, pow_mul_exp_from_total, pow_exponent_monotone_from_total, and pow_two_seed_bundle_from_total. They support the two-row compact base-window layer in 70c5b16 and the three-row compact six-step transport in 985a773. The final transport theorem is bertrand_hj_six_step_from_total.

Finally, 158d87c proves factorial_legendre_successor_agreement and prime_factorial_valuation_eq_legendre_sum, completing Legendre’s equality with FactorialVal at the body-evidence level. 00e8361 supplies the optimized constructor source needed by the frozen dependency order. All seven source blocks replay, reject their prescribed mutations, contain zero DNE, and remain fail-closed body_checked rows. At that Alpha-v7 checkpoint this was enrollment, not promotion, and Bertrand’s postulate was still open.

Alpha v8 recurrence-defined Choose and central lower bound#

Alpha v8 preserves that complete v7 prefix and appends 38 reviewed rows in two dependency-topological microbatches. The first 24 construct finite Pascal rows with Gödel-\(\beta\) codes, prove their pointwise and table extensionality, and derive relational Choose existence, functionality, zero, self, Pascal, symmetry, and positivity laws together with baseline CentralBinom wrappers. The second 14 add the central zero and successor laws, weighted vertical and factorial bridges, strict arithmetic growth, the exact fourth-row seed, and

\[ 4^n<n\binom{2n}{n}\qquad(4\le n). \]

The exact endpoint is the relational theorem four_pow_lt_mul_central_binom. The tranche is controlled by RFC HA-R6-BERTRAND-CB-1, whose frozen SHA-256 is 4f337990babf85ffaacdc990f0e09a3c1943b8edb20c72ffef675cbb28cde83b. All 38 dependency-curried body receipts replay with combined root fb6e40f2470a9c436f02676ea15b99a389ee7495b4c6cd81212a42a7010b4466. This is still body evidence: every new row rejects checked replay, and no Stable promotion or full campaign theorem follows from enrollment alone.

Alpha v9 Primorial foundation and membership#

Alpha v9 preserves the complete v8 prefix and appends 21 reviewed rows in two dependency-topological microbatches. The first ten freeze the selector and factor-prefix encodings and the inclusive mathematical Primorial Primorial(m,z), then prove factor choice and prefix totality, Primorial existence and functionality, the zero law, successor decomposition, and positivity. The next eleven prove

\[ \operatorname{Prime}(p)\Longrightarrow \bigl(p\mid m\#\iff p\le m\bigr), \]

successor and arbitrary-index divisibility, positive quotients, and weak numeric monotonicity. The two binding RFCs have SHA-256 values c68354c9aaad738581a14ccbe33e7eaa262940bad667d613e84b947454ff1a89 and 4f569e76c68aa486fd1f1415491a5a3d678a75c239aa72ebd707d67fedde0df5. All 21 dependency-curried body receipts replay with combined root 1a9bac74069a495d6ce17b906f46821731d6fad4e97d07e7272cf57da72593ab. This remains body evidence: every new row rejects checked replay, and interval splitting, duplicate-free external-product comparison, and the final Primorial bound remain future B4 work.

Alpha v10 Primorial interval splitting#

Alpha v10 preserves the complete v9 prefix and appends nine reviewed rows in exact 1+8 dependency order. The first row pins only beta_product_prefix_suffix_split from its two-row provider; the unreviewed concat converse remains excluded. The remaining rows define offset selector prefixes and interval Primorial products, prove their totality, functionality, entry transport and shift, restrict a full selector prefix, and conclude

\[ \operatorname{Primorial}(a+l,z)\Longrightarrow \exists x,y\, \bigl(\operatorname{Primorial}(a,x)\land \operatorname{PrimorialInterval}(a,l,y)\land z=xy\bigr). \]

The binding RFC has SHA-256 db7d2d58f0b44d3793673b21496ea7f5d5d2747c75795587f6b1c99b2e80f46e. All nine dependency-curried bodies replay with combined root fdac645cbc070b5a1cdfe71b19e98afe095a183d4cfa0ad4256fa42857ca736c. This remains body evidence: every new row rejects checked replay, and duplicate-free external-product comparison and the final Primorial bound remain future B4 work.

Alpha v11 B4 capstone and B5 prime support#

Alpha v11 preserves the complete v10 prefix and appends thirty-eight reviewed rows in exact 20+18 microbatches. The first microbatch proves duplicate-free prime-product comparison and connects Primorial intervals to factorial and Choose divisibility. The second supplies cap-safe central-binomial upper laws, proves the public bound

\[ \operatorname{Primorial}(n,z)\land \operatorname{Pow}(4,n,q) \Longrightarrow z\le q, \]

and adds the first B5 prime-divisor and valuation-support rows. In particular, under an explicit no-Bertrand certificate, every prime divisor of the central binomial coefficient is constructively confined to the three live ranges used by the eventual five-range factorization.

All thirty-eight rows remain body evidence only. Their source blocks bind to five subordinate RFCs and retain exact focused empty-context receipts, but Alpha enrollment itself grants no checked use and changes no Stable row.

Alpha v12 complete Bertrand proof#

Alpha v12 appends the complete dependency-closed proof chain in nine exact twenty-row microbatches. The first forty-three rows publish the reviewed B6 base-window, all-root, growth, main-inequality, and finite-product-order support. The remaining 137 rows complete B5’s five-range factorization, derive the B7 large-input contradiction, certify and cover the B8 finite range, and close both public endpoints:

bertrand_closed_upper : n != 0 -> exists p, Prime(p) /\ n < p /\ p <= n+n
bertrand_strict       : 1 < n  -> exists p, Prime(p) /\ n < p /\ p <  n+n

The focused BP01 and BP02 suites independently rebuild their complete empty-context graphs and kernel-check the final certificates. Alpha v12 records the same exact source bodies and provenance as body_checked evidence only; it intentionally leaves checked-use and Stable unchanged.

Dependency roadmap#

checked Alpha baseline
  |-- B0 bounded interval decision
  `-- B1 discrete inequality/fold API
        |-- B2 prime-power valuations and Legendre
        |-- B3 Choose/CentralBinom [Alpha v8 body evidence]
        `-- B4 Primorial [Alpha v11 body evidence; bound closed; depends on B3]

B2 + B3 + B4 --------------------> B5 central factor upper bound [complete]
B1 --------------------------------> B6 native main inequality [complete]
B0 + B3 + B5 + B6 ----------------> B7 n >= 512 [complete]
B0 + B7 + certified prime chain ---> B8 endpoints BP01 and BP02 [complete]

The retained Alpha-v8 central lower bound proves \(4^n<n\binom{2n}{n}\) at the body-evidence level. Under an explicit no-prime certificate for \((n,2n]\), valuations and the primorial will give

\[ \binom{2n}{n} \le (2n)^{\lfloor\sqrt{2n}\rfloor} 4^{\lfloor2n/3\rfloor}. \]

The exact natural-number B6 target is

\[ n(2n)^{\lfloor\sqrt{2n}\rfloor} 4^{\lfloor2n/3\rfloor}\le4^n \qquad(n\ge512). \]

The post-v7 candidate work reduces its difficult growth component to six residue classes using

\[ H(s)=(s+1)^{2s+2},\qquad E(s)=\left\lceil\frac{s^2}{6}\right\rceil, \]

and the exact identity \(E(s+6)=E(s)+2s+6\). FloorSqrt, ceiling-by-six, the quotient complement, threshold arithmetic, the relational-power bridge, compact \(H/J\) bases, six-step transport, the all-\(s\) envelope, and bertrand_main_inequality_nat now have reviewed candidate bodies and closure receipts. The post-v7 envelope and main-inequality rows remain outside Alpha v9, however, and cannot feed a checked large-\(n\) contradiction until the B4 primorial bound, B5 no-prime central upper bound, and branch integration are complete.

The implemented candidate lineage uses the RFC-v2 cutoff carrier 16 * 32, mathematically 512, and the root-32 envelope over the six bases \(s=32,\ldots,37\). In particular, bertrand_hj_envelope_thirty_two supplies the factorized large-branch envelope without placing a literal 512 in the public proof surface. The earlier possible \(n\ge2048\) optimization and roots \(64,\ldots,69\) were not selected for this lineage.

Durable checkpoints#

Commit	Content
`10dc017`	multiplicative order and base-power monotonicity
`6739532`	campaign RFC, constructive interval search, power growth
`be5b735`	bounded valuation existence and functionality
`941ad70`	selected valuation and successor nondivisibility
`3ce8a90`	additive, fail-closed Alpha v3 channel
`9efc5cd`	integer-envelope feasibility spike
`d6dac45`	ceiling-by-six and floor-square relation layer
`3cc6994`	constructive floor-square-root totality and monotonicity
`654aab2` / `bdb9cf7`	two-process closure infrastructure and retained Slurm diagnostics
`88d9e92`	exact prime-power valuation multiplication
`139b6ce`	floor/ceiling quotient budget
`e605faa`	additive, fail-closed Alpha v4 channel
`05cb3ff`	seven-row recursive `FactorialVal` proof layer
`f35b8ed`	eight threshold and residue-window base inequalities
`4df44c9`	five-row finite Legendre-sum interface
`85625d6`	additive, fail-closed Alpha v5 channel
`bb24543`	five-row relational-power bridge
`2f41a97`	three-row Legendre-valuation bridge
`5b9433a`	five Legendre-successor bodies, later enrolled in v7
`b2035ce`	four capacity-shared `PowTotal` bodies, later enrolled in v7
`5b189f0`	additive, fail-closed Alpha v6 channel
`70c5b16`	compact two-row \(H/J\) base window
`de58034`	five-row finite Legendre recurrence
`985a773`	compact three-row \(H/J\) six-step transport
`158d87c`	factorial valuation equals the finite Legendre sum
`00e8361`	optimized constructive initial-segment constructors
`874e81e`	additive, fail-closed Alpha v7 channel
`d1cbe16`	all-root \(H/J\) envelope candidate bodies
`8ea03f2`	B6 main-inequality candidate bodies
`d1ad971`	dependency-closed B6 inequality graph audit
`d46e513`–`74dc219`	frozen 38-row Choose/central-binomial tranche
`dfb2673`	frozen ten-row Primorial foundation tranche
`b0bc5de`	frozen eleven-row Primorial membership and monotonicity tranche
`c45d68a`	frozen Product split and eight-row Primorial interval tranche
`5eef9a5`–`7539b44`	dependency-closed B4 comparison, interval, upper, and capstone tranches
`56ecb02`	first five B5 central prime-divisor support rows

All checkpoints are pushed to nasqret/vietnam2026 on agent/new-theorems-tranche-01.

Reproduce the current gates#

make peano-library-alpha-v12-check
make book-bertrand-proof-explorer
make book-bertrand-defined-explorer

The first command validates the Alpha-v12 evidence boundary, including the complete 180-row dependency-closed Bertrand suffix. Its expensive body replay and focused proof suites run in bounded, serial stages so a single Python process cannot retain the campaign’s proof DAGs indefinitely. The second command deterministically regenerates the 544-node interactive proof map from the byte-frozen v12 catalog. The third adds the conservative definition-aware reading edition, with linked campaign notation and the same exact proof dependencies. Successful replay does not upgrade Alpha evidence or promote anything to Stable.