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 the dual gate (CLI)

Run the Swift internal gate and compare against the sealed Lean warrant:

cd cells/xcode
swift run M8RoarPack

The CLI walks all nine roars: Swift exact-Rat checker vs last-sealed lion_gate_agreement row per theorem. For a fresh Lean kernel build, use the reproduce path below — the wiki's reproduce-it-yourself section is the canonical hostile-verifier workflow.

Scope is honest: a Swift CALORIE alongside a sealed Lean CALORIE row IS an agreement (trust counter advances). A Swift CALORIE with no sealed Lean row is "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 cosignature: pending operator signing host (v26). Witness (sha256 of rendered body): c1164a71c4fc5bd2535f2eff49142232f8ce164fd30212f68e46b99ad9651f62. This page serves with a substrate-honest pending-signature notice until the operator's Franklin signer cosigns it.