---

title: Lion Math Artifacts — self-verifying math outputs

audience: junior_high_and_up

game: WIKI-LION-MATH-001

contract_version: 1.0.0

authority_kind: normative

generated: 2026-06-05T16:15:53Z

generator: proof/scripts/generate_lion_wiki.sh

---

Lion Math Artifacts

Lion Protocol: the cell does not ship claims. It ships Lean files the kernel accepts. The sorry-count is the un-foolable gate. This page's wiki-word for each target ("proof" or "conjecture") is generated from the count — no one decides it.

*The lion does not argue it is a lion. It produces the receipt.*

Last regenerated: 2026-06-05T16:15:53Z (from substrate lean_proof_state, written by LionMathObserver every 60s).

Current state

Per-file gate state

Live substrate surfaces

This wiki table is regenerated from the same counters the cell stores in lean_proof_state. Every column — sorry count, opaque count, falsifier ✓/✗, currency ✓/✗, terminal state, wiki word — comes from substrate or ./scripts/count_sorrys.sh; nothing is asserted in prose alone.

The LionMathObserver reflective actor refreshes lean_proof_state every 60s when Franklin.app is running. Peer reviewers who do not run the app use this page plus the reproduce command below.

How to verify any row yourself

git clone https://github.com/gaiaftcl-sudo/gaiaFTCL.git
cd gaiaFTCL/proof
./scripts/count_sorrys.sh

That script's output is this page's source of truth. The substrate table lean_proof_state is the cell's record of the same numbers, refreshed every 60s by the LionMathObserver reflective actor when Franklin.app is live.

Hard Lion rules (enforced in code, not in prose)

• No code path writes "proof" to wiki_word unless sorry_count = 0 AND axiom_count = 0 AND opaque_count = 0 AND falsifier_named = 1 AND currency_clean = 1 AND lake_build_exit_code = 0. The Boolean is checked in LionMathObserver.isCalorie().
• The wiki word per row is the substrate column lean_proof_state.wiki_word verbatim. No template renders the word.
• Currency clean = the Lean file contains zero framework vocabulary (M⁸, Klein, S⁴ × C⁴, entropy projection, …) in the theorem statement. The physics is held in proof/latex/ separately.

The kernel rules

Zero sorry + green lake build = proof. Anything else = honest, checkable, self-stating gap list. The cell ships both; the operator never decides which is which.