Archived
will
d3495476f4
El SDK Release / build-and-release (push) Failing after 13m0s
The generated C, amalgams, vendored runtime pins, and compiled binaries from the Claude Code era are removed from the worktree. The El sources survive; this tree is now source-only for the first-principles rebuild. Per Principal direction 2026-08-19.
53 lines
2.1 KiB
EmacsLisp
53 lines
2.1 KiB
EmacsLisp
// core.el — the math floor, rewritten in El (first principles).
|
|
// The constructor, the state space, ordered roles — the same relatives
|
|
// the substrate was verified with, now expressed in the language itself.
|
|
|
|
// term: a structural value is an atom "0"|"1" or a list ["R", a, b]
|
|
fn atom0() -> [String] { return ["0"] }
|
|
fn atom1() -> [String] { return ["1"] }
|
|
fn is_atom(t: [String]) -> Bool { return str_eq(native_list_get(t, 0), "R") == false }
|
|
fn is_zero(t: [String]) -> Bool { return is_atom(t) && str_eq(native_list_get(t, 0), "0") }
|
|
fn is_unit(t: [String]) -> Bool { return is_atom(t) && str_eq(native_list_get(t, 0), "1") }
|
|
|
|
// constructor — REFUSES impossible terms (distinct operands only)
|
|
fn R(a: [String], b: [String]) -> [String] {
|
|
if str_eq(native_list_get(a, 0), "0") && str_eq(native_list_get(b, 0), "0") { return ["ERROR"] }
|
|
if str_eq(native_list_get(a, 0), "1") && str_eq(native_list_get(b, 0), "1") { return ["ERROR"] }
|
|
let t: [String] = native_list_empty()
|
|
let t = native_list_append(t, "R")
|
|
let t = native_list_append(t, native_list_get(a, 0))
|
|
let t = native_list_append(t, native_list_get(b, 0))
|
|
return t
|
|
}
|
|
|
|
// term equality by serialization (canonical string of the structure)
|
|
fn term_str(t: [String]) -> String {
|
|
let n: Int = native_list_len(t)
|
|
if n == 1 { return native_list_get(t, 0) }
|
|
let out: String = "R("
|
|
let out = str_concat(out, str_concat(native_list_get(t, 1), ","))
|
|
let out = str_concat(out, str_concat(native_list_get(t, 2), ")"))
|
|
return out
|
|
}
|
|
fn term_eq(a: [String], b: [String]) -> Bool { return str_eq(term_str(a), term_str(b)) }
|
|
|
|
// ordered-role recovery (P-012): defined only on Im(R)
|
|
fn L(t: [String]) -> [String] {
|
|
if is_atom(t) { return ["ERROR"] }
|
|
return [native_list_get(t, 1)]
|
|
}
|
|
fn RR(t: [String]) -> [String] {
|
|
if is_atom(t) { return ["ERROR"] }
|
|
return [native_list_get(t, 2)]
|
|
}
|
|
|
|
fn main() -> Void {
|
|
let z: [String] = atom0()
|
|
let u: [String] = atom1()
|
|
let r1: [String] = R(z, u)
|
|
println(term_str(r1))
|
|
println(term_str(L(r1)))
|
|
println(term_str(RR(r1)))
|
|
println(term_eq(L(r1), z))
|
|
}
|