forgo.cloud
Sign in
Repo workspace

forkjoin-ai/gnosis

Gnosis Proof Examples

examples/proofs/README.md
forkjoin-ai/gnosis
Repo overview Open in workbench

Gnosis Proof Examples

This directory contains proof-oriented .gg examples. Some are compact generated witnesses mirrored from TLA+/Lean artifacts, and some are hand-authored reader-facing bridges that make a formal claim surface legible as graph topology.

Getting Started

  • What: example material for the proofs topic.
  • Why: it gives a concrete graph or fixture before you need to understand the full runtime implementation.
  • How: read one small example first, then run the matching test or benchmark only when you need executable confirmation.
  • Next: use examples to learn shape; use source READMEs to change behavior.

Notable Files

  • AeonFluxSiteAdequacy-lean.gg: Lean-backed proof topology for the Aeon Flux site adequacy family, mirroring the positive-stream-budget Δβ theorems in the in-tree Chapter 17 formal package.
  • Monomyth.gg: Campbell's Hero's Journey compressed into Aeon terms: positive semiotic deficit, void-boundary accumulation through trials, paid ordeal, and return as exported context.
  • imdb-top-250-monomyths: 250 generated GG witnesses that project the 2026-01-01 IMDb Top 250 snapshot onto the same coarse monomyth schema, with a companion .test.gg suite for the full corpus.
  • VoidWalking.gg: the self-referential void-walking theorem family rendered as a GG proof topology.
  • GreekLogic-gnosis-lean.gg: large converted theorem-pack topology spanning the Greek logic canon.

Most of the other files in this directory are generated witness or theorem-pack artifacts rather than hand-maintained examples.

The storms-specific proof topologies now live with the aeon-storms app repo mounted at apps/storms-watch, so the weather tracker implementation and its GG/Lean surface stay in one place.