renky
renky: system/graph (zero-dependency coordinate systems for rendering), system/algorithms/omniring, and system/algorithms/vlab (228 numbered linear-algebra algorithms over twelve combinable inner-product spaces, 152 self-proving tests). Axiom: a self-contained finite-field skeleton plus eight ring/semiring structures, heat (tropical) degenerations, homology, and a closed computational loop. No third-party dependencies.
#renky
renky/
└─ system/
├─ graph/ ← coordinate systems for a renderer (right-handed, Y-up): see system/graph/README.md
└─ algorithms/
└─ omniring/ ← the axiom book (公理書): sources, tests, proofs, docs
├─ kernel/ select/ A01–A07 proof-enabled (moon prove, Why3 + Z3)
├─ arith/ linalg/ ff/ poly/ A08–A34 finite-field skeleton + linear algebra
├─ ideal/ A35–A43 live ideal state (即時理想狀態)
├─ heat/ tropical/ A44–A51 Maslov dequantization → (min,+) semiring
├─ graded/ semigroup/ A52–A62 graded rings, affine semigroup rings
├─ padic/ smooth/ A63–A71 p-adic integers, ring of smooth germs
├─ homology/ cohom/ A72–A78 homology + cohomology rings
├─ fsplit/ A79–A81 perfect F-split rings
├─ classgroup/ A82–A86 ideal class group correspondence ring
├─ loop/ A87–A89 the closed computational chain (閉環)
├─ cmd/report/ ledger printer (main package)
└─ docs/{AXIOMS,THEOREMS,ALGORITHMS}.mdimport { "ky678/renky/system/algorithms/omniring/loop" }
fn main {
println(@loop.run_all(2).to_string()) // closed = true
}#Verification ledger
| layer | command | result |
|---|---|---|
| machine-checked proofs | moon prove | 2 of 2 packages proved, 9 goals proved |
| executable laws | moon test | 122 passed, 0 failed |
| build | moon check | 0 errors |
| algorithms | docs/ALGORITHMS.md | A01–A89 (89 > 18), no third-party dependencies |
#Reproduce
cd renky
moon check && moon test && moon prove
moon run system/algorithms/omniring/cmd/report#system/graph — coordinate systems for rendering (added in 0.1.2)
moon test -p ky678/renky/system/graphInstall
Download ziprenky: system/graph (zero-dependency coordinate systems for rendering), system/algorithms/omniring, and system/algorithms/vlab (228 numbered linear-algebra algorithms over twelve combinable inner-product spaces, 152 self-proving tests). Axiom: a self-contained finite-field skeleton plus eight ring/semiring structures, heat (tropical) degenerations, homology, and a closed computational loop. No third-party dependencies.
Apache-2.0
Updated 20 days ago
24 downloads