Ctrl+K

The strict-HA number-theory campaign

The strict-HA number-theory campaign#

This campaign develops reusable number theory in the unchanged Peano Lab object language

\[ 0,\quad S,\quad +,\quad \times,\quad = \]

with intuitionistic connectives, quantifiers, and formula-specific induction. Readable names such as Rem, IsGCD, and the proposed signed predicates are conservative notation: every occurrence expands before the ordinary kernel checks a certificate.

The controlling machine manifest is ha-number-theory-campaign.json. It separates three facts which are easy to blur in an informal development:

  • a dependency-curried tactic body may check;

  • its complete empty-context certificate may check while it remains isolated;

  • only an explicit promotion makes it a Stable theorem.

Historical Alpha v2 and current Alpha v16 / Stable status

The tables and dated checkpoints below preserve the campaign’s historical public/private admission boundary. They are not the current library membership ledger. The canonical Alpha edition now contains every reviewed row from this campaign: its strict-HA contribution is 121 Alpha-closed rows, one of which shares an exact QR specification and therefore occupies the earlier QR position. These rows are Alpha checked-use facts, but they are not Stable. The historical additive Alpha v2 edition preserved the sealed 885-row Alpha v1 ledger and appended seventeen K3C rows at indices 885–901. That sealed snapshot has 902 specs, 2,674 direct edges, 45 layers, 470 Alpha-only rows, and 570 checked-use rows. Current Alpha v16 has 1,673 specs and 885 checked-use rows after the independently verified QR-only promotion; Stable remains 432. The authoritative current counts and evidence states are in Alpha and Stable library editions and artifacts/peano-library/channels-v16.json; channels-v2.json remains an immutable historical pointer.

Historical Stable/public boundary#

Layer

Status

Result

Canonical remainder

public

Existence, functionality, the zero-modulus boundary, and unique existence.

Canonical congruence

public

Equality of supplied canonical remainders is equivalent to balanced congruence.

Bounded modular inverse

public

Existence from coprimality, the converse, bounded uniqueness, and the exact iff-with-unique-witness package.

Canonical relational gcd

mixed

The relational gcd core is public. Three canonical packaging rows and five zero/one/swap convenience rows remain closed private candidates.

Universal-property lcm

seven public / ten private

The projections, leastness, symmetry, uniqueness, and both forced-zero constructors are public. The L08 divisibility constructor and nine convenience rows remain private.

Gcd–lcm totality and compatibility

public K4

All nine constructive bridge rows are public: compatible gcd/lcm existence, relational and unique lcm existence, and the product identity.

Canonical signed naturals

closed candidate

The representation is frozen. Seventy-four parity, decoder, code-extensionality, balance-normalization, negation, addition, and multiplication theorems, together with the direct natural-scaling graph, its laws, and the balanced-to-signed Bezout bridge, close from the empty context without division.

Signed coefficients for relational gcd

closed K4 candidate

A separate client returns a relational gcd together with two canonical signed Bezout codes. Its audited dependency path intentionally includes Euclidean division.

Canonical pair/cell coding

15 closed private candidates

Doubled-Cantor constructors, doubled-triangular shell separation, and exact pair injectivity now close constructively. Cell functionality, descending projections, and uniform finite-data infrastructure remain open.

Generalized CRT

23 public / 6 private

The public dependency closure proves the all-modulus criterion, classifies solutions modulo relational LCM, supplies the zero/nonzero canonical boundary, and returns either a solution or a certified obstruction from raw inputs. Six convenience rows retain closed private receipts.

The public registry now has 432 entries. The nine tranche-01 interfaces at positions 384–392 are followed by the exact 16-row K4 admission at positions 393–408 and the exact 23-row M5 admission at positions 409–431. The research catalog has 433 entries, including 409 checked_m20 rows. The campaign manifest records 95 public references, 99 isolated candidates, and 147 exact theorem receipts across 22 candidate modules and 31 focused test paths. Generalized CRT accounts for 29 audited rows: 23 public interfaces and six closed private conveniences. This append-only extension leaves the frozen first-247 model curriculum unchanged.

Why canonical remainder is a relation#

For naturals (m,n,r), write

\[ \operatorname{Rem}(m,n,r) \;:\!\Longleftrightarrow\; \bigl(\exists q,\ n=mq+r\bigr)\land r<m. \]

Neither division nor remainder is added as a term former. Totality therefore has the honest boundary premise (m\ne0):

\[ \forall m,n,\quad m\ne0\to\exists r,\operatorname{Rem}(m,n,r). \]

Functionality requires no extra nonzero premise because an inhabitant of Rem(m,n,r) already contains (r<m), which is impossible when (m=0). Together the two results give a unique-existence interface. Follow the exact expanded statements and tactic recipes in the theorem atlas:

The bridge theorem then states, for supplied canonical remainders (r,s),

\[ a\equiv b\pmod m\quad\Longleftrightarrow\quad r=s. \]

Here congruence is still the subtraction-free balanced relation

\[ \exists u,v,\quad a+mu=b+mv. \]

See the exact bridge.

The modular-inverse package#

For (m\ne0), the public endpoint has the familiar mathematical reading

\[ \operatorname{Coprime}(a,m) \quad\Longleftrightarrow\quad \exists!u<m,\ au\equiv1\pmod m. \]

Its formal proof is deliberately split into reusable directions:

flowchart LR
  R[canonical remainder exists] --> E[coprime gives bounded inverse]
  U[bounded inverses are unique] --> P[unique bounded inverse package]
  E --> P
  C[any inverse implies coprime] --> P

The full endpoint has 9,512 structural proof occurrences, depth 70, 2,538 distinct proof objects, and 126 self-contained Cut nodes. Its certificate DAG SHA-256 is c3ed07e7caef52895001332d066ae9e4ce25167c7a0cd7189f8957c9aa7dc9f3. These are reproducibility receipts, not sources of logical authority.

The next closed layer: canonical gcd#

IsGCD(g,a,b) remains a relation. The new candidate package merely gives it the conventional value interface:

\[ \forall a,b,\ \exists g,\operatorname{IsGCD}(g,a,b), \]
\[ \operatorname{IsGCD}(g,a,b)\land\operatorname{IsGCD}(h,a,b) \to g=h, \]

and their unique-existence packaging. All three certificates check from the empty context without double-negation elimination, but deliberate public admission is a later gate.

Candidate

Nodes

Depth

Cuts

Certificate SHA-256 prefix

canonical_gcd_exists

1,280

47

36

8e3b24c93772

canonical_gcd_functional

708

35

20

7cca97c44c84

canonical_gcd_exists_unique

2,010

48

55

20db8565558e

Signed naturals without negative zero#

The selected HA-K3-SIGNED-1 representation interleaves signs by parity:

\[ \operatorname{enc}(p)=2p, \qquad \operatorname{enc}(-(k+1))=2k+1. \]

Thus (0,1,2,3,4) represent (0,-1,+1,-2,+2). Every natural is a valid code, zero has one code, and the construction is independent of division, CRT, Gödel-β coding, and the future pair/list codec.

flowchart TD
  P[K1-only parity separation] --> D[SignedDecode total and functional]
  D --> E[decoded-code extensionality]
  D --> B[SignedBalance totality]
  E --> X[SignedBalance extensionality and functionality]
  B --> X
  X --> N[signed negation]
  N --> A[signed addition]
  N --> M[signed multiplication]
  X --> Z[signed Bézout bridge]
  A --> Z
  M --> Z

The RFC freezes exact expansions for SignedDecode, SignedValid, SignedBalance, SignedNegate, SignedAdd, SignedMul, SignedNatScale, and SignedBezout. It also records a crucial dependency audit: the existing even_odd_exclusive_pointwise theorem depends on division uniqueness, so it cannot seed foundational K3 coding.

That prerequisite is now a closed candidate. Its mathematical statement is

\[ \forall n,a,b,\qquad n=2a\longrightarrow n=2b+1\longrightarrow\bot. \]

The proof is a direct induction on \(n\). At zero, the odd decomposition would identify zero with a successor. At \(S n\), the odd equation peels to \(n=2b\). The even half is either zero, which is immediately impossible, or a successor; peeling that equation produces \(n=2a'+1\), contradicting the induction hypothesis. The only named dependency is the elementary zero-or-successor decomposition. In particular, the certificate does not pass through quotient or remainder uniqueness.

The decoder itself is the expanded relation

\[ \operatorname{SignedDecode}(c,p,m)\;:\!\Longleftrightarrow\; \bigl(c=2p\land m=0\bigr) \lor \exists h\,\bigl((c=2h+1\land p=0)\land m=S h\bigr). \]

Seven isolated theorems now establish its two constructors, totality, normality, functionality, exact zero characterization, and the fact that every natural is a valid code. Functionality considers the four possible pairs of decoder branches. The even/even and odd/odd cases use uniqueness of their half witnesses; both mixed cases contradict the new elementary parity separation.

Closed candidate

Nodes

Depth

Cuts

Certificate SHA-256 prefix

even_odd_exclusive_k1

80

20

1

d2ebac65fdad

even_half_unique

245

24

7

03df34e8e967

signed_decode_total

105

20

1

6fb3f4a46760

signed_decode_functional

709

27

13

50818b666470

signed_decode_zero_iff

53

16

1

7a1f625296bb

signed_valid_all

112

21

2

38b54ca5dfbe

The two constructor certificates have only 5 and 8 nodes, and normality has 36. All nine parity/decoder candidates remain outside the public registry.

Literal code equality and balanced values#

Suppose codes \(c_1,c_2\) decode to natural pairs \((p_1,n_1),(p_2,n_2)\). Their represented signed values are equal exactly when

\[ p_1+n_2=n_1+p_2. \]

Three new candidates prove both constructive directions and package them as signed_code_eq_iff_balance. This is the key extensionality fact: later operation laws can conclude literal equality of canonical natural codes, instead of introducing an untrusted quotient or a second equality relation.

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_decoded_balance_implies_code_eq

276

31

8

61adea012248

signed_code_eq_implies_decoded_balance

830

28

17

8799714212e5

signed_code_eq_iff_balance

1,181

32

25

26dbecbb46fe

Canonical normalization of balanced pairs#

SignedBalance(c,l,r) says that \(c\) decodes to some normalized pair \((p,n)\) and that

\[ l+n=r+p. \]

The totality proof uses constructive trichotomy on \(l\) and \(r\). Equality selects code \(0\); a positive excess on the right selects the appropriate odd negative code; a positive excess on the left selects an even positive code. The extensionality proof transports equality of two balanced equations to the decoded cross sum and then invokes the literal-code theorem above.

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_balance_total

236

24

4

831fdaf085ae

signed_decode_to_balance

91

13

3

3d663431a6c1

signed_balance_equations_cross_sum

410

29

8

9124fbef806a

signed_balance_extensional

736

33

16

ba68aa6e0e09

signed_balance_functional

850

34

18

900fbfc0c813

signed_balance_zero_iff

1,660

36

33

d54bade5be97

These nine extensionality/normalization certificates, like the earlier nine parity/decoder certificates, contain no DNE and reach no division, remainder, CRT, or Gödel-β dependency. They remain nonpublic. The next dependency-ordered milestone was signed negation, before addition or multiplication.

The first signed operation: negation#

Negation is especially clean in the parity-interleaved representation. If the input decodes to ((p,n)), the output is the unique code decoding to ((n,p)):

\[ \operatorname{SignedNegate}(i,o) \;:\!\Longleftrightarrow\; \exists p,n, \operatorname{SignedDecode}(i,p,n) \land \operatorname{SignedDecode}(o,n,p). \]

No subtraction operation is involved. A constructive helper builds the swapped decoder by cases on the normalized input; output functionality follows from decoder functionality and the code-extensionality bridge. Symmetry is obtained by swapping the witnesses again, and involution follows by symmetry plus functionality.

flowchart LR
  D[decoder totality] --> W[swapped decoder exists]
  W --> T[negation totality]
  F[decoder functionality] --> E[decoder/spec elimination]
  E --> U[negation functionality]
  C[decoded code extensionality] --> U
  S[negation symmetry] --> I[negation involution]
  U --> I

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_decode_swap_exists

77

21

1

77550f5f6828

signed_negate_of_swapped_decode

11

10

0

e06c193ec50f

signed_negate_to_swapped_decode

774

28

14

068786f8c357

signed_negate_total

219

23

5

fe693a95bba9

signed_negate_functional

1,160

33

25

43ba0ab36414

signed_negate_zero

19

9

0

813a59731e04

signed_negate_symmetric

20

13

0

f911ecaee17a

signed_negate_involutive

1,199

35

27

7aec997db1ea

The bounded semantic oracle checks, among other cases,

\[ 0\mapsto0,\qquad 1\mapsto2,\qquad 2\mapsto1,\qquad 3\mapsto4,\qquad4\mapsto3, \]

which are exactly (0\mapsto0), (-1\mapsto+1), (+1\mapsto-1), (-2\mapsto+2), and (+2\mapsto-2). The oracle is a regression test; the authority remains the empty-context certificate. All eight negation results remain nonpublic.

Canonical signed addition: the closed graph core#

If the two inputs and output decode respectively as ((l_+,l_-)), ((r_+,r_-)), and ((o_+,o_-)), D05 defines addition by the subtraction-free equation

\[ (l_+ + r_+) + o_- = (l_- + r_-) + o_+. \]

This is exactly the integer identity

\[ (l_+-l_-)+(r_+-r_-)=o_+-o_-, \]

but the checked statement never introduces subtraction or an integer term type. Totality decodes both inputs and sends the two natural contribution sums through SignedBalance; functionality reduces two outputs to the same balance-normalization problem.

flowchart LR
  DL[decode left] --> C[contribution sums]
  DR[decode right] --> C
  C --> B[SignedBalance totality]
  B --> T[SignedAdd totality]
  DF[decoder functionality] --> E[decoded equation elimination]
  E --> U[SignedAdd functionality]
  BF[SignedBalance functionality] --> U

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_add_of_decoded_equation

26

23

0

94c77cd7434e

signed_add_to_decoded_equation

823

35

14

77bb73fbc741

signed_add_decoded_iff_equation

956

39

16

376faba0f2bf

signed_add_total

411

27

8

793ef15dc81c

signed_add_functional

1,754

38

34

63eb78997ade

The bounded semantic regression table starts with

encoded sum

left value

right value

output value

SignedAdd(1,1,3)

\(-1\)

\(-1\)

\(-2\)

SignedAdd(1,2,0)

\(-1\)

\(+1\)

\(0\)

SignedAdd(2,2,4)

\(+1\)

\(+1\)

\(+2\)

Two cold replays agree on the complete 31-theorem signed-stack digest 11f41d395be9597892e2d5577ff80b54d04a61a57c81e50d02bc335c7e6012da. The closure has no DNE, division, remainder, CRT, Gödel-β, or negation edge. These five results remain nonpublic. They establish the total functional graph and its decoded specification; zero identity, commutativity, associativity, and addition of a value to its negation are the next separate theorem tranche. Inspect the immutable native tactic source and its cold-closure audit for every expanded statement, tactic line, mutation, and receipt.

Elementary addition laws#

The next five graph theorems close commutativity, both zero orientations, and both orders of adding a code to its canonical negation:

\[ 0+x=x,qquad x+0=x,qquad x+y=y+x,qquad x+(-x)=0,qquad(-x)+x=0. \]

Each displayed equality abbreviates an exact D05 graph statement whose inputs and output are literal canonical natural codes. In particular, the inverse results consume the exact D04 negation graph; they do not use host subtraction or an integer evaluator.

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_add_commutative

139

38

3

047393b1f607

signed_add_zero_left

266

25

7

9612c4bdec80

signed_add_zero_right

427

40

10

a2cf2150e8f0

signed_add_negate_right_zero

145

24

4

fef01c135149

signed_add_negate_left_zero

299

40

7

c0644346209c

The complete 36-theorem signed stack has deterministic digest a5fdad35078f386ccb42fd6e17f942f83f504aaaf748c40259b68a2798ab28c7. An independent audit verified that the private literal-zero expansions are alpha-identical to D05 instantiated at the appropriate slot. The transitive closure uses only four public arithmetic facts and five earlier/local signed facts, with no division, remainder, CRT, Gödel-β, classical, or DNE edge.

At this checkpoint associativity remained deliberately separate because it needed a reusable cross-sum composition lemma before graph reassociation. Inspect the immutable law tactic source and its eight-gate audit for every expanded graph, native tactic, semantic fixture, and receipt.

Associativity through cross-sum composition#

The final additive law is organized as a three-step proof rather than one large graph manipulation:

flowchart LR
  C[generic cross-sum chain] --> E[three decoded equations associate]
  D[D05 elimination aligns decoders] --> E
  E --> G[SignedAdd graph associativity]
  I[D05 introduction] --> G

The reusable arithmetic helper says

\[ a+x=b+y,\quad y+c=x+d\quad\Longrightarrow\quad a+c=b+d. \]

It prefixes both target sums by the shared contribution and cancels it. The second lemma applies this principle twice, with a proved four-summand shuffle, to the decoded equations for \(a+b\), \((a+b)+c\), and \(b+c\). The graph theorem aligns all decoder witnesses through the existing elimination bridge and reconstructs exactly SignedAdd(a,bc,abc).

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

add_cross_sum_chain

315

29

7

dff8ac71df78

signed_add_equations_associate

703

35

13

ac5629e6081d

signed_add_associative

1,695

47

30

dbac676cc565

The complete 39-theorem signed stack has deterministic digest 39ac0f7083ed54d2762289c7417b57a21c6dc97971b57efe2649ecb1cb7ec895. The semantic regression gate exhausts 4^6 tuples for the generic helper, 3^12 tuples for the equation associator, and all 4,913 triples of the first 17 canonical codes for graph associativity. Independent replay verifies the exact witness map and finds no division, remainder, CRT, Gödel-β, classical, or DNE edge.

This closes the RFC’s totality, functionality, zero, commutativity, inverse, and associativity obligations for SignedAdd at nonpublic candidate status. The following sections carry the same discipline through the complete D06 elementary SignedMul algebra. Inspect the immutable associativity tactic source and its exhaustive focused audit for the full native proof and every receipt.

The total functional SignedMul core#

The D06 multiplication graph decodes the two inputs and output and checks the subtraction-free equation

\[ (l_+r_+ + l_-r_-) + o_- = (l_+r_- + l_-r_+) + o_+. \]

This is precisely

\[ (l_+-l_-)(r_+-r_-)=o_+-o_- \]

written in the unchanged natural-only object language. The implementation does not multiply parity codes as naturals and does not invoke an external integer evaluator. Its proof ladder mirrors the addition core:

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_mul_of_decoded_equation

26

23

0

94c77cd7434e

signed_mul_to_decoded_equation

877

39

14

d50b8c46989e

signed_mul_decoded_iff_equation

1,010

41

16

14adcb23ed89

signed_mul_total

411

27

8

85d12bb18f09

signed_mul_functional

1,808

40

34

632bd740e1f6

Totality sends the positive and negative product contributions through the already proved SignedBalance normalizer. Functionality sends two possible outputs to the same balance problem. The core therefore needs no commutativity, associativity, or distributivity theorem.

Two cold replays agree on the complete 44-theorem signed-stack digest 2230cd2b67196ccec58ab5259052b08f9ef3f43275ef0b717fc35cf581cd0f6c. The semantic gate checks the unique output for all 289 pairs of the first 17 codes, including

\[ (-1)(-1)=1,\qquad (-1)(1)=-1,\qquad (2)(-2)=-4. \]

These five rows remain nonpublic. Zero, one, commutativity, associativity, and distributivity are deliberately separate D06 law gates. Inspect the candidate source and focused audit for the complete expanded formulas, tactic scripts, mutations, and receipts.

Elementary SignedMul laws#

Five additional candidates prove the first algebraic laws of the D06 graph:

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_mul_commutative

376

41

8

6bc3661f663b

signed_mul_zero_left

209

25

4

78a9b2f876c7

signed_mul_zero_right

607

43

14

30d11a080942

signed_mul_one_left

347

25

10

8d1406a347d4

signed_mul_one_right

745

43

18

fe3977029e00

The multiplicative identity is code 2, not code 1:

\[ 2\longmapsto (1,0)=+1, \qquad 1\longmapsto (0,1)=-1. \]

Thus the identity statements are graph facts

\[ \operatorname{SignedMul}(2,a,a), \qquad \operatorname{SignedMul}(a,2,a), \]

while zero annihilates in both orientations. Commutativity swaps the two decoded input pairs, commutes the four products, and reorders the two cross terms. The left zero and unit proofs construct literal D01 decoders for codes 0 and 2; the right laws follow from graph commutativity. Every private literal expansion is alpha-checked against D06, so this convenience introduces no new object-language construct.

Two cold replays agree on the complete 49-theorem signed-stack digest be074dfe1b79e3f27b2d48851c64f58360ee86fc3776ae681c451d38f67d25b2. The semantic audit checks all five laws on every pair of the first 33 codes and preserves the crucial representation test

\[ 1\cdot 1=1\quad\hbox{as natural codes}, \qquad (-1)(-1)=+1\quad\hbox{with signed output code }2. \]

The dependency closure reaches no SignedAdd law, division, remainder, CRT, Gödel-β, classical theorem, or DNE. These laws are still isolated candidates; the next section closes associativity and distributivity without admitting them. Inspect the immutable law tactic source and focused audit for the full expanded formulas, tactic scripts, exact receipts, and rejected mutations.

SignedMul associativity and distributivity#

The last D06 algebra tranche consists of four associativity candidates and seven distributivity candidates. The endpoint statements preserve the exact forward graph surfaces used by the native proofs. Associativity is

\[\begin{split} \begin{aligned} \forall a,b,c,\mathit{ab},\mathit{abc},\mathit{bc},\quad &\operatorname{SignedMul}(a,b,\mathit{ab}) \to \operatorname{SignedMul}(\mathit{ab},c,\mathit{abc})\\ &\qquad\to \operatorname{SignedMul}(b,c,\mathit{bc}) \to \operatorname{SignedMul}(a,\mathit{bc},\mathit{abc}). \end{aligned} \end{split}\]

Left distributivity is

\[\begin{split} \begin{aligned} \forall a,b,c,\mathit{bc},\mathit{ab},\mathit{ac},\mathit{out},\quad &\operatorname{SignedAdd}(b,c,\mathit{bc}) \to \operatorname{SignedMul}(a,b,\mathit{ab}) \to \operatorname{SignedMul}(a,c,\mathit{ac})\\ &\qquad\to \operatorname{SignedMul}(a,\mathit{bc},\mathit{out}) \to \operatorname{SignedAdd}(\mathit{ab},\mathit{ac},\mathit{out}), \end{aligned} \end{split}\]

and right distributivity is the separately exposed orientation

\[\begin{split} \begin{aligned} \forall a,b,c,\mathit{bc},\mathit{ba},\mathit{ca},\mathit{out},\quad &\operatorname{SignedAdd}(b,c,\mathit{bc}) \to \operatorname{SignedMul}(b,a,\mathit{ba}) \to \operatorname{SignedMul}(c,a,\mathit{ca})\\ &\qquad\to \operatorname{SignedMul}(\mathit{bc},a,\mathit{out}) \to \operatorname{SignedAdd}(\mathit{ba},\mathit{ca},\mathit{out}). \end{aligned} \end{split}\]

These are relational laws: every intermediate product and sum is supplied as a graph witness. No hidden function application or host-integer operation is introduced.

The associativity ladder first proves that a balanced decoded pair remains balanced after multiplication on either side. It next proves the two raw positive/negative component identities for reassociation. Those helpers feed a decoded-equation associator, which is transported through the existing D06 elimination and introduction bridges to obtain the graph theorem.

The distributivity ladder reuses that two-sided transport instead of duplicating it. A four-term shuffle, pairwise cross-sum composition, raw component distribution, and balanced-output composition establish left distribution at the decoded level. D05 and D06 bridges then recover the exact left graph. The right graph uses three checked applications of signed_mul_commutative followed by the left law, so there is only one large decoded calculation.

Closed candidate

Nodes

Depth

Cuts

Certificate prefix

signed_pair_mul_cross_transport

785

26

15

1ff73d62de76

signed_pair_mul_components_associate

887

26

17

35dd7e68185d

signed_mul_equations_associate

2,150

33

30

159168d3c8ed

signed_mul_associative

3,196

47

47

c6a9694ced9e

add_shuffle_middle

245

17

6

4dd61bd9bfab

add_cross_sum_pairwise

272

18

7

cb63dfdbd073

signed_mul_distributive_component

345

19

9

c4f2ccd30f68

add_balance_outputs_compose

708

32

15

9be646df81e7

signed_mul_left_cross_sum_distributes

1,172

27

21

a40d2cd61a28

signed_mul_left_distributive

3,297

58

49

c02d8258cce2

signed_mul_right_distributive

3,717

60

53

63d17772d424

The focused validation is deliberately redundant. Each dependency-curried body and each empty-context certificate is checked; a conclusion-changing mutation is rejected for every row and a concrete semantic fixture confirms that each mutated claim is false. The natural helper sweeps include all 3^12 assignments for the decoded associator, of which exactly 11,283 satisfy its premises, and all 2^14 assignments for the decoded distributivity checkpoint, of which 496 satisfy its premises. The graph oracles exhaust all 17^3=4,913 triples for associativity and for both distributive orientations. Two cache-cleared closure runs agree on every receipt and on the complete 60-row signed-stack digest 7befb7ae830b866a606e47f674730959e76599ded863aadd9868b850bcb190cd.

All eleven rows are constructive, dependency-curried, registry-isolated, and closed from the empty context. Their transitive closure reaches neither DNE nor classical reasoning, forbidden automation, division, remainder, CRT, or Gödel-β coding. At this D06 checkpoint the campaign had 60 signed candidates, 63 candidates in total, and 72 theorem receipts. The public registry remained at 393; the definition freeze and research catalog likewise remained at 45 API rows over 44 distinct public-theorem replays and 394 entries, respectively. Nothing in this tranche is publicly admitted; D07 natural scaling was the next signed-arithmetic gate.

Inspect the immutable associativity tactic source, associativity audit, distributivity tactic source, and distributivity audit for the exact expanded statements, tactic scripts, dependency audits, mutations, semantic oracles, and closed receipts.

Direct natural scaling: D07#

SignedNatScale multiplies a canonical signed code by an ordinary natural without first encoding that natural as a signed value. If input decodes as ((i_+,i_-)) and output decodes as ((o_+,o_-)), its exact defining equation is

\[ s i_+ + o_- = s i_- + o_+. \]

Equivalently, the frozen D07 graph is the following conservative expansion:

\[\begin{split} \begin{aligned} \operatorname{SignedNatScale}(s,i,o)\;:\!\Longleftrightarrow\; \exists i_+,i_-,o_+,o_-,\quad &\operatorname{SignedDecode}(i,i_+,i_-)\\ {}\land{}&\operatorname{SignedDecode}(o,o_+,o_-)\\ {}\land{}&s i_+ + o_- = s i_- + o_+. \end{aligned} \end{split}\]

All three predicate occurrences expand before kernel checking. The first five candidate rows prove introduction from the decoded equation, elimination back to it, the exact iff package, totality, and literal-code functionality. The second five supply the arithmetic transport and graph laws:

signed_nat_scale_of/to_decoded_equation
  |--> totality / functionality
  |--> zero / one
  `--> signed_nat_scale_compose
            ^
            |
mul_cross_sum_left + add_cross_sum_chain
  `--> signed_nat_scale_equations_compose

The exposed graph formulas are exactly

\[ \operatorname{SignedNatScale}(0,i,0), \qquad \operatorname{SignedNatScale}(1,i,i), \]

and

\[\begin{split} \begin{aligned} &\operatorname{SignedNatScale}(n,i,m) \to \operatorname{SignedNatScale}(k,m,o)\\ &\hspace{34mm}\to \operatorname{SignedNatScale}(kn,i,o). \end{aligned} \end{split}\]

Here 0 is the unique signed-zero code and the product in the last scale slot is the ordinary natural product. The full ten-row empty-context receipt table is:

Closed candidate

Nodes

Depth

Cuts

Certificate SHA-256

signed_nat_scale_of_decoded_equation

19

17

0

348988d2b7802c5c319975a537c568f51b55b894890638b1465bc7c8617eb918

signed_nat_scale_to_decoded_equation

785

28

14

66ef87988a3703a713a4ce0a16e235228df640be182c22d51d01f082ca5df1bd

signed_nat_scale_decoded_iff_equation

888

31

16

1b96a56388461895781783b29c091b55a61f562b198a93c8c1a7449049ec1e6a

signed_nat_scale_total

431

39

8

e1ee2921a7e967369bd70cd70564ef340ad643926c15c62dba394ae535e76947

signed_nat_scale_functional

1,698

36

34

59f948b0d2c8335cd3cd0098fb4acec9f895d8db2f930393d4dad33375ee2727

mul_cross_sum_left

98

17

2

ffa3381d8208858dee25aba6f2f96ddfe2252f7c4c45d724a84f29f043e42586

signed_nat_scale_equations_compose

575

32

13

064add40a96584356d47ca6a5455d16273403d23648ea64de5c5b3c5dc37a76b

signed_nat_scale_zero

183

21

4

0e24789df5c82b513e59f376f03758a8d8f5e8ab03869d7e54fde7b7118e63af

signed_nat_scale_one

257

21

7

90f005fdc0330354282b2dfec0105558dbc4533f1ef6436bdc070ed3a8789c4b

signed_nat_scale_compose

1,453

34

30

7548acf6871b7db3db4ba2cdaf89b9544e2d641c881a9f27e47dc4c77448b49e

The direct D07 definition was chosen deliberately over the possible D06 alias SignedMul(2*scale,input,output). That alias can be related to D07 by a later theorem, but making it foundational would force a signed encoding of every natural coefficient, add D06 to each dependency path, and hide the simple equation needed by the forthcoming Bezout bridge. The direct graph keeps the common coefficient path smaller and exposes exactly the natural arithmetic being checked.

The core audit passes all eight focused tests and the law/helper audit passes all nine. In addition to statement, hygiene, dependency, body, mutation, registry-isolation, and two-cold-replay gates, their semantic oracles are exhaustive over the selected domains:

  • all (17\cdot17=289) scale/input pairs are tested against every one of 257 candidate output codes;

  • the natural helper checks exactly 425 assignments satisfying its cross-sum premise, and the decoded composition helper checks exactly 477 assignments satisfying both premises;

  • zero and one are checked on the first 33 canonical codes, while composition is checked on all (17^3=4{,}913) bounded triples.

The raw-code regression is essential: (2\cdot1=2) in natural arithmetic, but code 1 denotes (-1), so scaling it by two produces code 3, the canonical representation of (-2), rather than code 2. Host evaluation is only a test oracle; logical authority comes from the empty-context kernel certificates above.

Two cache-cleared closures agree on the five-core-row, 65-theorem signed-stack digest 511aa0ba4a6dac1a22f52db740f539c675307b5b77b6b1a7d9ef2e00dd8a5331. Adding the five law/helper rows gives the 70-theorem digest 81a18daf55e564c11dee83ce7465bc91876109a5e6bc092f75e0f31f46e27d8d. The closure is intuitionistic and reaches no DNE, forbidden automation, division, remainder, CRT, Gödel-β, or classical theorem.

This checkpoint contains 70 signed candidates and 73 candidates overall, with 82 theorem receipts across 15 K3 candidate modules and 17 focused evidence tests. The public registry is unchanged at 393 entries with 56 public references; the definition layer is unchanged at 45 API rows over 44 distinct public-theorem replays; and the research catalog is unchanged at 394 entries. None of D07 is admitted. D08 SignedBezout is the next signed-arithmetic gate.

The sealed checkpoint campaign manifest and signed-natural RFC bind these claims to the exact core tactic source, law tactic source, eight-test core audit, and nine-test law audit.

Canonical signed Bezout coefficients: D08#

The legacy Euclidean layer represents a signed Bezout identity with four naturals. Write

\[ \operatorname{BalancedBezout}(r,a,b) \;:\!\Longleftrightarrow\; \exists x_+,y_+,x_-,y_-,\quad a x_+ + b y_+ = r + \bigl(a x_- + b y_-\bigr). \]

This is honest natural arithmetic: it means (a(x_+-x_-)+b(y_+-y_-)=r) without adding subtraction or an integer type. D08 connects it to the parity-interleaved canonical signed codes. If (\operatorname{Decode}(x,x_+,x_-)) and (\operatorname{Decode}(y,y_+,y_-)) are the frozen D01 decoders, define

\[\begin{split} \begin{aligned} \operatorname{SignedBezout}(r,a,b,x,y) \;:\!\Longleftrightarrow\;& \exists x_+,x_-,y_+,y_-,\\ &\operatorname{Decode}(x,x_+,x_-) \land \operatorname{Decode}(y,y_+,y_-)\\ &\land\;a x_+ + b y_+ = r + \bigl(a x_- + b y_-\bigr). \end{aligned} \end{split}\]

The checked endpoint is the intuitionistic pair of implications

\[ \operatorname{BalancedBezout}(r,a,b) \quad\Longleftrightarrow\quad \exists x,y,\ \operatorname{SignedBezout}(r,a,b,x,y), \]

where the displayed (\Longleftrightarrow) is stored as a conjunction of two implications. It does not claim that ((x,y)) is unique. Canonical representation makes each chosen coefficient unique as a code, but a Bezout equation may have many coefficient pairs. For example,

\[ 2(-1)+3(1)=1=2(2)+3(-1), \]

so codes (1,2) and (4,1) are two distinct D08 witnesses for the same result and inputs.

The main algebraic step takes raw coefficients and normalized coefficients:

\[\begin{split} \begin{aligned} x_+ + x'_- &= x_- + x'_+,\\ y_+ + y'_- &= y_- + y'_+,\\ a x_+ + b y_+ &= r + (a x_- + b y_-), \end{aligned} \end{split}\]

and proves

\[ a x'_+ + b y'_+ = r + (a x'_- + b y'_-). \]

The first two equalities come independently from SignedBalance. They are lifted by mul_cross_sum_left, combined by add_balance_outputs_compose, and oriented with ordinary commutativity. No signed multiplication or natural-scale graph is needed in this bridge. The proof also makes an easy-to-miss representation change explicit: BalancedBezout stores witnesses in the order xp,yp,xn,yn, while SignedBezout groups decoder parts as xp,xn,yp,yn.

flowchart LR
  SB[SignedBalance totality] --> F[balanced to signed]
  MC[mul_cross_sum_left] --> T[equation transport]
  AC[add_balance_outputs_compose] --> T
  T --> F
  R[signed to balanced] --> I[packaged equivalence]
  F --> I

The proof surface has four topologically ordered rows:

Candidate

Nodes

Depth

Cuts

Certificate SHA-256

balanced_bezout_equation_transport

943

34

20

9e3f3b984b0c9bdd42e7747f5660541364bb5bee3655b95b9242e5ed3305e4cc

balanced_bezout_to_signed_bezout

1,241

39

24

f39a790749e8da2b6d6c36f3639e2b81ecdd1b5db892a543a7ece18941978923

signed_bezout_to_balanced_bezout

35

23

0

f0fb3fa8d5f09c69d22721164468227765bab34b6f1eadb8d67593bfeb81fa28

balanced_bezout_iff_signed_bezout_exists

1,326

40

26

1bc7e28457b07b7aaf37b48aea0f3f86b58035797aeca50a022c73409f6eae1d

The focused audit pins the exact D08 template, statements, ordered dependencies, tactic bodies, empty-context DAG receipts, false mutations, registry isolation, and endpoint reachability. Its untrusted semantic oracle exhausts 2,185 satisfying transport premises, 5,736 raw balanced witnesses, and 1,600 bounded direct graph cases. It includes nonunique solutions, an all-zero coefficient boundary, and a trap showing that the raw parity codes cannot be substituted for decoded signed values.

Two cache-cleared closures agree on the complete 74-row signed-stack digest b7949148236ab243830a2bfebd80ddafeb31a63c5e70ace1c032de8bd2415f15. The transitive closure contains no DNE, forbidden automation, division, remainder, CRT, Gödel-β, or classical theorem. The campaign now records 74 signed candidates, 77 candidates overall, and 86 exact receipts across 16 K3 candidate modules and 18 focused evidence tests. The public registry remains 393 entries with 56 public references; the definition freeze remains 45 rows over 44 public theorems; and the catalog remains 394 entries. No D08 row is publicly admitted.

The separate theorem that combines this bridge with gcd_balanced_bezout_exists belongs to K4, not this strict K3 closure: the public gcd route transitively reaches division. Likewise, D08 does not assert a canonical choice of Bezout pair. Those are deliberate mathematical and architectural boundaries, not missing hidden assumptions.

The sealed source checkpoint binds the exact campaign manifest, signed-natural RFC, D08 tactic source, and ten-test focused audit to commit bb02ee5a767f6c4c585916269de688e7068b3716.

K4 client: a gcd with canonical signed coefficients#

Once the strict D08 bridge is available, the public Euclidean theorem can be given its canonical signed interface without reproving the algorithm. The checked client states

\[ \forall a,b\;\exists d,x,y,\quad \operatorname{IsGCD}(d,a,b) \land \operatorname{SignedBezout}(d,a,b,x,y). \]

Both named relations are expanded to the base HA grammar. The proof has just two declared inputs:

gcd_balanced_bezout_exists
        |
        v
raw gcd + four-natural Bezout witnesses
        |
        +---- balanced_bezout_to_signed_bezout (D08)
        v
gcd_signed_bezout_exists

The first theorem supplies d together with the relational-gcd proof and raw coefficients. D08 normalizes only the coefficient conjunct; the gcd proof is copied unchanged. No uniqueness of (x,y) is asserted.

Candidate

Nodes

Depth

Cuts

Certificate SHA-256

gcd_signed_bezout_exists

3,535

48

74

4edeb4ffc7de0b9aa0a870d2125f7640f2447a7358ba454abba3db003f9044a3

The focused audit pins the 592-byte expanded statement (SHA-256 2e729fe9d25b8afda315489713f0a4cd7980371bf621e8af9e557f4ffca7496e), its 20-command body, two cold closures, a false successor mutation, bounded gcd semantics, and explicit nonunique Bezout pairs. The transitive closure contains eight local K3 rows and 33 public theorems. Exactly the expected division boundary is visible: divides_remainder, division_remainder_exists, and division_remainder_succ. It contains no DNE, CRT, Gödel-β, or classical theorem.

This is why the machine manifest adds the honest layer edge (K3\rightarrow K4). The client is not appended to the strict 74-row K3 stack, whose digest stays b7949148236ab243830a2bfebd80ddafeb31a63c5e70ace1c032de8bd2415f15. At this intermediate checkpoint the complete isolated corpus had 78 candidates and 87 receipts across 18 candidate modules and 19 focused tests; the public boundary was still 393 theorems. The later selective K4 admission does not include this client: gcd_signed_bezout_exists is one of the 19 checked K4 conveniences which remain private.

The immutable source links are the campaign manifest, K4 tactic source, and six-test focused audit.

Canonical gcd and universal-property lcm#

This K4 tranche first closed the natural-valued gcd and lcm interface in isolation and was then admitted selectively. It does not add either operation as a term former. Divisibility remains the relation

\[ d\mid n\quad:\!\Longleftrightarrow\quad\exists q,\ n=dq, \]

and the least-common-multiple relation is the exact order dual of IsGCD:

\[ \operatorname{IsLCM}(l,a,b) \;:\!\Longleftrightarrow\; (a\mid l)\land(b\mid l)\land \forall c,\ (a\mid c)\to(b\mid c)\to(l\mid c). \]

In the native parser this expands hygienically to

(((exists x. l = a * x) /\ (exists y. l = b * y)) /\
 forall c. (exists u. c = a * u) ->
           (exists v. c = b * v) ->
           exists w. c = l * w)

No new predicate reaches the kernel. In particular,

\[ \gcd(a,b)\operatorname{lcm}(a,b)=ab \]

is proved after the two universal properties; it is not used to define lcm. The product equation alone would be nonfunctional at \((a,b)=(0,0)\).

Forced boundary values#

The universal property constructively forces

\[ \operatorname{lcm}(0,b)=0,\qquad \operatorname{lcm}(a,0)=0,\qquad \operatorname{lcm}(0,0)=0. \]

The selected proof proves the right-zero constructor directly and derives the left-zero constructor by symmetry. Those two constructors, is_lcm_zero_right and is_lcm_zero_left, are public. The derived zero-value and unique-existence conveniences remain private. The companion gcd tranche supplies five function-style boundary laws:

\[\begin{split} \begin{aligned} \operatorname{IsGCD}(g,a,0)&\;\Longleftrightarrow\;g=a,\\ \operatorname{IsGCD}(g,0,a)&\;\Longleftrightarrow\;g=a,\\ \operatorname{IsGCD}(g,1,a)&\;\Longleftrightarrow\;g=1,\\ \operatorname{IsGCD}(g,a,1)&\;\Longleftrightarrow\;g=1, \end{aligned} \end{split}\]

together with equality of independently chosen gcd witnesses after swapping the two inputs. All five close from the empty context and remain private.

The constructive totality route#

The 17-row structural lcm API proves its two multiple projections, leastness, symmetry, uniqueness, zero/one/reflexive constructors, divisibility constructors, product common-multiple witnesses, and the zero-value packages. General totality is then obtained through the following K4 route:

balanced Bezout for a gcd
        |
        +--> cancel a nonzero gcd --> Bezout result 1 --> coprime quotients
        |                                                   |
        |                                                   v
        |                                      product of quotients is an lcm
        |                                                   |
decide gcd = 0                                              v
        |                                        scale the lcm by the gcd
        +---------------------------> compatible gcd/lcm existence
                                                     |
                          +--------------------------+-------------------+
                          v                          v                   v
                 relational lcm exists       unique lcm value     gcd*lcm = a*b

The zero branch uses the forced-zero lcm law. The nonzero branch cancels the gcd from a balanced Bezout equation, proves the two quotients coprime, takes their product as an lcm, and scales it by the gcd. The split uses the already proved constructive theorem eq_decidable; none of these certificates contains DNE or a classical axiom.

The public K4 atlas#

Admission is an exact append-only slice: seven universal-property lcm lemmas followed by nine bridge lemmas. Each name below opens its theorem-atlas card, where the expanded HA statement, direct prerequisites, tactic source, and certificate receipt can be inspected.

Position

Public theorem

Mathematical role

393

is_lcm_multiple_left

An lcm is a multiple of its left input.

394

is_lcm_multiple_right

An lcm is a multiple of its right input.

395

is_lcm_least

Every common multiple is a multiple of the lcm.

396

is_lcm_symm

Symmetry of the relational lcm specification.

397

is_lcm_unique

Uniqueness from the universal property.

398

is_lcm_zero_right

The forced right-zero constructor.

399

is_lcm_zero_left

The forced left-zero constructor.

400

balanced_bezout_one_implies_coprime

A balanced Bezout witness for one implies coprimality.

401

coprime_product_is_lcm

The product of coprime inputs satisfies IsLCM.

402

is_lcm_scale_nonzero

Nonzero common scaling preserves the lcm relation.

403

balanced_bezout_cancel_gcd

Cancel a nonzero gcd from a balanced Bezout equation.

404

gcd_zero_inputs

Both inputs are zero when their gcd is zero.

405

gcd_lcm_compatible_exists

Construct compatible relational gcd and lcm witnesses.

406

lcm_exists_relational

Totality of the relational lcm specification.

407

canonical_lcm_exists_unique

Unique existence of the natural lcm value.

408

gcd_lcm_product

The relational product identity (g l = a b).

Public K4 endpoint

Nodes

Depth

Cuts

DNE

Certificate SHA-256

gcd_lcm_compatible_exists

9,038

60

101

0

dfe0e69fb172e48b6aa785c0c088ebf1a7cdf09c95ae436305d51d6224e90bc3

lcm_exists_relational

9,071

61

102

0

f4e764738627255eb885d78b5cefd74663d68be022370a8036ee450b116a7220

canonical_lcm_exists_unique

9,791

62

111

0

3ab4c410a0e4c6717e77d7f951d26304a35b5e9451df299167bb42cadf227747

gcd_lcm_product

10,441

61

112

0

c0829496624e993a4c437aa98c32355605109e728acd03d6b5d857fcb5350d0a

The selective admission raises the runtime registry to 409 theorems and the research catalog to 410 rows, of which 386 are checked_m20. The campaign manifest now carries 72 public references, 116 isolated candidates, and 141 exact theorem receipts. The strict 74-row K3 signed stack and its digest b7949148236ab243830a2bfebd80ddafeb31a63c5e70ace1c032de8bd2415f15 are unchanged, as is the frozen first-247 model curriculum.

What remains private#

Admission deliberately stops at the reusable mathematical interface. The following 19 checked K4 conveniences retain exact receipts but are not public registry entries:

  • canonical gcd packaging (3): canonical_gcd_exists, canonical_gcd_functional, and canonical_gcd_exists_unique;

  • gcd boundary conveniences (5): canonical_gcd_zero_right_iff, canonical_gcd_zero_left_iff, canonical_gcd_one_left_iff, canonical_gcd_one_right_iff, and canonical_gcd_swap_functional;

  • residual lcm conveniences (10): is_lcm_of_dvd, is_lcm_of_dvd_right, product_common_multiple, is_lcm_refl, is_lcm_one_left, is_lcm_one_right, lcm_zero_left_value, lcm_zero_right_value, lcm_zero_left_exists_unique, and lcm_zero_right_exists_unique;

  • the signed client (1): gcd_signed_bezout_exists.

A checked private receipt is evidence of empty-context closure, not an admission by implication. The public/private boundary is therefore explicit and machine-audited.

The current implementation and audit trail are the canonical gcd/lcm RFC, relational-lcm source, relational-lcm tests, totality/compatibility source, totality/compatibility tests, and the exact K4 admission test.

Generalized CRT: the all-modulus binary criterion is closed#

The M5a layer keeps congruence and gcd relational. Its readable definitions are

\[ \operatorname{ModEq}(d,a,b)\;:\!\Longleftrightarrow\; \exists u,v,\ a+du=b+dv, \]
\[ \operatorname{CRTSolution}(x;m,n;a,b)\;:\!\Longleftrightarrow\; \operatorname{ModEq}(m,x,a)\land\operatorname{ModEq}(n,x,b), \]

and the already frozen result-first relation

\[ \operatorname{IsGCD}(g,m,n) \;:\!\Longleftrightarrow\; g\mid m\land g\mid n\land \forall d\,(d\mid m\land d\mid n\to d\mid g). \]

Every displayed predicate expands before parsing to the unchanged language ({0,S,+,\times,=}). The kernel receives no congruence, gcd, quotient, remainder, or CRT primitive.

The original eight-row foundation proves congruence algebra, necessity, and obstruction. The new seven-row sufficiency ladder is:

Row

Candidate

Mathematical role

1

factor_nonzero_right

The right factor of a nonzero product is nonzero.

2

is_gcd_quotients_coprime_nonzero

If (m=gM), (n=gN), and (g\ne0), then (M,N) are coprime.

3

is_gcd_nonzero_coprime_quotients

Package the two factor equations, all three nonzero facts, and cofactor coprimality.

4

mod_eq_common_remainder_decomposition

Compatible residues share (r<g): (a=gA+r), (b=gB+r).

5

crt_scaled_common_remainder_lift

Solve modulo (M,N), scale by (g), then add the common (r).

6

generalized_binary_crt_sufficient_nonzero

Gcd compatibility constructs an actual common solution for nonzero moduli.

7

generalized_binary_crt_solvable_iff_nonzero

Solvability is equivalent to gcd compatibility for nonzero moduli.

The capstone has the standard mathematical statement

\[\begin{split} \begin{aligned} &m\ne0\to n\ne0\to \operatorname{IsGCD}(g,m,n)\to{}\\ &\qquad\Bigl[ (\exists x\,\operatorname{CRTSolution}(x;m,n;a,b)) \to \operatorname{ModEq}(g,a,b) \Bigr]\\ &\qquad\land\Bigl[ \operatorname{ModEq}(g,a,b) \to \exists x\,\operatorname{CRTSolution}(x;m,n;a,b) \Bigr]. \end{aligned} \end{split}\]

Why the cofactors are coprime#

Suppose (d\mid M) and (d\mid N). Then

\[ gd\mid m,\quad gd\mid n, \]

so greatestness in IsGCD(g,m,n) gives (gd\mid g). For some (w),

\[ g=(gd)w=g(dw). \]

Since (g\ne0), left cancellation against (g\cdot1) gives (1=dw), and hence (d=1). This is the whole cofactor-coprimality proof; it does not need a new Bézout theorem.

Construction#

Compatibility supplies a common canonical remainder:

\[ a=gA+r,\qquad b=gB+r,\qquad r<g. \]

The public coprime CRT produces (z) with

\[ z\equiv A\pmod M,\qquad z\equiv B\pmod N. \]

Scale both congruences by (g), add the reflexive congruence (r\equiv r), and choose

\[ x=gz+r. \]

Then (x\equiv a\pmod m) and (x\equiv b\pmod n).

flowchart LR
  G[IsGCD(g,m,n)] --> Q[m=gM, n=gN]
  Q --> NZ[g,M,N nonzero]
  Q --> CP[Coprime(M,N)]
  C[a congruent b mod g] --> R[a=gA+r, b=gB+r, r<g]
  CP --> B[binary_crt M N A B]
  B --> Z[z mod M=A, z mod N=B]
  Z --> SC[scale congruences by g]
  R --> ADD[add common remainder r]
  SC --> ADD
  ADD --> X[x=gz+r is a common solution]
  X --> IFF[nonzero solvability iff compatibility]
  N[necessity theorem] --> IFF
  IFF --> D[decide m=0 and n=0]
  ZL[left modulus zero: choose x=a] --> D
  ZR[right modulus zero: choose x=b] --> D
  D --> ALL[all-modulus solvability iff compatibility]
  ALL -. next .-> L[classify solutions modulo IsLCM]

Closed candidate

Nodes

Depth

Cuts

Certificate SHA-256 prefix

is_gcd_quotients_coprime_nonzero

660

33

18

b20e99453775b469

mod_eq_common_remainder_decomposition

2,894

69

43

7615686f1fb9c23b

crt_scaled_common_remainder_lift

5,745

52

92

188a46f051c74f8a

generalized_binary_crt_sufficient_nonzero

9,482

74

141

9c1ad09a4bfb2ee8

generalized_binary_crt_solvable_iff_nonzero

10,073

76

149

8956a66d8f72d512

Two cache-cleared closures agree for every row. The focused tests pin the expanded statements, dependencies, scripts, body metrics, complete proof-DAG digests, false-endpoint mutations, and bounded arithmetic semantics. All certificates use the intuitionistic checker and contain zero DNE nodes. No formula or proof limit was raised.

The zero boundary does not use division#

The four-row M5b layer closes the cases deliberately excluded from the remainder construction:

Candidate

Mathematical role

generalized_binary_crt_sufficient_zero_left

From IsGCD(g,0,n), public gcd uniqueness gives (g=n); choose (x=a).

generalized_binary_crt_sufficient_zero_right

From IsGCD(g,m,0), public gcd uniqueness gives (g=m); choose (x=b).

generalized_binary_crt_sufficient

Constructively dispatch left-zero, right-zero, and both-nonzero cases.

generalized_binary_crt_solvable_iff

Combine total sufficiency with the earlier necessity theorem.

The first row includes ((m,n)=(0,0)): compatibility is then equality of the residues, so the chosen residue solves both equations. The total theorem uses the already checked constructive decision eq_decidable; it does not use excluded middle as a kernel principle. In readable notation the capstone is

\[\begin{split} \begin{aligned} \operatorname{IsGCD}(g,m,n)\to\Bigl(& [\exists x\,\operatorname{CRTSolution}(x;m,n;a,b) \to \operatorname{ModEq}(g,a,b)]\\ &\land[\operatorname{ModEq}(g,a,b) \to\exists x\,\operatorname{CRTSolution}(x;m,n;a,b)]\Bigr), \end{aligned} \end{split}\]

with no assumptions that (m), (n), or (g) is nonzero.

Closed candidate

Nodes

Depth

Cuts

Certificate SHA-256 prefix

generalized_binary_crt_sufficient_zero_left

834

37

26

074f07df17330847

generalized_binary_crt_sufficient_zero_right

805

36

26

da2d830f65077816

generalized_binary_crt_sufficient

11,240

78

160

931fbcc775154507

generalized_binary_crt_solvable_iff

11,825

80

168

3f1d82f0f06df9e0

All four certificates have zero DNE nodes and fit the existing limits. No private canonical-gcd convenience theorem is a dependency. This is still candidate evidence, not public admission: the registry remains at 409 and the research catalog at 410.

Complete solution classes via relational LCM#

The four-row M5c layer now closes that classification boundary without adding a primitive lcm function:

Candidate

Exact surface interface

Ordered direct dependencies

mod_eq_ordered_gap_multiple

k+x=y -> ModEq(d,x,y) -> Dvd(d,k)

add_comm, add_assoc, add_left_cancel, factor_difference

mod_eq_lcm_merge

IsLCM(l,m,n) -> ModEq(m,x,y) -> ModEq(n,x,y) -> ModEq(l,x,y)

le_total, mod_eq_symm, the ordered-gap row, is_lcm_least, mul_comm, remainder_decomposition_to_mod_eq

mod_eq_lcm_iff_pair

Under IsLCM(l,m,n), ModEq(l,x,y) iff ModEq(m,x,y) /\ ModEq(n,x,y)

is_lcm_multiple_left, is_lcm_multiple_right, mod_eq_of_mod_eq_multiple, the merge row

crt_solution_class_iff_lcm

For a fixed solution x, CRTSolution(y,m,n,a,b) iff ModEq(l,y,x)

crt_solution_pair_congruent, the LCM-iff-pair row, mod_eq_trans

The proof is subtraction-free. Total order chooses a directed gap between two naturals. Congruence modulo each input modulus makes each modulus divide that gap; is_lcm_least then makes the supplied relational LCM divide it. The public LCM projections prove the converse direction. For the capstone, the forward implication compares the candidate y with the fixed solution x; the reverse implication composes y == x with the two congruences already carried by x. This orientation is part of the audited interface.

Body receipts below use (dependencies, commands, nodes, depth, objects, edges, reused). Closed receipts use (nodes, depth, objects, edges, reused, Cuts, DNE, certificate SHA-256).

Closed candidate

Dependency-curried body

Empty-context certificate

mod_eq_ordered_gap_multiple

(4,31,44,21,44,43,0)

(558,30,310,325,16,13,0,6a30012cfc1213bf167be2de794e05cdae2893ab075cfc24abf9b181bde9be67)

mod_eq_lcm_merge

(6,113,127,26,127,126,0)

(1315,33,653,685,33,25,0,46cd67f69ccf0c669de283fca6a74a0a85cf18d54f248f1a6f428122196a331b)

mod_eq_lcm_iff_pair

(4,46,56,21,56,55,0)

(1570,37,864,908,45,32,0,855d5745c1613304fc0a5f26c70fe9f795ed3ebcff4a7276e3745681d41fc91a)

crt_solution_class_iff_lcm

(3,62,79,27,79,78,0)

(2208,39,1055,1104,50,40,0,305a913aaca1c3e307d8ca77bb90c063dd67f3fa9f9bdd69e28cf4064cdff7b3)

The theorem is uniform at (l=0): ModEq(0,y,x) is exactly (y=x), so the solution class collapses to exact uniqueness. The proof does not divide by the LCM and never asserts a remainder below zero. A bounded semantic audit passed 1,296 LCM-equivalence cases, 4,692 fixed-solution classification comparisons, and 678 comparisons with (l=0). Both cold closures check with zero DNE and the existing resource limits. M5c raises the private evidence totals to 116 candidate references and 141 exact receipts; the public registry and catalog remain unchanged at 409 and 410.

Honest canonical boundary at zero and nonzero LCM#

The three-row M5d layer now closes the boundary that M5c exposed. Write

\[ \operatorname{Below}(r,l)\;:\!\Longleftrightarrow\; \exists h\;(h+S(r)=l). \]

Candidate

Exact surface result

Ordered direct dependencies

crt_solution_unique_lcm_zero

At l=0, every solution y equals a fixed solution x.

crt_solution_class_iff_lcm, mod_eq_zero_iff_eq

crt_solution_canonical_remainder_nonzero

At l!=0, produce r with Below(r,l), CRTSolution(r), ModEq(l,r,x), and bounded uniqueness.

division/remainder, mul_comm, remainder-to-congruence, mod_eq_symm, M5c classification, mod_eq_bounded_unique

generalized_binary_crt_canonical_boundary

From IsGCD, IsLCM, and compatibility, return either an exactly unique zero-LCM solution or a unique bounded nonzero-LCM solution.

eq_decidable, total M5b sufficiency, the first two M5d rows

The capstone first constructs a fixed solution and decides l=0 constructively. In the zero branch, M5c plus mod_eq_zero_iff_eq gives exact equality. In the nonzero branch, division produces the remainder of the fixed solution; M5c transports it back into the CRT solution class, and bounded congruence uniqueness makes it canonical. The auxiliary ModEq(l,r,x) is retained in row 2 and intentionally hidden by the capstone.

Closed candidate

Dependency-curried body

Empty-context certificate

crt_solution_unique_lcm_zero

(2,33,37,28,37,36,0)

(2300,40,1126,1176,51,43,0,2afc46ac88613c95400eb37f80b1fbda095b18a7f6a774255426b48c35aed9ac)

crt_solution_canonical_remainder_nonzero

(6,83,141,39,141,140,0)

(4086,65,1668,1746,79,64,0,091e8f2b1ba7e4665b87071fcd924ea1098880d65a97bcdd264ed544e33ff0e4)

generalized_binary_crt_canonical_boundary

(4,66,76,33,76,75,0)

(17750,80,4239,4426,188,193,0,c704a17f6feed83142b160bbeafcc14764d5ae6590999187eed5455c3ad03bd7)

The body and closed-receipt schemas are the same as in the M5c table. Two cold closures agree and all three certificates have zero DNE. A retained bounded audit checks 4,021 compatible systems with m,n<7 and a,b<11: 611 zero-LCM exact-uniqueness cases and 3,410 nonzero-LCM canonical-remainder cases. Since either zero input modulus forces the relational LCM to zero, the first count is intentionally broader than the single (0,0) case. No branch asserts a remainder below zero. The private evidence totals are now 119 candidates and 144 exact receipts; public counts remain 409/410.

Executable solution or obstruction#

M5e makes the binary result total without adding a host-language decision oracle:

Candidate

Exact surface result

Ordered direct dependencies

mod_eq_decidable

ModEq(d,a,b) \/ ~ModEq(d,a,b) for every natural d.

eq_decidable, mod_eq_zero_iff_eq, public mod_eq_decidable_nonzero

generalized_binary_crt_solution_or_obstruction

Given IsGCD(g,m,n), return either compatibility plus an actual CRT solution, or incompatibility plus a proof that no solution exists.

mod_eq_decidable, total M5b sufficiency, crt_incompatibility_obstructs_solution

At modulus zero the first row decides equality and uses mod_eq_zero_iff_eq; at nonzero modulus it reuses the public remainder-based decision theorem. The second row cases on that proof. Its positive branch constructs a solution, while its negative branch applies the already isolated obstruction theorem. Both branches retain the compatibility or incompatibility certificate, so the result contains more information than P \/ ~P alone.

Closed candidate

Dependency-curried body

Empty-context certificate

mod_eq_decidable

(3,35,47,16,47,46,0)

(2339,70,1217,1278,62,44,0,298e2b18fff84bcf3a2ec69dbc464454f958d4155b7afb687f0bab2fd95efe7e)

generalized_binary_crt_solution_or_obstruction

(3,36,43,22,43,42,0)

(14182,80,3909,4090,182,182,0,16e7cb1c430fa4e17ea878adc72d34c92e0bc3f135c4a3cf24cb2a296b38e525)

Two cold closures agree, false endpoint mutations fail, and both certificates have zero DNE within unchanged limits. The retained semantic audit covers 847 all-modulus congruence decisions and all 5,929 systems with m,n<7 and a,b<11: 4,021 return compatibility with a solution and 1,908 return incompatibility with unsolvability. This brings private evidence to 121 candidates and 146 receipts; the public registry/catalog remain 409/410. M5d remains the separate composable canonicalization API.

Raw-input total decision#

M5f removes the need for a caller to supply a gcd witness. Its single theorem has the readable statement

\[\begin{split} \begin{aligned} \forall m,n,a,b\;\exists g\;\bigl(&\operatorname{IsGCD}(g,m,n)\land \Bigl([\operatorname{ModEq}(g,a,b)\land \exists x\,\operatorname{CRTSolution}(x;m,n;a,b)]\\ {}\lor{}&[\neg\operatorname{ModEq}(g,a,b)\land \neg\exists x\,\operatorname{CRTSolution}(x;m,n;a,b)]\Bigr)\bigr). \end{aligned} \end{split}\]

The proof first applies gcd_exists_relational, obtaining an existential natural (g) together with IsGCD(g,m,n), and then invokes generalized_binary_crt_solution_or_obstruction. Thus the exact ordered dependency list has only those two rows. The theorem does not introduce a primitive gcd function: its witness remains governed by the expanded IsGCD relation. Nor does it return a bounded canonical solution. That is the separate zero/nonzero-LCM interface supplied by M5d.

Closed candidate

Dependency-curried body

Empty-context certificate

generalized_binary_crt_total_decision

(2,17,42,25,42,41,0)

(15492,82,4052,4240,189,192,0,c2d915d2eb60ccbb2dac9f31e9e1f9c310c28264b74483ec97ae33a1a0d965ee)

The body and closed tuples use the schemas specified above. The expanded statement SHA-256 is 42d29bf501421be60c1a2b14fa858a14abf230eee2f7669503db019d6b014151. Two cold closures agree, the certificate has zero DNE nodes, and no proof limit changed. The raw-input semantic audit covers all 5,929 systems with m,n<7 and a,b<11: 4,021 take the solution branch and 1,908 take the obstruction branch. Among the 121 systems whose relational gcd is zero, 11 are solvable and 110 are obstructed. The campaign now contains 122 private candidates and 147 receipts; the public registry/catalog remain 409/410.

Finite generalized CRT remains gated by the independent finite-data representation.

Read the generalized-CRT RFC, congruence source, sufficiency source, zero-boundary source, classification source, canonical-boundary source, executable-boundary source, raw-input decision source, foundation audit, sufficiency audit, zero-boundary audit, classification audit, canonical-boundary audit, executable-boundary audit, and the raw-input decision audit for the exact expanded formulas and line-by-line tactic scripts.

Selective M5 admission: the exact public boundary#

The campaign did not promote every closed convenience theorem. It admitted the exact dependency closure needed by three durable endpoints: generalized_binary_crt_solvable_iff, generalized_binary_crt_canonical_boundary, and generalized_binary_crt_total_decision. In registry order, the resulting 23-row public surface is:

Role

Exact public theorem names

Congruence and necessity

mod_eq_zero_iff_eq; mod_eq_scale; crt_solution_pair_congruent; crt_common_solution_implies_gcd_compatible; crt_incompatibility_obstructs_solution

Nonzero construction

is_gcd_quotients_coprime_nonzero; mod_eq_common_remainder_decomposition; crt_scaled_common_remainder_lift; generalized_binary_crt_sufficient_nonzero

All-modulus solvability

generalized_binary_crt_sufficient_zero_left; generalized_binary_crt_sufficient_zero_right; generalized_binary_crt_sufficient; generalized_binary_crt_solvable_iff

Relational-LCM solution class

mod_eq_ordered_gap_multiple; mod_eq_lcm_merge; mod_eq_lcm_iff_pair; crt_solution_class_iff_lcm

Canonical boundary

crt_solution_unique_lcm_zero; crt_solution_canonical_remainder_nonzero; generalized_binary_crt_canonical_boundary

Executable decision

mod_eq_decidable; generalized_binary_crt_solution_or_obstruction; generalized_binary_crt_total_decision

The exact six-row private residual is equally important:

  • mod_eq_add_cancel_left and mod_eq_add_cancel_right;

  • mod_eq_unscale_nonzero;

  • factor_nonzero_right;

  • is_gcd_nonzero_coprime_quotients; and

  • generalized_binary_crt_solvable_iff_nonzero.

These six formulas still have deterministic empty-context receipts, but no public registry position and therefore no pa lib authority. The distinction is mathematical curation rather than a proof-status ambiguity: the public 23-row closure already contains every premise needed by the three selected endpoints.

The admission appends positions 409–431 without changing the first-247 model prefix. The current snapshot has 432 theorem cards and 1,185 direct dependency edges. Its synchronized Obsidian vault has 531 notes and 5,377 resolved links. The research catalog has 433 rows: 432 checked theorems and the one explicitly representation-blocked conventional integer-coefficient Bézout interface.

Independent pair/cell checkpoint#

The finite-data lane now has 15 closed private candidates: seven literal constructor and nil/cell-boundary rows, six shell-arithmetic rows, and two injectivity rows. For (s=x+y), write

\[ B_s=s(s+1), \qquad \operatorname{pair}_2(x,y)=B_s+2y. \]

This is twice the Cantor pairing polynomial. The shell layer proves the exact constructive bounds

\[ B_s\leq \operatorname{pair}_2(x,y)<B_{s+1}. \]

Consequently two unequal shell indices force two unequal codes. The final pair_code_injective proof applies trichotomy to (s_1=x_1+y_1) and (s_2=x_2+y_2). Either strict branch, together with pair_code_shell_separated, would make the shared code strictly smaller than itself, so (s_1=s_2). Cancelling the common boundary (B_{s_1}) gives (2y_1=2y_2); double_add_injective gives (y_1=y_2); and one final additive cancellation gives (x_1=x_2). Thus injectivity uses no decoder, division, choice, or hidden host computation.

The two largest checkpoint receipts, displayed as (nodes, depth), are pair_code_shell_separated = (1600, 30) and pair_code_injective = (2525, 32). Every one of the 15 rows closes twice from the empty context with zero DNE. Their transitive closures are quarantined to the K0–K2 equality, addition, multiplication, order, cancellation, and formula-specific induction foundation: no division, remainder, CRT, Gödel-β, prime-factor coding, classical rule, or assumed sequence enters.

The full statements, tactic bodies, receipts, mutations, and bounded semantic oracles are linked from the pair/cell RFC, the three source modules (seed, shells, injectivity), and their focused audits (seed test, shell test, injectivity test).

These rows remain private: the public runtime and research catalog stay at 432 and 433 entries. The campaign now records 95 public references, 114 closed candidates, 162 distinct receipts, 25 candidate modules, and 34 focused test paths. At this checkpoint the honest next obligations were cell functionality, strict head and tail bounds, and an independent uniform computation-history representation supporting lists and finite maps. A successor-tagged cell constructor alone cannot express variable tail iteration, lookup, append, or folds.

Those obligations now continue in the separate post-K4/M3 K3B bridge. The Cell histories and extensional lookup chapter explains its conservative definitions, seventeen Alpha-only alpha_closed rows, outer-head lookup equations, compact dependency map, and exact WMI closure receipt. That later result does not retroactively move any K3B theorem into strict K3 or Stable. The next K3C validity and membership layer appends seventeen Alpha-only body_checked rows; they fail closed until their repeated isolated WMI receipt is recorded.

Reproducing the boundary#

From the repository root:

make ha-number-theory-check
python3 scripts/verify_arithmetic_knowledge_base.py
python3 scripts/build_peano_library_snapshot.py --check
python3 scripts/build_peano_library_channels.py --check
python3 scripts/verify_peano_library_channels.py
python3 scripts/build_peano_library_channels_v2.py --check
python3 scripts/verify_peano_library_channels_v2.py

The first command checks the 12-layer campaign manifest and all 162 theorem receipts: 95 public evidence rows and 114 closed private candidates. This includes the exact nine-row tranche-01 admission, the exact 16-row K4 admission, eight private gcd conveniences, ten private lcm conveniences, seventy-four strict-K3 signed rows, the private K4 signed-gcd client, the 15-row private pair checkpoint, and the complete M5a–M5f generalized-CRT evidence ladder. The generalized-CRT lane has 29 audited rows: the exact 23 public rows listed above and six closed private residuals. The manifest also pins 25 candidate modules and 34 focused test paths. It checks the 45-row definition API over 44 distinct public-theorem replays. The second cross-checks all 432 public runtime theorems against the 433-row research catalog. The third independently replays the full public ladder and compares the deterministic snapshot. The two v1 channel commands preserve the sealed parent. The final v2 command checks the additive 902-row Alpha publication and unchanged Stable subset; it does not perform the still-pending K3C WMI closure work.

Contents