Mirrored from https://github.com/SNAPKITTYWEST/foundry-j at commit cee36b3. Part of the SnapKitty October 2026 main drop.

foundry-j

A pure-J recreation of the mathematical cores of Foundry F1: the Goldilocks prime field, prime monomial matrices, the spectral contraction governor, and the additive Banach recurrence — each property traced to a source line and checked by a J harness.

---

Abstract

Foundry F1 is a C++/C99 system whose lowest layer is a small, self-contained body of mathematics: arithmetic in the 64-bit Goldilocks prime field, a sparse signed-matrix type graded by prime monomials, a Gershgorin and power-iteration spectral test, and a contraction recurrence

$$x_{t+1}={\mathrm{\Xi }}_t\cdot x_t+{\mathrm{\Lambda }}_t\cdot T(x_t)+g_{t}x\_\{t+1\}\; =\; \backslash Xi\_t\; \backslash cdot\; x\_t\; +\; \backslash Lambda\_t\; \backslash cdot\; T(x\_t)\; +\; g\_t$$

whose step is kept contractive by a soft projection of its weight schedules. Around that core the upstream project builds orchestration: audit chains, seals, gates, certificates, and hardware.

This repository recreates only the mathematics, in J, with no other runtime. The work proceeds from an inventory of fifty-six numbered properties extracted from the upstream sources, each with a file:line citation, through a frozen J API, to a verification harness that tests every property and prints one verdict line per check. The latest run on disk reports 61 PASS, 0 FAIL, 4 SKIP; the four skips are properties that are narrative or system-level rather than mathematical.

The repository is also the reference against which the sibling project HCALC states what it borrows and what it does not.

---

1. Purpose and method

There are two reasons to recreate a numerical core in a second language. The first is to understand it: an array language forces every reduction, every boundary case, and every implicit cast in the original to be made explicit. The second is to have an independent oracle: when two implementations of the same property agree on the same inputs, and the property is pinned to a line of the original, disagreement anywhere downstream becomes a precise question rather than a vague suspicion.

foundry-j follows a fixed method:

1. Inventory. spec/PROPERTIES.md lists 56 properties of the upstream mathematics. Each one cites a header, a source file, a test, or a README section. Numeric constants are copied, never invented.
2. Gap rulings. Where upstream prose and upstream code disagree, spec/GAP_DECISIONS.md records a ruling. The default policy is match the C++ as coded, unless the prose is the only statement of an identity.
3. API. spec/J_API.md fixes nouns, verbs, ranks, and record field orders. j/BOXING.md freezes how multi-field records are boxed so that J's link operator never flattens them.
4. Core. The J sources under j/ implement the API in a single locale, foundry.
5. Verify. The harness under verify/ loads the core, runs one check per property plus nine named baseline tests, and writes a timestamped log.

---

2. The Goldilocks prime field

2.1 The prime

$$p=2^{64}-2^{32}+1=18446744069414584321=\mathtt{0}\mathtt{x}\mathtt{F}\mathtt{F}\mathtt{F}\mathtt{F}\mathtt{F}\mathtt{F}\mathtt{F}\mathtt{F}\mathtt{00000001}\mathrm{.}p\; =\; 2^\{64\}\; -\; 2^\{32\}\; +\; 1\; =\; 18446744069414584321\; =\; \backslash mathtt\{0xFFFFFFFF00000001\}.$$

Field elements are integers $0 \le v < p$. In J the modulus is the extended-precision noun GOLDILOCKS_PRIME (alias p), and all field verbs promote their arguments to extended integers with x:, so intermediate sums and products never wrap.

2.2 Why this prime reduces cheaply

The prime is chosen so that powers of two fold back into small expressions. From $p = 2^{64} - 2^{32} + 1$,

$$2^{64}\equiv 2^{32}-1(\mathrm{m}\mathrm{o}\mathrm{d}p),2^{96}=2^{32}\cdot 2^{64}\equiv 2^{64}-2^{32}\equiv -1(\mathrm{m}\mathrm{o}\mathrm{d}p)\mathrm{.}2^\{64\}\; \backslash equiv\; 2^\{32\}\; -\; 1\; \backslash pmod\{p\},\; \backslash qquad\; 2^\{96\}\; =\; 2^\{32\}\; \backslash cdot\; 2^\{64\}\; \backslash equiv\; 2^\{64\}\; -\; 2^\{32\}\; \backslash equiv\; -1\; \backslash pmod\{p\}.$$

Write a 128-bit product as $a \cdot b = \mathrm{lo} + 2^{64},\mathrm{hi}$ and split the high word as $\mathrm{hi} = \mathrm{hi_{lo}} + 2^{32},\mathrm{hi_{hi}}$, with $\mathrm{lo} < 2^{64}$ and $\mathrm{hi_{lo}}, \mathrm{hi_{hi}} < 2^{32}$. Then

$$a\cdot b\equiv \mathrm{l}\mathrm{o}+(2^{32}-1)\mathrm{h}{\mathrm{i}}_{\mathrm{l}\mathrm{o}}-\mathrm{h}{\mathrm{i}}_{\mathrm{h}\mathrm{i}}(\mathrm{m}\mathrm{o}\mathrm{d}p)\mathrm{.}a\; \backslash cdot\; b\; \backslash equiv\; \backslash mathrm\{lo\}\; +\; (2^\{32\}\; -\; 1)\backslash ,\backslash mathrm\{hi\_\{lo\}\}\; -\; \backslash mathrm\{hi\_\{hi\}\}\; \backslash pmod\{p\}.$$

This is the reduction identity of properties 5–9. The constant $2^{32} - 1 = 4294967295$ is the fold constant, named EPSILON in the upstream README and EPSILON_FOLD here.

2.3 The fold as coded

fp_mulmod follows the upstream algorithm step by step (properties 7–11):

1. Form the product and split it: lo = product mod 2^64, hi = floor(product / 2^64).
2. Split the high word: hi_lo = hi mod 2^32, hi_hi = floor(hi / 2^32).
3. Fold: folded = lo + hi_lo * EPSILON_FOLD.
4. Subtract with underflow handling: if folded >= hi_hi then reduced = folded - hi_hi, else reduced = folded + p - hi_hi.
5. Final conditional reduction: if reduced >= p then subtract $p$ once.

One subtraction suffices in the last step. The largest possible fold is $(2^{64} - 1) + (2^{32} - 1)^2 = 2^{65} - 2^{33}$, which is below $2p = 2^{65} - 2^{33} + 2$; hence after removing $\mathrm{hi_{hi}}$ the value is below $2p$ and one conditional subtraction lands it in $[0, p)$.

A source comment in fp_mulmod records the one subtle point: upstream extracts hi_lo with the bit mask hi & 0xFFFFFFFF, which is reduction modulo $2^{32}$, not modulo the fold constant $2^{32} - 1$. Getting that wrong produces a multiplication that looks plausible on small inputs and breaks on products whose high word is large — which is exactly where exponentiation, and hence inversion, spends its time.

2.4 Field operations

Verb	Definition	Property
fp_reduce	$x - p$ if $x \ge p$, else $x$ (single limb)	12
fp_add	$a + b$, minus $p$ if the sum reaches $p$	13
fp_sub	$a - b$, plus $p$ on underflow	14
fp_mul	fp_mulmod	15
fp_pow	square-and-multiply from result = 1, base = a	17
fp_inv	Fermat: $a^{-1} = a^{p-2} \bmod p$	16
fp_add_batch, fp_mul_batch	element-wise over lists	18

Fermat inversion is correct because $p$ is prime: for $a \not\equiv 0$, $a^{p-1} \equiv 1$, so $a \cdot a^{p-2} \equiv 1$. The harness checks it on the upstream test value $a = 42$.

---

3. Named constants

The upstream header include/types.h defines constants beyond the field. foundry-j reproduces them exactly, because other layers and other repositories cite them:

Noun	Value	Property	Note
K_MAX	133144	19	upstream: maximum W8A8 accumulation
MAX_DRIFT	300000000000000000	20	upstream: drift bound, $3 \times 10^{17}$
PIRTM_MAGIC	0x7F504952	21	bytecode magic \x7FPIR
PHI	1.618033988749895	22	present upstream; no consuming identity in the math sources
P64 (alias P_64)	2, 3, 5, …, 311	23	the first 64 primes
GENESIS_HASH_SIZE	32	24	recorded, not used by the math cores
tier_eps	T1: 0.10, T2: 0.05, T3: 0.02, T4: 0.01; default 0.10	25	contraction margins $\varepsilon$

$P_{64}$ and the tier margins are the two constants that matter most outside this repository: HCALC builds its prime-weighted transform from $P_{64}$ and takes its default margin from tier T2, and sedona-k uses $P_{64}$ as the mode set of its Riemann gas.

---

4. Prime monomial matrices (PMAT)

A PMAT is a sparse matrix whose non-zero entries are signs, each tagged with a signature — a pair of integer grades $(\delta_{\mathrm{src}}, \delta_{\mathrm{tgt}})$ called the entry's monomial. In J a PMAT is the triple rows ; cols ; entries, where each entry row is sign, ds, dt, row, col.

4.1 Insertion (properties 26–28)

pmat_insert rejects an entry if row >= rows, col >= cols, or the sign is not $\pm 1$, and otherwise appends it. Upstream documentation states a grading condition — target signature minus source signature equals the monomial — but the upstream code never checks it, and validate_grading always returns true. Gap ruling 3 is to mirror the code: pmat_validate_grading returns 1, and insertion performs domain checks only. The stated condition is recorded as a possible future upgrade, not as a property of this core.

4.2 Conservation (property 29)

The conservation law says that the component-wise sum of all entry monomials equals the accumulated signature:

$$\sum _{e\in M}({\delta }_{\mathrm{s}\mathrm{r}\mathrm{c}}(e),{\delta }_{\mathrm{t}\mathrm{g}\mathrm{t}}(e))=({\mathrm{\Sigma }}_{\mathrm{s}\mathrm{r}\mathrm{c}},{\mathrm{\Sigma }}_{\mathrm{t}\mathrm{g}\mathrm{t}})\mathrm{.}\backslash sum\_\{e\; \backslash in\; M\}\; \backslash left(\backslash delta\_\{\backslash mathrm\{src\}\}(e),\backslash \; \backslash delta\_\{\backslash mathrm\{tgt\}\}(e)\backslash right)\; =\; \backslash left(\backslash Sigma\_\{\backslash mathrm\{src\}\},\backslash \; \backslash Sigma\_\{\backslash mathrm\{tgt\}\}\backslash right).$$

The upstream test inserts monomials $(3,5)$, $(1,2)$, $(2,1)$ and expects $(6,8)$; the harness reproduces that case.

4.3 Composition (properties 30–31)

For $A$ of shape $r_A \times c_A$ and $B$ of shape $r_B \times c_B$, the composite has shape $r_A \times c_B$. For each output cell $(i,j)$ and each pair of entries $a$ in row $i$ of $A$ and $b$ in column $j$ of $B$ with matching inner index ($a.\mathrm{col} = b.\mathrm{row}$), the code accumulates

$$\sigma \leftarrow \sigma \cdot \mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}(a)\cdot \mathrm{s}\mathrm{i}\mathrm{g}\mathrm{n}(b),{\delta }_{\mathrm{s}\mathrm{r}\mathrm{c}}\leftarrow {\delta }_{\mathrm{s}\mathrm{r}\mathrm{c}}+{\delta }_{\mathrm{s}\mathrm{r}\mathrm{c}}(a),{\delta }_{\mathrm{t}\mathrm{g}\mathrm{t}}\leftarrow {\delta }_{\mathrm{t}\mathrm{g}\mathrm{t}}+{\delta }_{\mathrm{t}\mathrm{g}\mathrm{t}}(b)\mathrm{.}\backslash sigma\; \backslash leftarrow\; \backslash sigma\; \backslash cdot\; \backslash mathrm\{sign\}(a)\; \backslash cdot\; \backslash mathrm\{sign\}(b),\; \backslash qquad\; \backslash delta\_\{\backslash mathrm\{src\}\}\; \backslash leftarrow\; \backslash delta\_\{\backslash mathrm\{src\}\}\; +\; \backslash delta\_\{\backslash mathrm\{src\}\}(a),\; \backslash qquad\; \backslash delta\_\{\backslash mathrm\{tgt\}\}\; \backslash leftarrow\; \backslash delta\_\{\backslash mathrm\{tgt\}\}\; +\; \backslash delta\_\{\backslash mathrm\{tgt\}\}(b).$$

Only the source grade of the left factor and the target grade of the right factor are accumulated. A fuller reading of the upstream prose ("sum of both signatures") would add all four; gap ruling 4 keeps the coded rule.

4.4 Norm (property 32)

Every entry has magnitude one, so the Frobenius norm is the square root of the entry count:

$$\parallel M{\parallel }_F=\sqrt{\mathrm{\#}\mathrm{e}\mathrm{n}\mathrm{t}\mathrm{r}\mathrm{i}\mathrm{e}\mathrm{s}(M)}\mathrm{.}\backslash lVert\; M\; \backslash rVert\_F\; =\; \backslash sqrt\{\backslash \#\backslash mathrm\{entries\}(M)\}\; .$$

---

5. The spectral governor

The governor answers one question: is a Jacobian $J \in \mathbb{R}^{n \times n}$ safely contractive with margin $\varepsilon$?

5.1 Gershgorin bound (properties 33–34)

For each row $i$, the Gershgorin disc has centre $J_{ii}$ and radius $R_i = \sum_{j \ne i} \lvert J_{ij} \rvert$. The bound is the farthest reach of any disc from the origin:

$$G(J)=\underset{i}{\max }(\mid J_{ii}\mid +\sum _{j\mathrm{\ne }i}\mid J_{ij}\mid )\mathrm{.}G(J)\; =\; \backslash max\_i\; \backslash left(\; \backslash lvert\; J\_\{ii\}\; \backslash rvert\; +\; \backslash sum\_\{j\; \backslash ne\; i\}\; \backslash lvert\; J\_\{ij\}\; \backslash rvert\; \backslash right).$$

$J$ is declared contractive when $G(J) < 1 - \varepsilon$. Note that $G(J)$ is exactly the maximum absolute row sum, i.e. the operator norm of $J$ induced by $\ell_\infty$. It therefore bounds the spectral radius from above, and it is a Lipschitz constant of the linear map $x \mapsto Jx$ in the sup norm — which is why HCALC, whose metric is $\ell_\infty$, can use it directly.

5.2 Power iteration (properties 35–36)

Starting from the uniform unit vector, iterate $v \leftarrow Jv / \lVert Jv \rVert_2$ and track the Rayleigh quotient $\lambda \approx v^{\top} J v$. Stop when successive estimates differ by less than $10^{-12}$ or after 100 iterations, and return $\lvert \lambda \rvert$. The same predicate, $\lvert \lambda \rvert < 1 - \varepsilon$, defines contractivity.

5.3 Fallback policy (property 37)

spectral_analyze tries Gershgorin first. If Gershgorin reports contractive and the bound lies within five percent of the margin, $G(J) > 0.95,(1 - \varepsilon)$, the result is recomputed by power iteration. The returned record (SpectralResult) carries the spectral-radius estimate, the verdict, both bounds, and a flag saying whether power iteration was used.

5.4 Reference cases (property 38)

The upstream tests use $\varepsilon = 0.1$, so the margin is $0.9$:

J_1 = \begin{bmatrix} 0.2 & 0.1 \\ 0.05 & 0.15 \end{bmatrix}, \qquad
J_2 = \begin{bmatrix} 0.9 & 0.3 \\ 0.3 & 0.95 \end{bmatrix}.

For $J_1$ the row sums are $0.3$ and $0.2$, so $G(J_1) = 0.3 < 0.9$: contractive. For $J_2$ they are $1.2$ and $1.25$, so $G(J_2) = 1.25$: not contractive. The harness reproduces both verdicts as the named tests spectral_contractive and spectral_expansive.

---

6. The Banach recurrence

6.1 The step (properties 39–40)

$$x_{t+1}={\mathrm{\Xi }}_t\cdot x_t+{\mathrm{\Lambda }}_t\cdot T(x_t)+g_t\mathrm{.}x\_\{t+1\}\; =\; \backslash Xi\_t\; \backslash cdot\; x\_t\; +\; \backslash Lambda\_t\; \backslash cdot\; T(x\_t)\; +\; g\_t\; .$$

The contraction condition is

and when it holds uniformly the map is a strict contraction, so Banach's theorem gives a unique fixed point (property 41). That last statement is upstream narrative — the code checks $q_t$ at each step but does not prove the theorem — so the harness records property 41 as SKIP rather than claiming it.

6.2 How $q$ is estimated in the step (property 42)

As coded, $q$ is an inexpensive, state-dependent estimate:

$$q=n_{\mathrm{\Xi }}+n_{\mathrm{\Lambda }}\cdot n_T,n_{\mathrm{\Xi }}=\underset{i}{\max }\mid {\mathrm{\Xi }}_i\mid ,n_{\mathrm{\Lambda }}=\underset{i}{\max }\mid {\mathrm{\Lambda }}_i\mid ,n_T=\frac{\parallel T(x){\parallel }_{\mathrm{\infty }}}{\parallel x{\parallel }_{\mathrm{\infty }}},q\; =\; n\_\{\backslash Xi\}\; +\; n\_\{\backslash Lambda\}\; \backslash cdot\; n\_T,\; \backslash qquad\; n\_\{\backslash Xi\}\; =\; \backslash max\_i\; \backslash lvert\; \backslash Xi\_i\; \backslash rvert,\; \backslash quad\; n\_\{\backslash Lambda\}\; =\; \backslash max\_i\; \backslash lvert\; \backslash Lambda\_i\; \backslash rvert,\; \backslash quad\; n\_T\; =\; \backslash frac\{\backslash lVert\; T(x)\; \backslash rVert\_\backslash infty\}\{\backslash lVert\; x\; \backslash rVert\_\backslash infty\},$$

where the division in $n_T$ is skipped when $\lVert x \rVert_\infty \le 10^{-15}$.

6.3 Soft projection (property 43)

If $q > 1 - \varepsilon$, both weight vectors are rescaled before the update:

$$(\mathrm{\Xi },\mathrm{\Lambda })\leftarrow \frac{1-\epsilon }{q}\cdot (\mathrm{\Xi },\mathrm{\Lambda }),(\backslash Xi,\; \backslash Lambda)\; \backslash leftarrow\; \backslash frac\{1\; -\; \backslash varepsilon\}\{q\}\; \backslash cdot\; (\backslash Xi,\; \backslash Lambda),$$

and $q$ is re-estimated. The StepInfo record notes that a projection occurred. This is the operation HCALC's in-step governor is a cousin of; the difference is that soft_project scales the schedules, not the state.

6.4 Weight synthesis (property 44)

synth_weights builds per-step schedules from a tier and a profile. With $q^{\star} = 1 - \varepsilon_{\mathrm{tier}}$ and a profile factor $f_t$,

$${\xi }_t=0.7q^{\star }{f}_t,{\lambda }_t=0.3q^{\star }{f}_t,\backslash xi\_t\; =\; 0.7\backslash ,\; q^\{\backslash star\}\; f\_t,\; \backslash qquad\; \backslash lambda\_t\; =\; 0.3\backslash ,\; q^\{\backslash star\}\; f\_t,$$

where $f_t = 1$ (Uniform), $f_t = 1/(t+1)$ (Harmonic), or $f_t = 1/\ln(t+2)$ (LogDecay). As coded, each schedule row has length two and component $i$ reads entry $\min(i, 1)$; the $\Xi$ row is $(\xi_t, 0)$ and the $\Lambda$ row is $(0, \lambda_t)$. The 70/30 split makes $\xi_t + \lambda_t = q^{\star} f_t$, so with $n_T \le 1$ the step estimate of §6.2 satisfies $q \le q^{\star} f_t$. For the Uniform and Harmonic profiles $f_t \le 1$ and the schedule starts inside the margin; LogDecay begins at $f_0 = 1/\ln 2 \approx 1.44$, and its early steps rely on the soft projection of §6.3.

6.5 Projector and residual (properties 45–46)

After the affine update, an optional projector hook is applied (the upstream test clips to $[-1, 1]$; the default in rec_run is the identity verb). The residual is the Euclidean step length,

$$r_t=\parallel x_{t+1}-x_t{\parallel }_2,r\_t\; =\; \backslash lVert\; x\_\{t+1\}\; -\; x\_t\; \backslash rVert\_2\; ,$$

and rec_run stops when $r_t$ falls below the tolerance (default $10^{-6}$) or the step cap (default 200) is reached. It returns the list of per-step StepInfo records and sets REC_STATE to the final state, the convergence flag, and the history.

---

7. Emission, CSL, and certificate arithmetic

The upstream gate and certification layers contain a few scalar formulas that consume the recurrence's outputs. They are mathematics, not orchestration, so they are recreated and tested (properties 48–54):

• Emission policies (emit_apply): pass-through; suppress (emit zeros if $q \ge 1 - \varepsilon$); hold (emit the previous output under the same condition); and attenuate, which multiplies the output by $\max(0, 1 - \varepsilon - q)$.
• CSL neutrality: fail if some pair with $\lvert x_i - x_j \rvert > 10^{-15}$ has $\lvert T_i - T_j \rvert / \lvert x_i - x_j \rvert > 1 + \varepsilon$.
• CSL beneficence: require $\lVert T(x) \rVert_2 \le (1 + \varepsilon) \lVert x \rVert_2$ and residual at most $(1 + \varepsilon) \lVert x \rVert_2$.
• CSL commutation: require $\lVert \mathrm{filter}(T(x)) - T(\mathrm{filter}(x)) \rVert_\infty \le \varepsilon$.
• Certificate arithmetic (ace_certify over a StepInfo history): with $q_{\max}$ the largest step estimate,

and the tail bound is $+\infty$ when $q_{\max} \ge 1$.

The tail bound is the standard a-posteriori Banach estimate: if each step contracts by at most $q_{\max}$, the remaining distance to the fixed point is bounded by the last step length divided by $1 - q_{\max}$.

What is not recreated is the machinery those formulas sit inside: seal chains, multi-party locks, guardians, and consensus. Their properties (47, 55, 56) are recorded in the inventory and skipped by the harness.

---

8. Repository layout, API, and verification

8.1 Layout

foundry-j/
  LICENSE                GNU AGPL v3
  README.md              this document
  spec/
    PROPERTIES.md        56 numbered properties with source citations
    J_API.md             nouns, verbs, ranks, record field orders
    GAP_DECISIONS.md     rulings where upstream prose and code disagree
    COVERAGE_MATRIX.md   property-to-harness coverage at an earlier commit
    HCALC_CROSSLINKS.md  Foundry properties relevant to HCALC
    HCALC_PRODUCTION_REVIEW.md   review of HCALC PRODUCTION.md
    LICENSE_NOTE.txt
  j/
    foundry.ijs          loader: types, goldilocks, pmat, spectral,
                         recurrence, gate, certify; foundry_export
    types.ijs            constants, tiers, enums
    goldilocks.ijs       field arithmetic
    pmat.ijs             prime monomial matrices
    spectral.ijs         Gershgorin, power iteration, analyze
    recurrence.ijs       synth_weights, soft_project, q_estimate,
                         rec_step, rec_run
    gate.ijs             emission and CSL checks
    certify.ijs          certificate arithmetic
    BOXING.md            record boxing contracts
  verify/
    run.sh, run.ijs, harness.ijs
    tests/               goldilocks, constants, pmat, spectral,
                         recurrence, emit_csl_ace
    PROPERTY_MAP.md      property-to-harness map
    INVENTORY.md         named tests and coverage files
    logs/                timestamped runs
  docs/images/           harness screenshot

8.2 Using the core

load 'j/foundry.ijs'      NB. verbs live in locale foundry
foundry_export ''         NB. optional: copy the public names into base

42 fp_mul fp_inv 42       NB. 1
P64                       NB. 2 3 5 ... 311
tier_eps T2               NB. 0.05

Records follow j/BOXING.md. The three that matter most:

Record	Fields, in order
StepInfo	step, q, epsilon, n_xi, n_lam, projected, residual
SpectralResult	spectral_radius, contractive, gershgorin_bound, power_iter_bound, used_power_iteration
AceCert	lipschitz_upper, safety_margin, tail_bound, certified

rec_step returns x_next ; <StepInfo>, always of length two, so a caller can unpack it without worrying about J's link operator splicing record fields into the outer list.

8.3 Running the harness

Requires J with jconsole. The wrapper defaults to /home/box/j/j9.7/bin/jconsole; set JCONSOLE to override.

cd verify
./run.sh                  # writes logs/run-YYYYMMDD-HHMMSS.log
# or directly:
jconsole verify/run.ijs

Each line is PASS name, FAIL name: reason, SKIP name: reason, or BLOCKED name: missing …. The harness exits non-zero on any failure.

---

9. Measured results

Source: verify/logs/run-20261007-080122.log, J 9.7.1, stamped 2026-10-07 08:01:22 PDT.

PASS=61 FAIL=0 SKIP=4 BLOCKED=0
exit_code=0

Section	Checks in log	PASS	SKIP
goldilocks	4 named tests + properties 1–18	22	0
constants	properties 19–25	7	0
pmat	2 named tests + properties 26–32	9	0
spectral	2 named tests + properties 33–38	8	0
recurrence	1 named test + properties 39–46	8	1 (property 41)
emit / CSL / ACE	properties 47–56	7	3 (properties 47, 55, 56)
total	9 named tests + 56 properties	61	4

The skips and their logged reasons:

Property	Reason in log
41	narrative-only Banach guarantee
47	WORM/seal chain / triple-lock theater out of harness scope
55	no Core guardian verb (gate theater out of harness scope)
56	narrative-only consensus / $2^{-256}$ bound

How the count got here

The logs directory keeps the earlier runs, and the history is informative:

• The first runs (06:12–06:18 PT) exercised only the nine named tests. After initial load and wiring errors were cleared, Fermat inversion failed in three consecutive runs, with 42 * fp_inv 42 returning 11152786313141180820 instead of 1. Once the field core was corrected, the named tests reached 9/9 (run-20261007-061853.log).
• The run at 07:59 PT (run-20261007-075943.log) was the first to cover all 56 properties and reported PASS=59 FAIL=2 SKIP=4. The failures were property 49 (attenuation scale) and property 50 (CSL neutrality), both caused by J's right-to-left evaluation order in expressions transcribed from C++.
• Those two were fixed (commit f8ab694), and the run at 08:01 PT is the current result.

verify/PROPERTY_MAP.md and spec/COVERAGE_MATRIX.md cite earlier logs in places; the log above is the authoritative current measurement.

---

10. Relationship to sibling repositories

HCALC

HCALC defines a nested recurrence,

$$X_{t+1}=\mathrm{\Xi }(t,{\mathrm{\Lambda }}_m\cdot C(T_p(X_t))),X\_\{t+1\}\; =\; \backslash Xi\backslash left(t,\backslash \; \backslash Lambda\_m\; \backslash cdot\; C\backslash left(T\_p(X\_t)\backslash right)\backslash right),$$

on $\mathbb{R}^n$ with a prime-weighted diagonal transform built from $P_{64}$. Its core loads this repository and cites exactly two things: the list P64 and the estimator spectral_analyze. It does not call soft_project or rec_step.

The two recurrences are related by an explicit parameter table that HCALC calls InstanceBridge ($T := C \circ T_p$, $\Lambda := \Lambda_m \cdot \mathbf{1}$, $\Xi := \xi_t$). Under that table, the additive step of §6.1 evaluated on HCALC inputs differs from HCALC's nested step by the drift term $\xi_t \cdot x$, so the two are distinct maps. The Foundry J review of HCALC's production specification, kept in spec/HCALC_PRODUCTION_REVIEW.md, accepts the bridge as a non-identity morphism and rejects any reading of HCALC's step as property 39. In particular:

• HCALC's state-level governor reuses the scale factor $(1 - \varepsilon)/q$ of property 43 but is not property 43;
• HCALC's weight law $\alpha_j = 1/(1 + \ln p_{j \bmod 64})$ is HCALC's own definition, not a Foundry property;
• HCALC's residual uses $\ell_\infty$, whereas property 46 uses $\ell_2$.

A passing foundry-j harness therefore says nothing about HCALC beyond the correctness of the two cited hooks.

sedona-k

sedona-k takes the Goldilocks prime, the fold constant, and $P_{64}$ from j/types.ijs and computes Riemann-gas thermodynamics over $P_{64}$ in ngn/k. It uses no field arithmetic, PMAT, governor, or recurrence.

david

david is an unrelated product (sparse agent routing in J, PostgreSQL/pgvector, and Prolog). It shares the J toolchain and nothing else.

---

11. Out of scope

• The upstream orchestration layers: SHA-256 audit and seal chains, multi-party locks, guardians, publishers, consensus, and their certificates as system objects.
• The bytecode linker associated with PIRTM_MAGIC (the constant is recorded; the linker is not recreated).
• Hardware and hardware-verification trees in the upstream project.
• Barrett reduction (upstream defines a constant for it and never uses it; gap ruling 2).
• Enforcement of the stated PMAT grading condition (gap ruling 3).
• A Lean or Alloy formalization of these cores. foundry-j is executable and tested, not proved.
• Continuous-integration workflows. The harness is run locally and its logs are committed.

Upstream reference (not shipped here): https://github.com/SNAPKITTYWEST/SNAPKITTYWEST/tree/main/cpp-foundry.

---

12. Demo

---

13. License

Copyright © 2026 Foundry J contributors.

This repository is distributed under the GNU Affero General Public License, version 3 only — see LICENSE. SPDX identifier: AGPL-3.0-only.

Some file headers inherited from earlier drafts (for example under verify/ and parts of spec/ and j/) still carry AGPL-3.0-or-later tags or "version 3 or later" wording; they have not yet been aligned with the repository-level choice stated here.

💼 Commercial License

SnapKitty code is free and open under AGPL-3.0 for open-source use. Building a commercial product or service? A proprietary commercial license from Snapkitty Collective LLC lets you ship this code without the AGPL's source-sharing and network-use obligations.

→ Get a commercial license · A.parr@belespritdaccord.uk