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-05-31T14:12:34Z (from substrate lean_proof_state, written by LionMathObserver every 60s).

Current state

Total files	CALORIE	CURE	Total sorrys	Total opaques	Total open gates
72	60	12	21	23	44

Per-file gate state

File	Sorrys	Opaques	Falsifier	Currency	Terminal	Wiki word
FirstRoars/AffectDynamics.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/AmpAmpN4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/AperyZeta3.lean	2	4	✓	✓	CURE	conjecture / formalized skeleton, 6 open gates
FirstRoars/BTCPreimageLarge.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/BTCPreimageN4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/BertrandSmall.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/BosonSampling2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/CTQW2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/CantileverBeam.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/CantileverMixedLoad.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/CantileverOffTipLoad.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/CantileverTwoLoad.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/ChainOfCustodyHash.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/CollapseGate.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/ConstitutionalInvariant.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/CriticalAxisExact.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/DrugEfficacyThreshold.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/ElasticityBar.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/EulerProduct.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/EulerProductFamily.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/FermatLittle.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/FlourishingFloor.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/FourierDFT4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/FuncEqRationalPayloads.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/GTWEDDistance.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/GTWEDTriangleGeneralN.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/GammaHalfInteger.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/GaussianBoson2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/GroverN4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/HHL2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/HamSim2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/HeatEquation1D.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/LaplaceEquation1D.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/LedgerBreaker.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/MLKEMConstraint.lean	0	0	✗	✓	CURE	conjecture / formalized skeleton, 0 open gates
FirstRoars/MaxwellPlaneWave.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/MeaningInUse.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/MeaningInvariant.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/MeaningQuantity.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/MobiusInversion.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/NavierStokesStep.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/PQWalletFinance.lean	6	0	✓	✓	CURE	conjecture / formalized skeleton, 6 open gates
FirstRoars/PharmacokineticOneComp.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/PoissonEquation1D.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/PolyaVinogradov.lean	3	12	✓	✓	CURE	conjecture / formalized skeleton, 15 open gates
FirstRoars/QAOA1.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/QFTN4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/QPCA2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/QPEN4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/QSVT2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/QUBO3.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/RCDischarge.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/RadioactiveTracerDecay.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/RiemannFunctionalEquation.lean	3	7	✓	✓	CURE	conjecture / formalized skeleton, 10 open gates
FirstRoars/RiemannRobinBoundedSweep.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/RungeKutta4.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/SchrodingerStep.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/ShorFactor15.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/ShorFactorLarge.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/ShorWitnessCertifier.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/SigmaMultiplicative.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/SteaneSyndrome.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/StoryInvariant.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/SurfaceCodeD3.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/TellingGate.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/TopologicalFib.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/UILanguageGameDrift.lean	1	0	✓	✓	CURE	conjecture / formalized skeleton, 1 open gates
FirstRoars/VQC2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/VQE2.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/WaveEquation1D.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/WilsonTheorem.lean	0	0	✓	✓	CALORIE	proof
FirstRoars/WitnessTopology.lean	0	0	✓	✓	CALORIE	proof

Live UI surfaces

The Workbench renders the same numbers shown above. Every cell — sorry count, opaque count, falsifier ✓/✗, currency ✓/✗, terminal state, wiki word — is read directly from lean_proof_state every 30 seconds. No value in the UI is asserted in code.

The Lion Math panel — bottom-left of the workbench

The panel mounts as a co-resident overlay (mirror of the Reflective Feedback Board at bottom-right). Always visible while the workbench is open. Click any row to drill into the full Lean source.

Proof drill-in — full Lean source with sorry/opaque/falsifier highlighted

The sheet exposes the un-foolable lines directly:

• SORRY chips (orange) mark every sorry keyword the kernel would refuse on if asked to type-check.
• OPAQUE chips (gold) mark each undischarged opaque definition — the named placeholders for objects the proof has not yet constructed in pure Mathlib vocabulary.
• THEOREM chips (green) mark the stated targets.
• FALSIFIER chips (purple) mark the named counter-example form (Lion Gate G4).
• GATE chips (cyan) mark the -- Gate Gx annotations inside the body explaining what each open gate decomposes to.

Click any line → Copy GitHub link button appears, copying …/EulerProduct.lean#L72 to the clipboard. Reveal in Finder, Open on GitHub, Re-run counter are wired buttons.

Reflective mesh — Lion Math as the sixth observer

The Lion Math observer (gold function icon) runs every 60s alongside Inventory, Attention, Handoff, Atom Steward, and UI Listener. It produces one feedback row per Lean file whose gates moved since the previous tick — a sealed CURE → CALORIE transition is the headline event the operator is waiting for.

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. The workbench UI surface LionMathPanel reads the same table.

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.

---

Federation-cosigned

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