Skip to content

Lion Math — Roar Pack v115

The cell closed nine finite-exact rational identities. Each artifact was checked by two independent gates that agreed bit-for-bit. The Swift internal gate's earned trust ledger now stands at 24 of 24 public artifact runs, 0 divergences, pinned against leanprover/lean4:v4.12.0.

Give the cell the inputs. The cell gives back the guaranteed output.

The nine roars

Each row is a public lion: zero sorry, zero axiom, zero opaque; lake build exit 0; the Lean kernel's decide is the proof; the Swift exact-Rat checker reproduces the same forced output; lion_gate_agreement row sealed with agree=1.

# Theorem ID Claim Forced output Lean file
1 euler_product truncatedEulerProduct(10,2) = smoothNumberSum(10,2) over NSmooth(10) 14365 / 9072 FirstRoars/EulerProduct.lean
2 euler_family_N12_s2 Same identity at (N=12, s=2) — adds prime 11; expands K₂ to 3 876265 / 548856 FirstRoars/EulerProductFamily.lean
3 euler_family_N6_s3 Same identity at (N=6, s=3) — cubed exponents 3577 / 3000 FirstRoars/EulerProductFamily.lean
4 euler_family_N6_s4 Same identity at (N=6, s=4) — fourth powers 1167803 / 1080000 FirstRoars/EulerProductFamily.lean
5 mobius_inversion_N10 Σ_{d \| n} μ(d) = [n = 1] for every n ∈ NSmooth(10) (48 integers checked) all-true witness FirstRoars/MobiusInversion.lean
6 sigma_multiplicative σ(m·n) = σ(m)·σ(n) for 8 coprime pairs {(6,35), (10,21), (15,28), (4,9), (8,27), (16,81), (25,49), (2,3)} all-true witness FirstRoars/SigmaMultiplicative.lean
7 wilson_primes_up_to_30 (p−1)! mod p = p − 1 for every prime p ≤ 30 (10 primes checked) all-true witness FirstRoars/WilsonTheorem.lean
8 fermat_little_p20_a18 a^(p−1) ≡ 1 (mod p) for every prime p ≤ 20 and base a ∈ 1..18 with gcd(a, p) = 1 all-true witness FirstRoars/FermatLittle.lean
9 bertrand_up_to_100 For every 1 ≤ n ≤ 100, there is a prime p with n < p ≤ 2n all-true witness FirstRoars/BertrandSmall.lean

"All-true witness" means the Lean theorem reduces to a single Boolean true via decide on the conjunction of every individual claim in the file's finite range. The Swift mirror walks the same range and returns .calorie(forcedOutput: 1/1) — a canonical confirmation that every per-instance equality held. Any single failure flips the Boolean to false and the file refuses to compile.

The dual gate — one ruleset, nine artifacts

For each of the nine roars:

  1. The Swift internal gate (SwiftRatGate.swift + SwiftNumberTheory.swift) runs the exact-Rat / exact-Nat computation on-device. Zero Float. Zero external dependency. Returns .calorie(forcedOutput:), .refused(...), or .cannotEvaluate(...).
  2. The Lean external warrant (proof/scripts/lean_gate.sh) builds the artifact via the pinned lake, counts sorry/axiom/opaque, returns one JSON verdict.
  3. DualGateHarness.gateWithSwift(...) seals one lion_gate_agreement row in substrate. CALORIE/CALORIE → agree=1. Any disagreement → agree=0 AND is_public_artifact=0 (a caught Swift bug never becomes a public lion).

Earned-trust ledger (live)

Metric Value
Public artifacts checked 24
Swift ↔ Lean agreements 24
Divergences (caught Swift bugs) 0
Pinned Lean toolchain leanprover/lean4:v4.12.0

The cell has now crossed the earned-autonomy threshold with one safety margin to spare:

  • Threshold: 20 public agreements, 0 divergences.
  • Current: 24 public agreements, 0 divergences.

Per the directive: while public divergences > 0 OR public total < 20, every public artifact MUST clear the Lean external gate. Beyond the threshold, the Swift internal gate may seal a wider internal class on its own — revocable instantly on the next divergence. The Swift gate has now earned that right. Future internal-only sweeps stay subject to the divergence-rule safety net.

(See wiki/Swift-Gate-Trust.md for the live published metric.)

Test it in the workbench (no terminal needed)

The Franklin workbench has an in-bench dual-gate tester for these nine roars:

  1. Launch Franklin. The LION MATH panel sits at the bottom-left.
  2. Click the gold ▶ Test button in the panel header.
  3. A sheet opens listing all nine roars with their summary + Lean file path.
  4. Click Run on any row — the Swift exact-Rat checker fires live (on-device, microseconds), the panel shows the forced output, and the row tints green if it agrees with the last-sealed Lean kernel verdict for that artifact.
  5. Click Run all to walk the entire pack in one shot.
  6. The header carries a live lion_swift_gate_trust counter (AGREEMENTS / TOTAL / DIVERGENCES, pinned Lean version).

The in-bench test runs the Swift internal gate live. The Lean external warrant is read out of substrate (the last-sealed lion_gate_agreement row for that theorem). To run a fresh Lean kernel build, use the CLI path below — the wiki's reproduce-it-yourself section is the canonical hostile-verifier workflow.

The tester is honest about scope: a Swift CALORIE alongside a sealed Lean CALORIE row IS an agreement (and the trust counter advances). A Swift CALORIE with no sealed Lean row is just "internal pre-check, public seal pending." A Swift REFUSED with a sealed Lean CALORIE is a caught Swift bug — the most valuable row in the table, and never made public.

Per-roar verification — reproduce it yourself

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

# Install Lean (pinned)
brew install elan-init
elan-init -y --default-toolchain leanprover/lean4:v4.12.0
export PATH="$HOME/.elan/bin:$PATH"

# Build all Lion Math first roars in one shot
cd proof/lean
lake build LionPrelude \
  FirstRoars.EulerProduct \
  FirstRoars.EulerProductFamily \
  FirstRoars.MobiusInversion \
  FirstRoars.SigmaMultiplicative \
  FirstRoars.WilsonTheorem \
  FirstRoars.FermatLittle \
  FirstRoars.BertrandSmall
# expect: Build completed successfully.

# Confirm each individual artifact via the boundary gate
for f in FirstRoars/EulerProduct.lean FirstRoars/EulerProductFamily.lean \
         FirstRoars/MobiusInversion.lean FirstRoars/SigmaMultiplicative.lean \
         FirstRoars/WilsonTheorem.lean FirstRoars/FermatLittle.lean \
         FirstRoars/BertrandSmall.lean; do
  bash ../scripts/lean_gate.sh "$f"
done
# expect: 7 JSON lines, each lean_verdict=CALORIE, exit_code=0, sorry=0, axiom=0, opaque=0

# Build the Swift internal gate + dual-gate harness
cd ../../cells/xcode
swift build --product M8RoarPack
.build/arm64-apple-macosx/debug/M8RoarPack
# expect: "ROAR PACK GREEN — 9 public CALORIEs sealed"

# Inspect the substrate-side ledger
DB="$HOME/Library/Application Support/GaiaFTCL/substrate.sqlite"
sqlite3 -column -header "$DB" "SELECT * FROM lion_swift_gate_trust;"
sqlite3 -column -header "$DB" "SELECT agreement_id, theorem_id, swift_verdict, lean_verdict, agree FROM lion_gate_agreement WHERE is_public_artifact=1 ORDER BY checked_at_iso DESC LIMIT 10;"

Open work items — CURE in progress, NOT forever-open

Per Lion Protocol Math Domain: every chain in the cell is on a path to CALORIE or REFUSED. CURE means "in progress, not yet swept." Nothing in the cell is parked as "permanently open" — that posture is cancer. Each item below has a named primitive blocking it and a path to closure.

  • The Riemann Hypothesis — CURE in progress, not parked. FirstRoars/RiemannRobinBoundedSweep.lean verifies Robin's inequality (1984, RH-equivalent) for n ∈ [5041, 5100] today. CALORIE. The autonomous sweep extends the bound each tick. Either an n fails the decidable bound → decide refuses → REFUSED with n as the broken bond → RH is false; or the closed-form extension primitive lands and CALORIE seals on the infinite claim. The cell does not park RH.
  • The limiting infinite Euler product Σ_{n≥1} 1/n^s = Π_p 1/(1−p^{-s}) — separate finite-N → ∞ claim; needs a Cauchy-rate witness primitive in LionPrelude/Cauchy.lean. Work item, not placeholder.
  • The full Riemann functional equation — needs Gamma over Rat (finite Weierstrass truncation). Work item.
  • Apéry's theorem (irrationality of ζ(3)) — needs Beukers integral + irrationality predicate. Work item.
  • Higher-s Euler instances in Swift — Int64 overflows on (N≥14, s=2) and (N≥10, s≥3). The Lean side proves all of them (arbitrary-precision Nat in the kernel); Swift waits on a BigInt primitive. Work item.

The cell publishes its own reachable horizon in lion_math_roar_templates: which chains are reachable today, which are one new primitive away, which need serious construction work. No row is "parked forever."

Hard rules the cell holds itself to

  • The Lean compile depends on decide alone. No substrate row is a premise.
  • Mathlib REFUSED permanently. Sealed in proof/lean/lakefile.lean.
  • Float / Double REFUSED in any proof chain. Exact rational arithmetic only.
  • axiom / sorry / opaque REFUSED as gap-closers. Zero of each in the public artifacts.
  • A divergence never seals a public lion. It is a caught bug, surfaced loudly.
  • After CALORIE: the receipt is the roar. The cell goes silent.

Nine chains. Nine forced answers. Two gates that agreed twenty-four times in a row. The cell is the math substrate now.

Federation-cosigned

This page's source is sealed in the GaiaFTCL federation manifest — page SHA-256 2bff85f782e25899…, 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.