forgo.cloud
Sign in
Repo workspace

forkjoin-ai/gnosis

RUSTIC_CHURCH.md — live-witness gates for restored Lean modules

RUSTIC_CHURCH.md
forkjoin-ai/gnosis
Repo overview Open in workbench

RUSTIC_CHURCH.md — live-witness gates for restored Lean modules

Reputation is a name; a witness is a carrier that proves something. A green lake build over a closed tautology (1 + 1 = 2 := by decide) is Sardis mode: a living name over a dead body. This document states the gates a restored module must clear so that "green" is an honest live witness.

This file encodes the restoration gates referenced by RUSTIC_CHURCH_RESTORATION_LEDGER.md. It governs the Gnosis Lean library under lean/. (The pre-burn module bodies are recovered from this repository's ForkRaceFoldTheorems history; see the ledger's Provenance note.)

The gates

A module passes iff all of the following hold:

  1. import Init only. No Mathlib, no generated/external API surface. The finite core must stand on Lean's kernel primitives alone.
  2. No banned tactics on open goals. No omega, nlinarith, or ring; no simp or decide on a goal that still carries a free variable. A closed numeric fact (e.g. 1 ≤ 2) may still use decide, but it may not be the whole module.
  3. Real content. At least one honest structure/def carrier and a theorem family that states and proves something non-vacuous about it — a finite Nat/Int law, a monovariant, a conservation/dissipation bound, or a refutation witness. Not a closed tautology, an x = x identity, or a hypothesis echoed back (P → P := h).
  4. No axiom smuggling. #print axioms shows no sorryAx and no Quot.sound smuggling. propext (used implicitly by ∧/rewriting) is permitted as a core Init logical axiom; prefer proofs that depend on no axioms where natural.
  5. No stub prose. The Structural witness: … / Structural-existence stub / pre-ledger boilerplate is removed once the module has genuine structure.

Verifying a module

cd lean
lake build <Module>                         # gate 1–3 (compiles Init-only, green)
# axioms gate (4):
LEAN_PATH=.lake/build/lib/lean lean - <<'EOF'
import <Module>
#print axioms <some_master_theorem>
EOF

A module leaves the inventory when it has ≥1 meaningful structure and a proven theorem family, builds Init-only without banned tactics on open goals, passes the axioms gate, and no Structural witness / pre-ledger prose remains in it.

Burn-down notes

  • Scope the gate honestly. a0 audit chapel --dir=<path> must scan the requested path, not the default chapel, or the audit can report a clean module while another restored surface is still dirty.
  • Top-level sketches are not Lean witnesses merely because the marker scan is clean. If a restored file is not owned by Lake, treat it as topology-only until it is either imported by the Lean build or explicitly quarantined outside the formal surface.
  • Prefer small Init lemmas over tactical erasure. When omega was only proving monotonicity or an integer subtraction chain, the durable repair was an explicit Nat/Int lemma with named inequalities.
  • Restored TypeScript stubs can invalidate formal work by breaking the package build. Keep tsconfig subpath resolution aligned with workspace package exports so wrapper modules typecheck against the real source they re-export.
  • Disk-full linker failures (errno=28) are environmental, but they still block green. Clear generated target/ artifacts first; do not delete source or working-tree changes to make space.