Skip to content

GaiaFTCL v120 β€” Sovereign Mathematics Substrate goes generally available

Apple Silicon, on-device. No cloud. No external authority. Every mathematical claim is either sealed by two independent gates, blind-tested against an unmodified public reference, or named on the open frontier with the licensing certificate that would close it.

Norwich, Connecticut β€” 2026-05-25 β€” Today GaiaFTCL releases v120, the first generally available version of a sovereign verification substrate that proves its own results through a dual-gate architecture: a Lean 4 kernel constraint (C⁴) and a Swift exact-rational recompute (S⁴) that must agree bit-for-bit before any claim is admitted as true. The cell runs on the operator's Mac β€” Apple Silicon, macOS 26 β€” with zero external cloud dependencies, zero remote LLM calls during a seal, and no ArangoDB or external database in the proof path.

The novelty in this release is the verification discipline, not new mathematics. Forty-five Lean artifacts compile cleanly under Lean 4.12.0; forty of them pass the cell's strict five-gate Lion criterion (zero sorry, zero axiom, zero opaque, currency-clean theorem statement, named falsifier theorem). The remaining five are CURE β€” honestly open, with their open obligations enumerated in the source files themselves. Nineteen standard quantum algorithms carry finite-instance dual-gate seals at textbook parameter sizes (Shor at N=15, Grover at N=4, QFT at N=4, etc.); ten engineering-math PDE domains carry one-step finite seals over exact rationals; and a new HTTP verification node broadcasts the cell's live trust state via RSS 2.0 / Atom 1.0 / JSON Feed 1.1, readable by any iPad, dashboard, or air-traffic-style status board with no integration code.

What this is, plainly

A verification substrate. Not a new factoring algorithm, not a new PQC primitive, not a new cryptographic break. The cell takes finite mathematical claims, processes them through two independent verifiers, and emits a hostile-verifier-reproducible receipt β€” or refuses honestly. The discipline is the product. The 19 quantum-algorithm seals are textbook-instance demonstrations that the dual-gate machinery works end-to-end, not capability claims about quantum computing.

What's in v120

1. Lion Math Domain β€” 40 of 45 Lean artifacts CALORIE-sealed

lake build completes cleanly across all 45 artifacts. Of those:

Bucket Count What it means
CALORIE-sealed 40 Zero sorry, zero axiom, zero opaque. Currency-clean theorem statement. Named falsifier theorem (Gate G4). Lean kernel decide or native_decide closes the certificate.
CURE β€” explicitly open 5 The four files AperyZeta3.lean, PolyaVinogradov.lean, RiemannFunctionalEquation.lean, PQWalletFinance.lean carry a combined 14 sorry instances + 23 opaque definitions as explicit open conjectures with the obligation written into the file header. The fifth, MLKEMConstraint.lean, compiles without sorry but is flagged CURE because its Lean tautologies are not paired with a separately-named falsifier per Gate G4 β€” the cell's auditor catches this.

The cell does not hide its open work. Every sorry and opaque is in source you can grep. The five CURE files are listed in wiki/Lion-Math-Artifacts.md with their gate counts.

Coverage:

Category Files What they seal
Number theory 11 Euler product at N=30 s=2, Bernoulli table, Wilson, Οƒ multiplicativity, MΓΆbius inversion, Bertrand small, Fermat little, Riemann-Robin bounded sweep
Continuum firewall (GAMMA) 1 Ξ“(n+Β½) = cβ‚™Β·βˆšΟ€ with cβ‚™ exact Rat, plus the βˆšΟ€Β·βˆšΟ€ β†’ Ο€ collapse held
Functional equation rung (FUNCEQ) 2 ΞΆ(1βˆ’2n) = βˆ’Bβ‚‚β‚™/(2n) and ΞΆ(2n) = qₙ·π²ⁿ at n=1..3 with qβ‚™ exact and π²ⁿ as an opaque token; Re(s)=Β½ exact rational fixed locus
Quantum algorithms (QC-001..QC-019) 19 Finite-instance dual-gate seals of standard quantum algorithms at textbook parameter sizes. Shor at N=15 (factor 3Β·5), Grover at N=4 (2 qubits), QFT at N=4, QPE at Ο†=ΒΌ, plus VQE/QAOA/VQC/QUBO/HHL/QSVT/qPCA/CTQW/HamSim/BosonSampling/GBS/Steane/Surface/Topological at the smallest non-trivial parameters that stay in exact rational arithmetic.
Engineering math (PDEs) 10 One-step finite seals at small grids: 1D heat, wave, Laplace, Poisson; Maxwell plane-wave dispersion; SchrΓΆdinger 1-qubit; Hooke; DFTβ‚„ of delta; RK4 on ẏ=y; Navier-Stokes rest-state preservation
Algebraic-constraint shapes 2 ML-KEM / Module-LWE relation as a Lean tautology; PQ-wallet keystone theorem (coordinate_does_not_substitute_crypto) as a Lean tautology

Each CALORIE seal has a Swift S⁴ recompute running over RationalBig (BigInt-backed; no Float, no Double, no Int64 overflow) that matches the Lean C⁴ verdict bit-for-bit.

On the quantum-algorithm seals β€” to be precise. Shor at N=15 is the canonical 2001 textbook instance. Grover at N=4 is two qubits. These are not new factorings or new search wins. What's new is that each finite-instance run is sealed by two independent verifiers β€” a Lean kernel and a Swift recompute β€” that must agree byte-for-byte, with every intermediate amplitude staying in exact Rat or RatComplex (no floating-point at any step), and the entire chain is reproducible by a hostile verifier in one command. That's the discipline being demonstrated, applied to algorithms whose correctness was already understood at the parameter sizes shown. The license each seal carries is correspondingly modest: summit.shor.parameterised, summit.grover.parameterised, etc. β€” explicit named obligations to extend the scaffolding to arbitrary parameters (which would require, e.g., a LionSymbol.invSqrt(N) opaque token for non-power-of-4 N).

2. Rosetta-Lion-001 β€” meaning earned from seals

Every CURE-sealed proof becomes one MeaningEntry in a dependency lattice. Meaning is read from the seal, never assigned. The cell's audit alarms on meaning-without-seal with the same severity as a divergence. The lattice currently carries 40 sealed nodes and 7 named open frontier summits, each summit accompanied by the licensing certificate that would close it (e.g., RH ← finite decidable certificate over the FUNCEQ-001/001c critical-axis surface).

3. Inventory Self-Audit β€” internal verification gate

M8InventoryAuditor runs five category audits against the live file system. Each category's count is a count of audit facts β€” discrete claims the auditor verified β€” not a count of artifacts.

βœ“ shebang          COMPLETE  43/43   (43 shell scripts; every one uses zsh)
βœ“ quantumAlgorithm COMPLETE  57/57   (19 algorithms Γ— 3 tiers: registry + Lean + Swift gate)
βœ“ engineeringMath  COMPLETE  10/10   (every PDE domain references a registered Lean file)
βœ“ lionMathProof    COMPLETE  93/93   (every disk file registered + every registry entry on disk + frontier-skeletons accounted for)
βœ“ mcpSurface       COMPLETE  17/17   (11 MCP tools exposed + 6 named future-target slots accounted for)
OVERALL TERMINAL: COMPLETE

The audit's lionMathProof: 93/93 is the registry-consistency check (each artifact Γ— its registration roles); the underlying artifact count remains 45 disk files, 40 CALORIE, 5 CURE.

Exit code 1 if any category drifts. The auditor IS the gate.

4. Verification Node (GFTCL-NODE-001) β€” RSS over HTTP

A single HTTP listener on 127.0.0.1:8423 serves both surfaces from one ledger:

Endpoint Tier Format Auth
/feed/status.xml Public RSS 2.0 none
/feed/status.atom Public Atom 1.0 none
/feed/status.json Public JSON Feed 1.1 none
/feed/divergence.xml Public RSS 2.0 (ATC alarm) none
/feed/summits.xml Public RSS 2.0 (open frontier) none
/feed/{token}/receipts.xml Scoped RSS 2.0 (full receipts) path token
/mcp/health Public JSON none
/ Public HTML index none

Sovereignty boundary verified at release time by direct packet capture: across all five public endpoints, zero substrate internals leak. Public tiers carry verdict + category only; scoped tier carries receipt + reproduction command so a subscriber can re-run any seal locally. ETag + Last-Modified honored, If-None-Match β†’ 304 confirmed live.

5. Open Frontier β€” 7 named summits with licensing certificates

The Rosetta lattice carries 7 named open summits. Each is a terminal state, not a hidden gap: the licensing certificate that would close it is written verbatim in cells/xcode/Sources/M8FrequencySweep/Rosetta/LeanArtifactRegistry.swift and emitted live at /feed/summits.xml.

Summit Statement Required certificate
summit.rh Riemann Hypothesis Finite decidable certificate over the FUNCEQ-001/001c critical-axis surface
summit.funceq.full-xi Full Riemann functional equation as a Lean object Zeta analytic-continuation primitive over LionPrelude (no Mathlib)
summit.apery ΞΆ(3) is irrational Irrational predicate + Beukers integral rate witness
summit.polya-vinogradov Character-sum bound Character sums over Zmod n in LionPrelude
summit.grover.parameterised Grover at arbitrary N LionSymbol.invSqrt(N) opaque token
summit.mlkem.break Sovereign research direction (see Section 6) FoF/MPS contraction over Module-LWE + blind ORACLE CHECK 1 PASS against unmodified pq-crystals reference + bounded dMax
summit.wallet.finance Finance-grade PQ wallet standard met Hardware PUF read interface + concrete M8 wallet conservation formula + PQC FIPS KAT pass + 5 Lean theorems closed without sorry

6. Sovereign research direction: summit.mlkem.break

summit.mlkem.break is a research summit on the open frontier, not a roadmap-to-capability. Its presence in v120 alongside the post-quantum wallet apparatus deserves explicit framing, because a careless read would see a contradiction.

There is none. The cell's posture toward its own cryptographic floor is adversarial. ML-KEM is the wallet's KEM primitive in v120 because it's the NIST-standardised FIPS-203 choice; the cell uses what the regulator accepts. That does not mean the cell trusts the primitive uncritically. summit.mlkem.break is the named cryptanalytic research direction the cell pursues against its own crypto floor β€” the cell would rather find any weakness in ML-KEM internally than have a hostile party find it. The scaffolding ships in CURE-conjecture state with every halt-condition written down: no known classical or quantum algorithm achieves the necessary bounded-bond-dimension recovery at standardised parameters, and the cell will not fabricate a green it has not earned. A real seal here would be a Nobel-class break; the cell does not claim one.

If the cryptographic research community closes ML-KEM (with a bounded-dMax attack or a security reduction that breaks), v120's wallet apparatus rotates to its agility slot (HQC, code-based) β€” the crypto-agility test T9 in the wallet attack suite seals that the rotation is a slot swap, not a re-architecture. Vigilance in the same release as use is the correct posture.

7. Post-Quantum Wallet Apparatus β€” finance-grade verifiability, not finance-grade seal

The PQ-wallet target (GFTCL-OWL-PQWALLET-FINANCE-001) ships in v120 as honest scaffolding under two named halt conditions:

  • HALT-1 β€” Apple Silicon's Secure Enclave does not expose a Physical Unclonable Function as readable integer bytes. The cell refuses to fabricate a PUF fingerprint from /dev/urandom or IORegistry UUID and call it irreproducible.
  • HALT-2 β€” The concrete M8 wallet conservation formula S8 = S4 + Sc is unspecified in the manifold doc at the integer-arithmetic precision a financial security claim requires. The cell refuses to invent the formula and seal the load-bearing theorems against it.

The wallet apparatus's terminal state is CURE-conjecture. It is NOT finance-grade-sealed in v120. What v120 ships is the apparatus whose verifiability is finance-grade β€” the T1-T9 attack suite framework, the Lean theorem skeleton (with sorry honestly carried where the proof is open), the receipt format a regulator would re-run.

A correct one-line summary of where v120 stands on PQ wallets:

A sovereign verification substrate whose sealed claims are finance-grade reproducible, with the post-quantum wallet standard's obligations explicitly named and open.

Not first finance-grade wallet. The wallet is the explicitly named open work.

8. Cryptographic stance

  • PQC primitives: ML-KEM-1024 + ML-DSA-87 + SLH-DSA backup; pq-crystals reference at pinned SHA-256 10b478fc...; FIPS 203/204/205 KAT verification fires when the operator authorises the pull (pre-flight halt in the receipt).
  • Hybrid by default (PQC + classical legs) and crypto-agile (HQC substitution sealed as a slot swap in test T9).
  • Constant-time invariant: any data-dependent timing in key ops = REFUSED at the gate.
  • No Float, no Int64 overflow in any proof or grading path. All arithmetic exact BigInt/Rational.

9. Sovereignty invariants (enforced in code, not in prose)

Invariant Where it's enforced
No external cloud / no remote LLM call during a seal SubstrateBridge is the only door to the gates; inbound-only
No ArangoDB Swift-local SQLite ledger; no remote DB driver in any sealed path
Apple-native HTTP (Network.framework) No third-party HTTP server dependency
127.0.0.1 binding + remote-endpoint filter HTTPListener rejects non-loopback connections at byte-zero
Pinned Lean 4.12.0 + pinned pq-crystals SHA-256 Mismatch on pull = REFUSED
Apple-native zsh (no bash) 10 legacy bash scripts converted; auditor enforces 43/43

Reproduce the release in five commands

A hostile verifier reproduces v120 end-to-end. Every line below was run live by the cell on the day of release. The output you see here is real output, not what-it-will-say-when-it-passes.

git clone https://github.com/gaiaftcl-sudo/gaiaFTCL.git && cd gaiaFTCL

# 1. Lean kernel β€” every artifact compiles (lake build returns 0)
cd proof/lean && lake build && cd ../..

# 2. Lion gate counter β€” substrate truth
bash proof/scripts/count_sorrys.sh

# 3. Dual-gate smoke tests (each ~1s on Apple Silicon)
cd cells/xcode
swift run M8GammaQ001SmokeTest          # continuum firewall β€” SEALED
swift run M8FuncEqQ001SmokeTest         # zeta functional equation β€” SEALED at 001b + 001c
swift run M8GroverN4SmokeTest           # QC-002 finite-instance β€” bit-for-bit match
swift run M8QFTN4SmokeTest              # QC-003 finite-instance β€” bit-for-bit match
swift run M8RosettaLionSmokeTest        # meaning lattice β€” FINALIZED, 40 nodes / 7 summits
swift run M8InventoryAuditor            # internal self-audit (exit 0 = OVERALL COMPLETE)

# 4. CURE-conjecture scaffolding (the honest open work)
swift run M8MLKEMBreakSmokeTest         # ML-KEM cryptanalysis β€” CURE-conjecture, pre-flights named
swift run M8PQWalletSmokeTest           # PQ wallet β€” CURE-conjecture, 3 PASS / 6 blocked

# 5. Bring up the verification node
swift run GaiaNodeServer                # 127.0.0.1:8423
# In another shell:
curl http://127.0.0.1:8423/feed/status.xml          # RSS 2.0 β€” verdict + category, no internals
curl http://127.0.0.1:8423/feed/divergence.xml      # empty (no item) = healthy
curl http://127.0.0.1:8423/feed/summits.xml         # 7 named open summits with certificates
curl http://127.0.0.1:8423/mcp/health               # JSON liveness

v120 release test sweep β€” actual output, run on the cell at release time

Lean kernel               : 45 artifacts, 40 CALORIE-sealed, 5 CURE / open
GAMMA-Q-001               : SEALED β€” continuum firewall PROVEN
FUNCEQ-001                : SEALED (001b 6/6, 001c) β€” 001a remains CURE-conjecture
Grover N=4                : SEALED β€” S4 ↔ C4 bit-for-bit
QFT N=4                   : SEALED β€” S4 ↔ C4 bit-for-bit
Rosetta-Lion-001          : FINALIZED β€” 40 sealed nodes, 7 open summits
Inventory audit           : OVERALL COMPLETE (5/5 categories)
Node server               : 200 on every public endpoint (RSS / Atom / JSON / divergence / summits / health)
Sovereignty boundary      : 0 receipt-internal leaks across 5 public endpoints
HTTP cache contract       : ETag + If-None-Match β†’ 304 confirmed live
JSON Feed 1.1 valid       : parses, version "https://jsonfeed.org/version/1.1", items array present
MLKEM-BREAK scaffolding   : CURE-conjecture, pre-flight halts named in receipt
PQWallet-Finance suite    : 3 PASS / 6 blocked-by-prerequisite / 0 fabricated

If any line above fails to reproduce, the cell's central thesis is wrong and the release is invalid. The cell ships the bet anyway. That's the point.

What this is for

  • For mathematical research: a reproducible substrate where each formal seal is independently verifiable by a hostile party with no privileged access.
  • For regulators and auditors: a sovereign verification harness whose sealed claims are reproducible at the standard a careful audit would demand, with every open obligation explicitly named β€” the PQ wallet apparatus's two halt conditions being the central named-open work.
  • For agent toolkits (Claude Code, Codex, Gemini Desktop): an MCP-routable certification node. Drafts go in; certified verdicts come out; the receipt is what the consumer ships.
  • For anything that watches (iPads, dashboards, ATC-style boards): an RSS endpoint. Subscribe to http://127.0.0.1:8423/feed/divergence.xml and watch silence. An item appearing IS the alarm.

Hard rules baked into v120

  • No Mathlib in LionPrelude β€” the cell carries its own math primitives so the trust base is the cell's, not someone else's.
  • No Float / no Double / no CGFloat in any proof or grading path. Every arithmetic step is exact Rational over arbitrary-precision BigInt.
  • No silent seals. A target that cannot close honestly returns CURE-conjecture with the named obligation. A fabricated CURE is the one unforgivable Red Entropy.
  • Falsifier theorems named per Gate G4: every CALORIE seal duplicates its claim as a separately-named theorem; if the math drifts, both refuse to compile.
  • Inventory audit exit-code-gates further work. The auditor IS the gate. If OVERALL β‰  COMPLETE, MCP exposure of the affected domain halts.

What's open (named on the frontier, not hidden as gaps)

Seven open summits. Each carries the licensing certificate that would close it, written verbatim in LeanArtifactRegistry.swift and emitted live at /feed/summits.xml. RH stays open. ApΓ©ry stays open. The PQ wallet standard stays open under two named halt conditions. ML-KEM cryptanalysis stays open with the explicit framing that no known algorithm reaches the necessary bound.

A named open summit is a terminal state, not a hidden gap. That distinction is the entire reason the cell can be trusted on what it does claim.

Roadmap (post-v120, in named-obligation order)

  1. MCP Streamable HTTP transport β€” merge the existing stdio MCP tools (11) into the same HTTP listener as RSS. One process, two transports, one ledger. Named on summit.node.unified-transport.
  2. pq-crystals reference pull at pinned SHA-256 β€” closes the wallet apparatus's Layer-1 KAT obligation and unlocks T6/T7 of the wallet attack suite.
  3. Heat / wave / Laplace / Poisson multi-step seals β€” extend the one-step finite seals to parameterised families with uniform-stability bounds.
  4. MCP-served seal request flow β€” gaiaftcl.seal_claim returns CURE / REFUSED / CURE-conjecture with the receipt agent toolkits can embed.
  5. Hardware PUF research β€” close HALT-1 of the wallet apparatus, contingent on Apple Silicon (or equivalent) exposing per-die entropy at a level the regulator accepts.

Repositories

  • Code + Lean: https://github.com/gaiaftcl-sudo/gaiaFTCL
  • Wiki: https://github.com/gaiaftcl-sudo/gaiaFTCL/wiki
  • Receipt formats (RSS 2.0 + Atom 1.0 + JSON Feed 1.1): http://127.0.0.1:8423/feed/* after swift run GaiaNodeServer

Licensing + IP

The cell is the sole licensable substrate of GaiaFTCL. Β© 2026 Richard Gillespie. All rights reserved. USPTO patent applications 19/460,960 and 19/096,071 filed by Rick Gillespie as named inventor of record.

About GaiaFTCL

GaiaFTCL is a sovereign Mac cell β€” Apple Silicon, on-device β€” that provides a dual-gate verification substrate for mathematical and cryptographic claims. The cell binds a Lean 4 kernel (C⁴ constraint) with a Swift exact-rational recompute (S⁴ manifest) so no verdict crosses any boundary unless both gates agree bit-for-bit. v120 is the first generally available version. The Manifold is Holding. Calories or Cures.

Federation-cosigned

This page's source is sealed in the GaiaFTCL federation manifest β€” page SHA-256 da7c8b9947c59209…, manifest witness a090592e0609adc8…, signed 2026-06-02T18:58:22Z by cell gaiaftcl-mac-cell. Verify with gaiaftcl wiki sign --all and compare wiki-all-signatures.json.