Build

Coq

cd coq
coqc MinimalSIGDemo.v

Lean4

cd lean
# WIP: add Lakefile / dependencies
lake build

Status: Work in Progress (WIP)

This repository is an evolving minimal demo in Coq and Lean4. Goal: formalize a Collatz-style iterator, gate reachability, and uniqueness of the first hitting time (“gate index”). Expect refactors and file moves.

MinimalSIGDemo

Contains a small Collatz-style iterator T,gate reachability, and uniqueness of the first hitting time (“gate index”). The same core definitions are implemented in both assistants to compare proof styles and automation.

Roadmap

• unify naming between Coq and Lean versions
• add lemma: gate_index decreases along orbit (no nontrivial cycles under global reachability)
• add CI for both toolchains

Layout

• coq/ — Coq development
• lean/ — Lean4 development