Antihydra

antihydra is the planned ontology, toolkit, and search engine for Lafont interaction-combinator nets.

The current state is:

• project scaffold created
• source shelf downloaded locally
• first-pass phasing plan written down
• verified Lafont kernel implemented
• exact tiny canonicalization oracle implemented
• vendored Traces-backed canonical graph backend integrated
• exact tiny connected-shell generator implemented
• first connected-shell classifier implemented
• first connected-shell artifact/report writer implemented
• SQLite-backed release pipeline scaffolded
• exact holdout explorer implemented
• disconnected n = 4 composition implemented
• monotone-ray atlas lane implemented
• ridge-map analysis lane for n = 2 and n = 4 implemented
• exact-only n = 4 ownership lane implemented
• exact ordered-aux Burnside total counts implemented

This is intentionally a buildable research project, not just a note dump.

Current Goal

Build an exact core plus a frontier toolkit for:

• isomorph-free connected-net generation
• packed deterministic reduction
• exact classification and holdout exploration
• BBchallenge-style certificate plugins for hard non-normalizers
• symmetry discovery and quotienting where it is exact
• sound bounding and abstraction where exact closure becomes too expensive
• progressively coarser but still useful representations above the exact core

There is now also one explicit priority side channel:

• enumerate the monotone rays d = 0 and c = 0 as far as possible
• use those rays as the first exact large-scale counting regime
• treat them as the cleanest bridge between IC enumeration and Ramanujan-adjacent sequence analysis

The project is not limited to "very small ICs."

There is now a clean split between:

• the light
  • exact total counts T(c,d,e)
  • pure combinatorics / Burnside counting
• the shadow
  • the split into normalizing vs non-normalizing nets
  • actual reduction dynamics

Read light.md for the exact convention and formula that match the repo’s atlas data. Read real_map.md for the current skeleton / reaction / routing hierarchy that replaces the old composition-only picture.

The exact core is the anchor. Above that core, we still want useful structure:

• exact canonical objects
• exact derived invariants and decompositions
• sound abstractions and bounds
• explicit heuristic summaries when needed

The point is to push outward as far as possible without lying about what level of certainty we have.

What Exists Today

The project now has a first verified Lafont kernel in Rust.

That kernel is not the atlas yet. It is the trusted semantic base the atlas will sit on.

Current verified pieces:

• ontology types for combinator kinds, slots, and active pairs
• a correctness-first reference reducer
• a packed mutable reducer
• shared rewrite-composition logic used by both reducers
• a small verification-oriented shape snapshot representation
• a green test suite for the six rules and core semantic regressions
• a tiny exact canonicalization oracle over colored incidence graphs
• a tiny exact connected-shell generator using canonical partial-state search
• a deterministic packed classifier for connected canonical nets
• a shell driver that writes one JSON artifact and one markdown report per shell

Local Layout

• docs/sources/
  • downloaded papers, pages, and code references for future sessions
• docs/mission.md
  • first-principles statement of what the project is trying to become
• docs/kernel.md
  • current verified Lafont-kernel scope
• docs/architecture.md
  • how the current crate is organized and why the representations are split
• docs/testing.md
  • what is currently verified and how to run or extend the checks
• docs/canonicalization.md
  • the current exact small-net canonicalization oracle
• docs/release.md
  • authoritative release command, SQLite ground truth, and holdout explorer
• docs/frontiers.md
  • the clean split between the structural atlas frontier and the exact behavioral closure frontier
• docs/monotone_rays.md
  • why the d = 0 and c = 0 rays are a priority exact counting channel
  • the current monotone atlas lane and its verification/analysis contract
• docs/mining.md
  • symmetry and quotient mining over the structural atlas corpus
• docs/growth.md
  • first certificate-style growth decider for active-growing holdouts
• docs/ridge.md
  • exact-only ridge-map pass over the existing atlas DB
  • composition table, holdout inventory, and simplex heatmap contract
• docs/n4_ownership.md
  • proof-grade shell-ownership lane
  • exact connected-first closure and exact disconnected derivation
• docs/rust_before_lean.md
  • what belongs in Rust
  • what gets verified before formalization
  • when Lean should enter the loop
• docs/kind_formalization.md
  • what local Kind actually supports
  • how to run the local Kind workflow on this machine
  • what should and should not be formalized in Kind first
• docs/real_map.md
  • the current “real map” hierarchy: composition -> reaction counts -> reaction+routing -> full wiring
  • current shell-2 / shell-4 / (3,3,0) prep results
• docs/rust_timeline.md
  • stable Rust-phase numbering for this project
  • what is done now and what comes next
  • definition of done for each Rust phase
• docs/wiki/
  • theorem and conjecture knowledge base
  • stable ids, proof status, dependencies, and arsenal use
• docs/atlas.md
  • lower-order atlas contract: horizon, enumeration policy, classification policy, and documentation rules
• docs/shell_review_n2_n4.md
  • reviewed shell decisions for n = 2 and n = 4, including the current n = 6 gate
• docs/phasing.md
  • suggested implementation order and milestones
• src/
  • Rust kernel implementation
• tests/
  • Rust integration tests for the current semantic kernel

Start Here

1. read docs/sources/README.md
2. read docs/mission.md
3. read docs/kernel.md
4. read docs/architecture.md
5. read docs/testing.md
6. read docs/canonicalization.md
7. read docs/atlas.md
8. read docs/release.md
9. read docs/frontiers.md
10. read docs/monotone_rays.md
11. read docs/mining.md
12. read docs/growth.md
13. read docs/ridge.md
14. read docs/shell_review_n2_n4.md
15. read docs/n4_ownership.md
16. read docs/rust_before_lean.md
17. read docs/kind_formalization.md
18. read docs/rust_timeline.md
19. read docs/real_map.md
20. read docs/wiki/README.md
21. read docs/phasing.md
22. treat the downloaded files under docs/sources/raw/ as the local baseline

Quickstart

Run the current verification suite:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo test

Format the crate:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo fmt

Run the canonicalization demo:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin canonicalize -- lafont-quine-seed

Run the authoritative release command:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_release -- --db artifacts/low_atlas.sqlite --out-dir artifacts/low_atlas_release

Run the structural-first atlas release:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_structural -- --db artifacts/structural_atlas.sqlite --out-dir artifacts/structural_atlas_release --max-n 4

Run the first mining pass over that structural corpus:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_mine -- --db artifacts/structural_atlas.sqlite --out-dir artifacts/atlas_mining_n4 --max-n 4

Run the monotone-ray release bundle:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_monotone -- --db artifacts/monotone_atlas.sqlite --out-dir artifacts/monotone_atlas_release --max-n 10 --verify-max-n 6

Rebuild the monotone analyses from SQLite:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_monotone_analyze -- --db artifacts/monotone_atlas.sqlite --out-dir artifacts/monotone_atlas_analysis --max-n 10

Verify that monotone ray equality is literal γ <-> δ relabeling:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin verify_monotone_duality -- --db artifacts/monotone_atlas.sqlite --max-n 8

Compute the pure-ternary closed sequence directly by Burnside:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin pure_ternary_burnside -- --max-n 12

Compute the exact ordered-aux total count at one composition:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --release --bin composition_burnside -- --g 3 --d 3 --e 0

Run the first growth-family non-normalization decider:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin growth_decider -- --db artifacts/structural_atlas.sqlite --shell 2 --g 1 --d 1 --e 0 --ordinal 7

Run the exact-only ridge-map pass over the existing structural atlas DB:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --release --bin atlas_ridge -- --db artifacts/structural_atlas.sqlite --out-dir artifacts/undecidability_ridge

Run the exact-only shell-ownership lane:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --release --bin n4_ownership -- --db artifacts/structural_atlas.sqlite --out-dir artifacts/n4_ownership

Run the proof-net recognizer benchmark against a shell decision log:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --release --bin proof_net_scan -- --db artifacts/structural_atlas.sqlite --decision-log artifacts/cryptid_hunt/cryptid_decision_log.csv --shell 2 --out-dir artifacts/proof_net_scan_shell2

Build and verify the shell-2 certificate bundle:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --release --bin shell2_certificates -- --db artifacts/structural_atlas.sqlite --out-dir artifacts/shell2_certificates

Inspect the finished conservative ridge bundle currently checked into artifacts/:

artifacts/undecidability_ridge_conservative.sqlite
artifacts/undecidability_ridge_conservative/undecidability_ridge_compositions.csv
artifacts/undecidability_ridge_conservative/undecidability_ridge_holdouts.csv
artifacts/undecidability_ridge_conservative/undecidability_ridge_summary.md
artifacts/undecidability_ridge_conservative/undecidability_ridge_simplex.svg

Run a bounded smoke release while the exact frontier is still open:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_release -- --db artifacts/low_atlas_smoke.sqlite --out-dir artifacts/low_atlas_smoke --explorer-state-cap 64

Run the exact holdout explorer on one stored connected net:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin holdout_explorer -- --db artifacts/low_atlas_smoke.sqlite --canonical-id <HEX>

Probe one stored connected net under a custom deterministic step budget:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin probe_connected -- --db artifacts/structural_atlas.sqlite --shell 2 --g 1 --d 1 --e 0 --ordinal 7 --max-steps 1024

Run only the canonicalization tests:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo test canonicalization

Run the exact connected-shell census:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin census -- --g 2 --d 0 --e 0

Cross-check the isomorph-free census against the labeled baseline:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin census -- --g 2 --d 0 --e 0 --compare-baseline

Classify one composition:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin classify -- --g 0 --d 0 --e 2 --compare-baseline --cross-check-ref

Write the first connected-shell atlas artifact and report:

cd /Users/fresh/Documents/bend-experiments/antihydra
cargo run --bin atlas_shell -- --n 2 --compare-baseline --max-steps 64 --out-dir artifacts/connected_shell_n2

Current Code Map

• src/ontology.rs Shared semantic vocabulary: kinds, slots, active pairs, packed port refs.
• src/reference.rs Correctness-first reducer with straightforward node/port state.
• src/packed.rs Packed mutable reducer intended to become the execution fast path.
• src/compose.rs Shared boundary-composition logic for local rewrites.
• src/shape.rs Snapshot representation for exact small-world verification and future canonicalization work.
• src/incidence.rs Colored incidence graph and exact byte serialization for the tiny-net oracle.
• src/canonical.rs Production canonicalization layer, with vendored Traces underneath and the tiny oracle kept as a verification-compatible shape path for the current n <= 4 release regime.
• src/enumerate.rs Exact connected-shell enumeration, including the new canonical partial-state generator and the old labeled baseline oracle.
• src/classify.rs Deterministic connected-net classifier using the packed kernel plus optional reference cross-checks.
• src/atlas.rs Shell artifact schema, shell driver, and markdown report generation.
• src/explorer.rs Exact reachable-state explorer for connected holdouts.
• src/disconnected.rs Exact disconnected-shell composition for the n <= 4 release.
• src/db.rs SQLite schema and persistence helpers for the low-order atlas.
• src/release.rs Authoritative release orchestration and export generation.
• src/structural.rs Structural-first atlas release path: exact objects, deterministic frontier behavior, and shell exports that can move ahead of exact closure.
• src/mining.rs Symmetry and quotient mining over the structural atlas corpus.
• src/growth.rs First certificate-style growth-family decider for active-growing holdouts.
• src/render.rs Small shared formatting helpers for ids, words, and hashes.
• src/fixtures.rs Small named nets shared by tests and the CLI.
• src/bin/canonicalize.rs Terminal entrypoint for the current canonicalization oracle.
• src/bin/census.rs Terminal entrypoint for exact connected-shell census runs and baseline cross-checks.
• src/bin/classify.rs Terminal entrypoint for per-composition connected-net classification.
• src/bin/atlas_shell.rs Terminal entrypoint for full connected-shell atlas runs.
• src/bin/holdout_explorer.rs Terminal entrypoint for exact holdout exploration backed by SQLite.
• src/bin/atlas_release.rs Terminal entrypoint for the authoritative low-order release pipeline.
• src/bin/atlas_structural.rs Terminal entrypoint for the structural atlas frontier release.
• src/bin/atlas_mine.rs Terminal entrypoint for symmetry and quotient mining over the structural DB.
• src/bin/growth_decider.rs Terminal entrypoint for the first growth-family non-normalization decider.
• src/bin/probe_connected.rs Terminal entrypoint for single-net deterministic probing from a stored atlas DB.
• tests/kernel.rs Rule tests and semantic regressions for the current kernel.
• tests/canonicalization.rs Canonicalization oracle cross-checks and relabeling-invariance tests.
• tests/census.rs Lower-order census regressions and isofree-vs-baseline agreement tests.
• tests/atlas.rs Classifier regressions plus artifact/report writer checks.
• tests/release.rs Explorer and disconnected-composition smoke tests for the release path.

Design Constraints

• exact only
• no sampling in the exact core
• no top-level labeled perfect-matching enumeration plus post-hoc dedup
• connected closed nets first, disconnected nets as multisets of connected components
• partial states may be deduplicated canonically during search; that is the intended path, not a compromise
• canonical forms for identity, not pairwise isomorphism checks in the hot path
• packed mutable runtime for reduction, separate from canonical shape storage
• never blur exact facts, sound bounds, and heuristic structure into one status