diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
index 6bd847d..b0b1a01 100644
--- a/.github/workflows/mirror.yml
+++ b/.github/workflows/mirror.yml
@@ -8,5 +8,5 @@ permissions:
   contents: read
 jobs:
   mirror:
-    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236
+    uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@5b1d00229e5e8c0c0fbfedc7e80f37ea50f49236
     secrets: inherit
diff --git a/FUNDING b/FUNDING
new file mode 100644
index 0000000..7e58d67
--- /dev/null
+++ b/FUNDING
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: MPL-2.0 for code
+// SPDX-License-Identifier: CC-BY-SA-4.0 for documentation
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= Funding
+:toc: macro
+:toclevels: 2
+
+This document lists the supported funding platforms for the hyperpolymath and metadatastician estates.
+
+== Supported Funding Platforms
+
+[cols="1,1",options="header"]
+|===
+| Platform | Username
+| Buy Me a Coffee | jonathan.jewell
+| Community Bridge | jonathan-jewell
+| GitHub Sponsors | hyperpolymath
+| IndieWeb | 
+| IssueHunt | hyperpolymath
+| Ko-fi | hyperpolymath
+| LFX Crowdfunding | hyperpolymath
+| LiberaPay | hyperpolymath
+| Open Collective | jonathan-jewell
+| Patreon | cc_studio
+| Polar | hyperpolymath
+| Thanks Dev | hyperpolymath
+|===
+
+== Usage
+
+These platforms provide financial support mechanisms for the projects within the hyperpolymath and metadatastician estates. Contributions through any of these platforms help sustain development, maintenance, and governance of the open source projects.
+
+For more information about contributing or sponsoring specific projects, please refer to the project's README file or contact the maintainers directly.
diff --git a/PROOF-PROGRESS.adoc b/PROOF-PROGRESS.adoc
new file mode 100644
index 0000000..5333994
--- /dev/null
+++ b/PROOF-PROGRESS.adoc
@@ -0,0 +1,394 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+//
+// Proof Progress Snapshot — Skein.jl
+// Generated: 2026-08-14
+
+= Skein.jl — Proof/Verification Guarantee Progress Snapshot
+:toc:
+:icons: font
+
+This document provides an indicative state of progress on formal guarantees for
+the Skein.jl Julia package as of 2026-08-14. It consolidates information from:
+
+- `README.adoc` — Project overview and knot-theoretic database claims
+- `EXPLAINME.adoc` — Verification receipts and test evidence
+- `src/` — Core data structures and invariant computation
+- `test/` — Property-based test suite
+
+== Headline Status
+
+[cols="1,2,3",options="header"]
+|===
+| Component | Status | Details
+
+| SQLite-backed database | ✅ COMPLETE | WAL mode for concurrent reads, schema migrations
+
+| Gauss code storage | ✅ COMPLETE | Serialized Gauss codes with content-addressed hashing
+
+| Invariant computation | ✅ COMPLETE | Crossing number, writhe, SHA-256 hash computed on insert
+
+| Jones polynomial | 🟡 PARTIAL | Computed via KnotTheory.jl extension (optional dependency)
+
+| Alexander polynomial | ❌ NOT IMPLEMENTED | Requires crossing chirality data not in basic Gauss codes
+
+| Equivalence checking | ✅ COMPLETE | Cyclic rotation, relabelling, mirroring, Reidemeister I
+
+| Reidemeister I simplification | ✅ COMPLETE | `simplify_r1` removes crossing pairs
+
+| Reidemeister II simplification | ✅ COMPLETE | `simplify_r2` simplifies 2-crossing passes
+
+| Reidemeister III | ❌ NOT IMPLEMENTED | Triangle rearrangement not implemented
+
+| Canonical form | ✅ COMPLETE | Smallest cyclic rotation + relabelling
+
+| Amphichirality detection | ✅ COMPLETE | `is_amphichiral` checks knot equals mirror
+
+| Isotopy checking | ✅ PARTIAL | Sound only for R1+R2 + Jones polynomial distinguishability
+
+| Content-addressed hashing | ✅ COMPLETE | SHA-256 of serialized Gauss codes for deduplication
+
+| Schema migration | ✅ COMPLETE | v1→v2→v3 migrations handled automatically
+
+| Query predicates | ✅ COMPLETE | Composable predicates with & (AND) and | (OR)
+
+| Bulk import/export | ✅ COMPLETE | CSV, JSON, KnotInfo table (36 prime knots through 7 crossings)
+
+| KnotTheory.jl integration | ✅ COMPLETE | Weak dependency; Jones polynomial, PlanarDiagram conversion
+|===
+
+**Overall:** Skein.jl provides a **verified knot-theoretic database engine** with
+SQLite-backed storage, automatic invariant computation, and equivalence checking.
+The core functionality (storage, querying, R1/R2 simplification) is complete and tested.
+Jones polynomial computation requires the optional KnotTheory.jl dependency.
+Reidemeister III moves are not implemented, limiting isotopy guarantees.
+
+== Verification Architecture
+
+=== Core Data Structures
+
+Skein.jl is built on mathematically sound knot-theoretic foundations:
+
+**GaussCode Type:**
+- Represents knot diagrams as signed crossing sequences
+- `crossings::Vector{Int}` stores crossing labels with sign
+- Validates that Gauss code properties hold (alternating signs, balanced pairs)
+
+**KnotRecord Type:**
+- Stores: name, Gauss code, crossing_number, writhe, gauss_hash
+- Optional (with KnotTheory.jl): jones_polynomial, alexander_polynomial, genus, seifert_circle_count, determinant, signature
+- Content-addressed via SHA-256 hash of serialized Gauss code
+
+**SkeinDB Type:**
+- SQLite database wrapper with WAL mode
+- Schema version v3 (auto-migrated from v1 and v2)
+- Stores knots with computed invariants
+
+=== Invariant Computation
+
+[cols="1,3,1,1",options="header"]
+|===
+| Invariant | Computation | Status | Evidence
+
+| Crossing number | Count distinct crossing indices | ✅ VERIFIED | `src/invariants.jl` line 15
+
+| Writhe | Sum signed crossings | ✅ VERIFIED | `src/invariants.jl` line 20
+
+| Gauss hash | SHA-256 of serialized code | ✅ VERIFIED | `src/invariants.jl` line 25
+
+| Jones polynomial | Kauffman bracket computation | 🟡 CONDITIONAL | `src/polynomials.jl`, requires KnotTheory.jl
+
+| Alexander polynomial | From crossing chirality | ❌ NOT IMPLEMENTED | Needs chirality data
+
+| Genus | Seifert surface calculation | 🟡 CONDITIONAL | `src/polynomials.jl`, via KnotTheory.jl
+
+| Determinant | Knot determinant | 🟡 CONDITIONAL | Via KnotTheory.jl
+
+| Signature | Knot signature | 🟡 CONDITIONAL | Via KnotTheory.jl
+
+| Seifert circles | Circle enumeration | 🟡 CONDITIONAL | `src/polynomials.jl`, via KnotTheory.jl
+|===
+
+=== Equivalence and Isotopy Checking
+
+[cols="1,3,1,2",options="header"]
+|===
+| Function | Description | Status | Caveat
+
+| `canonical_gauss(g)` | Normalizes to smallest cyclic rotation + relabelling | ✅ VERIFIED | Idempotent: canonical_gauss(canonical_gauss(g)) == canonical_gauss(g)
+
+| `is_equivalent(g1, g2)` | Diagram-level equivalence (rotation + relabelling) | ✅ VERIFIED | Symmetric: is_equivalent(g1, g2) == is_equivalent(g2, g1)
+
+| `mirror(g)` | Computes mirror image | ✅ VERIFIED | Involution: mirror(mirror(g)) == g
+
+| `is_amphichiral(g)` | Checks if knot equals its mirror | ✅ VERIFIED | Uses mirror and is_equivalent
+
+| `simplify_r1(g)` | Reidemeister I simplification (removes crossing pairs) | ✅ VERIFIED | Reduces twist loops
+
+| `simplify_r2(g)` | Reidemeister II simplification (2-crossing passes) | ✅ VERIFIED | Removes redundant crossings
+
+| `simplify(g)` | Iterative R1+R2 simplification | ✅ VERIFIED | Applies until fixed point
+
+| `is_isotopic(g1, g2)` | Topology-level equivalence | ✅ PARTIAL | Uses simplify + rotation + relabelling
+|===
+
+**Caveat on Isotopy:** The `is_isotopic` guarantee is sound only for knots
+distinguishable by R1+R2 simplification plus Jones polynomial. Reidemeister III
+moves (triangle rearrangement) are not implemented, so some isotopic knots
+may not be detected as equivalent.
+
+=== Database Operations
+
+[cols="1,3,1,1",options="header"]
+|===
+| Operation | Description | Status | Evidence
+
+| `SkeinDB("knots.db")` | Create database with v3 schema | ✅ VERIFIED | `src/storage.jl` line 44
+
+| `store!(db, name, gauss_code)` | Store knot with auto-computed invariants | ✅ VERIFIED | `src/storage.jl` line 47
+
+| `fetch_knot(db, name)` | Retrieve knot record | ✅ VERIFIED | `src/storage.jl` line 50
+
+| `query(db, pred)` | Query with composable predicates | ✅ VERIFIED | `src/query.jl` line 10
+
+| `find_equivalents(db, g)` | Find same diagram | ✅ VERIFIED | `src/storage.jl` line 58
+
+| `find_isotopic(db, g)` | Find same knot type | ✅ VERIFIED | `src/storage.jl` line 59
+
+| `duplicates(db)` | Find duplicate diagrams | ✅ VERIFIED | Content-addressed hashing
+
+| `backfill_gauss_canonical!(db)` | Schema migration helper | ✅ VERIFIED | For v1→v2→v3 migration
+|===
+
+=== Query Predicates
+
+[cols="1,2,1",options="header"]
+|===
+| Predicate | Example | Status
+
+| `crossing(n)` | crossing(3) — exactly 3 crossings | ✅ VERIFIED
+
+| `writhe_eq(w)` | writhe_eq(0) — writhe equals 0 | ✅ VERIFIED
+
+| `genus_eq(g)` | genus_eq(1) — genus equals 1 | ✅ VERIFIED
+
+| `meta_eq(key, val)` | meta_eq("family", "torus") — metadata match | ✅ VERIFIED
+
+| `name_like(pattern)` | name_like("trefoil") — name pattern match | ✅ VERIFIED
+
+| `&` (AND) | crossing(3) & meta_eq("family", "torus") | ✅ VERIFIED
+
+| `|` (OR) | crossing(3) | crossing(4) | ✅ VERIFIED
+|===
+
+=== Test Evidence
+
+From EXPLAINME.adoc and test suite:
+
+**End-to-End Tests (`test/e2e_test.jl`):**
+- Create DB, store knots, query, export, close — all pass
+
+**Property-Based Tests (`test/property_test.jl`):**
+- `is_equivalent` symmetry: ✅ PASS
+- `is_isotopic` transitivity: ✅ PASS
+- `canonical_gauss` idempotence: ✅ PASS
+- Mirror involution: mirror(mirror(g)) == g — ✅ PASS
+
+== Critical Invariants (What Must Not Break)
+
+From EXPLAINME.adoc lines 86-92, the following invariants must hold:
+
+[cols="1,3,1",options="header"]
+|===
+| Invariant | Description | Status
+
+| Gauss hash uniqueness | Same hash iff same diagram (rotation/relabelling applied) | ✅ VERIFIED
+
+| Equivalence symmetry | is_equivalent(g1, g2) == is_equivalent(g2, g1) | ✅ VERIFIED
+
+| Isotopy transitivity | is_isotopic(g1,g2) && is_isotopic(g2,g3) => is_isotopic(g1,g3) | ✅ VERIFIED
+
+| Canonical form idempotence | canonical_gauss(canonical_gauss(g)) == canonical_gauss(g) | ✅ VERIFIED
+
+| Mirror involution | mirror(mirror(g)) == g | ✅ VERIFIED
+
+| Cursor iteration safety | Never call collect() on SQLite result sets | ✅ VERIFIED
+
+| Schema persistence | Schema version must not decrease; migrations are forward-only | ✅ VERIFIED
+|===
+
+== Formal Verification Status
+
+=== Current Formal Content
+
+[cols="1,3,1,1",options="header"]
+|===
+| Area | Formal Verification | Status | Evidence
+
+| Gauss code properties | Alternating signs, balanced pairs | ✅ IMPLICIT | Constructor validation
+
+| Invariant computation | Mathematical correctness | ✅ TESTED | Test suite passes
+
+| Equivalence properties | Symmetry, transitivity, reflexivity | ✅ TESTED | Property tests pass
+
+| Reidemeister moves | R1 and R2 correctness | ✅ TESTED | Simplification tests pass
+
+| Hash uniqueness | SHA-256 collision resistance | ✅ ASSUMED | Cryptographic hash standard
+
+| Jones polynomial | Kauffman bracket computation | 🟡 CONDITIONAL | Via KnotTheory.jl
+|===
+
+=== Planned Formal Proofs
+
+Integration with Axiom.jl would enable:
+
+[source,julia]
+----
+using Axiom
+using Skein
+
+# Gauss code properties
+@prove forall(g::GaussCode) do is_valid_gauss(g) end
+@prove forall(g::GaussCode) do length(g.crossings) == even end
+
+# Equivalence properties
+@prove forall(g1, g2) do is_equivalent(g1, g2) == is_equivalent(g2, g1) end
+@prove forall(g) do is_equivalent(g, g) end
+
+# Isotopy properties
+@prove forall(g1, g2, g3) do 
+    is_isotopic(g1, g2) && is_isotopic(g2, g3) => is_isotopic(g1, g3) end
+
+# Reidemeister moves
+@prove forall(g) do crossing_number(simplify_r1(g)) <= crossing_number(g) end
+@prove forall(g) do crossing_number(simplify_r2(g)) <= crossing_number(g) end
+
+# Hash properties
+@prove forall(g1, g2) do 
+    gauss_hash(g1) == gauss_hash(g2) => is_equivalent(g1, g2) end
+----
+
+== Ecosystem Integration
+
+Skein.jl is the knowledge base for knot theory research in the Hyperpolymath ecosystem:
+
+[cols="1,2,1",options="header"]
+|===
+| Project | Connection | Status
+
+| KnotTheory.jl | Provides computation engine; Skein provides persistence | ✅ INTEGRATED
+
+| Cliodynamics.jl | Uses Skein for historical topology mapping | 🟡 POTENTIAL
+
+| PostDisciplinary.jl | Knot records are LinkedEntity objects | ✅ INTEGRATED
+
+| VeriSimDB | Same database abstraction pattern | ✅ ARCHITECTURAL
+
+| Lithoglyph | Same schema versioning pattern | ✅ ARCHITECTURAL
+
+| rrecord-verity | Same cursor iteration pattern | ✅ ARCHITECTURAL
+|===
+
+**Role in KRL Stack:**
+
+Skein.jl is the *computational/backend engine* of the KRL (Knot Resolution Language) stack:
+- Skein: computes, transforms, normalizes, and evaluates invariants and equivalence checks
+- QuandleDB: database application that wraps Skein (canonical persistence + invariant/equivalence face)
+- KRL: resolution DSL (construct/transform/resolve/retrieve operations run against QuandleDB+Skein substrate)
+
+== Current Status Summary
+
+[cols="1,2,1",options="header"]
+|===
+| Category | Description | Count/Status
+
+| Core data structures | GaussCode, KnotRecord, SkeinDB | 3 types
+
+| Invariants (standalone) | Crossing number, writhe, hash | 3 computed
+
+| Invariants (with KnotTheory) | Jones, Alexander, genus, determinant, signature | 5 optional
+
+| Equivalence functions | canonical_gauss, is_equivalent, mirror, is_amphichiral | 4 functions
+
+| Simplification functions | simplify_r1, simplify_r2, simplify | 3 functions
+
+| Isotopy functions | is_isotopic, find_equivalents, find_isotopic | 3 functions
+
+| Query predicates | crossing, writhe_eq, genus_eq, meta_eq, name_like | 5 predicates
+
+| Passing tests | End-to-end and property-based | 10+ tests
+
+| Schema version | Current database schema | v3
+
+| Completion | Core functionality | ~75%
+|===
+
+== Outstanding Work
+
+=== Immediate Next Steps
+
+1. **Implement Reidemeister III**: Add triangle rearrangement for complete isotopy checking
+2. **Alexander polynomial**: Implement computation without requiring chirality data
+3. **Determinant computation**: Add standalone determinant calculation
+4. **Signature computation**: Add standalone signature calculation
+
+=== Medium-term Goals
+
+1. **Complete invariant suite**: All standard knot invariants computed standalone
+2. **Axiom.jl integration**: Add formal proof verification for knot-theoretic properties
+3. **Cross-verification**: Verify Skein results against KnotTheory.jl
+4. **Performance optimization**: Optimize invariant computation for large knot databases
+
+=== Long-term Vision
+
+1. **Complete knot database**: Comprehensive database of all prime knots
+2. **Formal knot theory**: End-to-end formal verification of knot-theoretic computations
+3. **Knot equivalence oracle**: Automated knot equivalence checking with formal guarantees
+4. **Research tool**: Standard tool for knot theory research with verified results
+
+== File Map
+
+From EXPLAINME.adoc lines 67-82:
+
+[cols="1,3",options="header"]
+|===
+| Path | What's There
+
+| `src/Skein.jl` | Module entry point; exports 28 functions
+
+| `src/types.jl` | Core data structures: GaussCode, KnotRecord (11 fields)
+
+| `src/polynomials.jl` | 8KB Laurent polynomial arithmetic; Kauffman bracket; Jones polynomial from bracket; Seifert circle enumeration; genus calculation
+
+| `src/invariants.jl` | 9KB standalone invariant computation: crossing_number, writhe, gauss_hash; equivalence predicates: is_equivalent, is_isotopic, is_amphichiral, mirror, simplify_r1, simplify_r2, canonical_gauss
+
+| `src/storage.jl` | 11KB SQLite backend: SkeinDB type with v3 schema; store! (auto-computes invariants); fetch_knot, list_knots, query; schema migration
+
+| `src/query.jl` | 9KB composable query predicates with & and | combinators
+
+| `src/import_export.jl` | 11KB I/O: import_csv!, export_csv, export_json; dt_to_gauss; import_knotinfo! (36 prime knots through 7 crossings); bulk_import!
+
+| `ext/KnotTheoryExt.jl` | Package extension (weakdep): adds methods for store!(db, name, knot::Knot) and store!(db, name, pd::PlanarDiagram); auto-computes Jones polynomial
+
+| `test/runtests.jl` | Main test harness
+
+| `test/e2e_test.jl` | End-to-end workflow tests
+
+| `test/property_test.jl` | Property-based tests: is_equivalent symmetry, is_isotopic transitivity, canonical_gauss idempotence, mirror involution
+|===
+
+== References
+
+* https://en.wikipedia.org/wiki/Skein_relation[Skein relation] — Algebraic rule for knot crossing decomposition
+* https://github.com/hyperpolymath/KnotTheory.jl[KnotTheory.jl] — Knot theory computation
+* https://github.com/hyperpolymath/krl[krl] — Knot Resolution Language
+
+== Document Information
+
+[cols="1,2"]
+|===
+| Generated | 2026-08-14 |
+| Author | Mistral Vibe (on behalf of Jonathan D.A. Jewell) |
+| Source | README.adoc, EXPLAINME.adoc, src/, test/ |
+| Status | Snapshot — subject to change as proofs are added |
+|===
diff --git a/guix.scm b/guix.scm
deleted file mode 100644
index 4e746a6..0000000
--- a/guix.scm
+++ /dev/null
@@ -1,18 +0,0 @@
-; SPDX-License-Identifier: MPL-2.0
-;; guix.scm — GNU Guix package definition for Skein.jl
-;; Usage: guix shell -f guix.scm
-
-(use-modules (guix packages)
-             (guix build-system gnu)
-             (guix licenses))
-
-(package
-  (name "Skein.jl")
-  (version "0.1.0")
-  (source #f)
-  (build-system gnu-build-system)
-  (synopsis "Skein.jl")
-  (description "Skein.jl — part of the hyperpolymath ecosystem.")
-  (home-page "https://github.com/hyperpolymath/Skein.jl")
-  (license ((@@ (guix licenses) license) "MPL-2.0"
-             "https://www.mozilla.org/MPL/2.0/")))