use neberu::encoding::{certificate_bytes, compute_q2, fmt_hex, pack_word, trit_word_display};
use neberu::expr::Expr;
use neberu::gen::Gen;
use neberu::governance::Governance;
use neberu::rat::Rat;
use neberu::trace::{verify_kot, walk_from_trace};
use neberu::trit::P as TRIT_P;
use neberu::word::Word;
fn main() {
let ei0 = Gen::imaginary(0);
let gov = Governance::cl(1, 0, 0);
let expr = Expr::term(Rat::one(), Word::from_gens(&[ei0, ei0]));
let (terminal, trace) = gov.canonicalize_traced(&expr);
let walk = walk_from_trace(&trace, &gov);
let kot = verify_kot(&walk, &expr, &gov);
let q1 = kot.as_trit();
let q2 = compute_q2(&kot);
let step = walk.steps().first().expect("exactly one rewrite step");
let n1_val = pack_word(&step.matched); let n1_bits = step.matched.grade() * 2;
let n2_src_bits: usize = 6; let p_bits = TRIT_P.bits() as u128;
let passing_cert: u128 = p_bits | (p_bits << 2) | (p_bits << 4); let n2_val = passing_cert | (p_bits << n2_src_bits); let n2_bits = n2_src_bits + 2;
let n3_bytes = certificate_bytes(n1_val, n1_bits, n2_val, n2_bits);
let n3_val = n3_bytes
.iter()
.rev()
.fold(0u128, |acc, &b| (acc << 8) | b as u128);
let q1_bits = q1.bits();
let q2_bits = q2.bits();
let q_chain = match q1.bits() {
0b10 => "P (== +1 == 0b10 == 2)",
0b01 => "N (== -1 == 0b01 == 1)",
0b00 => "Z (== 0 == 0b00 == 0)",
_ => "INV",
};
let bar = "━".repeat(60);
println!("nēberu v0.0.0");
println!("(potentially)_optimal_kase!PROOF!.neb");
println!();
println!("╔════════════════════════════════════════════════════════════╗");
println!("║ ║");
println!("║ K A S E O P T I M A L I T Y T H E O R E M ║");
println!("║ ║");
println!("║ this program's a proof of correct computation, ║");
println!("║ proving then the proof's correct. ║");
println!("║ ║");
println!("╚════════════════════════════════════════════════════════════╝");
println!();
println!(" This program proves that a computation was performed correctly.");
println!(" It then proves that the proof is correct.");
println!(" Every number below is exact. Nothing is approximated.");
println!();
println!("{}", bar);
println!("THE AXIOM");
println!("{}", bar);
println!();
println!(" The entire system is built from one rule.");
println!();
println!(" A value can be one of three things:");
println!(" N = negative (-1) stored as 01");
println!(" Z = zero (0) stored as 00");
println!(" P = positive (+1) stored as 10");
println!();
println!(" When two values multiply, the sign follows one rule:");
println!(" N · N = P (negative × negative = positive)");
println!(" N · P = N (negative × positive = negative)");
println!(" P · P = P (positive × positive = positive)");
println!(" Z · anything = Z (zero kills everything)");
println!();
println!(" That is the complete axiom. Everything below derives from it.");
println!();
println!("{}", bar);
println!("THE COMPUTATION");
println!("{}", bar);
println!();
println!(" We compute: e1 · e1 in the algebra Cl(1,0,0)");
println!();
println!(" e1 is a geometric basis vector — the kind that squares to -1.");
println!(" (This is the same as the imaginary unit i in complex numbers.)");
println!(" The algebra Cl(1,0,0) has exactly one such vector.");
println!();
println!(" The rule for this algebra:");
println!(" e1 · e1 = -1");
println!();
println!(" ⟨Cl(1,0,0)⟩ e1 · e1");
for step in &trace.steps {
if let Some((ri, pos)) = step.fired {
println!(
" ↓ apply rule {}: e1·e1 → {} @ position {}",
ri, step.after, pos
);
}
}
println!(" ⟨Cl(1,0,0)⟩ {} ✓ done", terminal);
println!();
println!(
" The computation took {} step. The result is {}.",
trace.steps.len(),
terminal
);
println!();
println!("{}", bar);
println!("THE TRACE → N₁");
println!("{}", bar);
println!();
println!(" Every step of the computation is recorded as an exact number.");
println!(" This record is called the trace.");
println!();
if let Some(step) = walk.steps().first() {
println!(" The step that fired:");
println!(
" rule number: {} — the only rule in Cl(1,0,0), implicit",
step.rule_idx
);
println!(
" position: {} — the only possible position, implicit",
step.start
);
println!(
" what matched: {} — two imaginary generators",
trit_word_display(&step.matched)
);
println!();
println!(" Rule index and start position are both 0 in this algebra.");
println!(" There is only one rule and one position where it can apply.");
println!(" They carry no information. Encoding them wastes trits.");
println!();
println!(" N₁ encodes only the informative content: the matched types.");
println!();
println!(" matched types: N N");
println!(" Trit encoding: 01 01 (2 bits per trit, trit 0 at LSB)");
println!();
println!(
" packed: 01 01 = 0b{:04b} = {} = {}",
n1_val,
fmt_hex(n1_val, n1_bits),
n1_val
);
}
println!();
println!(" ┌──────────────────────────────────────┐");
println!(" │ N₁ = {:<29}│", n1_val);
println!(" │ {:<36}│", "The trace. 2 trits. 4 bits.");
println!(" └──────────────────────────────────────┘");
println!();
println!("{}", bar);
println!("THE PROOF");
println!("{}", bar);
println!();
println!(" Now we ask: was the computation correct?");
println!(" \"Correct\" means three things. Each produces a Trit.");
println!();
println!(" ── MINIMAL ───────────────────────────────────────────────");
println!();
println!(" Was every step necessary?");
println!(" The trace has 1 step.");
println!(" Removing it gives us e1·e1 with no reduction applied.");
println!(" That is not -1. So the step was necessary.");
println!();
println!(" Answer: yes → P");
println!();
println!(" ── COMPLETE ──────────────────────────────────────────────");
println!();
println!(" Is the result fully reduced? Can any rule still fire?");
println!(" The result is -1. It is a plain number, not a geometric term.");
println!(" No rule in Cl(1,0,0) applies to a plain number.");
println!(" Nothing more can be done.");
println!();
println!(" Answer: yes → P");
println!();
println!(" ── CONSISTENT ────────────────────────────────────────────");
println!();
println!(" Was there only one possible path to this result?");
println!(" Only one rule exists in Cl(1,0,0): e1·e1 → -1.");
println!(" There is no alternative. No two rules could have conflicted.");
println!();
println!(" Answer: yes → P");
println!();
println!(" ── THE THREE TRITS ───────────────────────────────────────");
println!();
println!(" minimal = P = 10");
println!(" complete = P = 10");
println!(" consistent = P = 10");
println!();
println!(" Together these form a 3-trit word: [P · P · P]");
println!();
let cert_word = {
use neberu::gen::Gen;
use neberu::trit::P;
Word::from_gens(&[
Gen { sig: P, idx: 0 },
Gen { sig: P, idx: 1 },
Gen { sig: P, idx: 2 },
])
};
let cert_val = pack_word(&cert_word);
println!(" Encoded as bits:");
println!(" 10 10 10 = {:06b} = {}", cert_val, cert_val);
println!();
println!(" This word is the certificate.");
println!(
" {} is what a correct computation looks like, in this system.",
cert_val
);
println!();
println!("{}", bar);
println!("THE KOT GOVERNANCE → N₂");
println!("{}", bar);
println!();
println!(" To verify the certificate, we need a standard.");
println!(" The standard defines what an optimal certificate looks like.");
println!();
println!(" The KOT governance has exactly one rule:");
println!();
println!(" [P · P · P] → P the only passing certificate");
println!();
println!(" Everything else fails. This is not a special assumption —");
println!(" it is how governance works: no matching rule means no rewrite.");
println!(" A certificate that does not equal [P·P·P] simply fails to");
println!(" match the one rule that produces a positive verdict.");
println!();
println!(" Enumerating 7 failure cases is unnecessary. The closed-world");
println!(" assumption handles them. N₂ encodes one complete rule:");
println!();
println!(
" source [P·P·P]: 10 10 10 = 0b{:06b} = {} (6 bits)",
passing_cert, passing_cert
);
println!(
" verdict P : 10 = 0b{:02b} = {} (2 bits)",
TRIT_P.bits(),
TRIT_P.bits()
);
println!();
println!(
" concatenated: 10 10 10 10 = 0b{:08b} = {} = {}",
n2_val,
fmt_hex(n2_val, n2_bits),
n2_val
);
println!();
println!(" Note: N₂ = [P·P·P·P] — four P-trits. The passing rule is");
println!(" itself all-positive. The axiom is self-similar.");
println!();
println!(" ┌──────────────────────────────────────┐");
println!(" │ N₂ = {:<29}│", n2_val);
println!(" │ {:<36}│", "The KOT rule. 4 trits. 8 bits.");
println!(" └──────────────────────────────────────┘");
println!();
println!("{}", bar);
println!("THE CERTIFICATE → N₃");
println!("{}", bar);
println!();
println!(" The certificate is the trace joined to the governance.");
println!(" N₁ is what happened. N₂ is the standard.");
println!(" Together they are the complete proof.");
println!();
println!(
" N₁ = {} = {} ({} bits)",
n1_val,
fmt_hex(n1_val, n1_bits),
n1_bits
);
println!(
" N₂ = {} = {} ({} bits)",
n2_val,
fmt_hex(n2_val, n2_bits),
n2_bits
);
println!();
println!(
" N₃ = N₁ | (N₂ << {}) = {} | {} = {}",
n1_bits,
n1_val,
n2_val << n1_bits,
n3_val
);
println!();
println!(" As a 12-bit trit sequence (trit 0 at LSB):");
println!(" 01 01 | 10 10 10 10");
println!(" N N | P P P P");
println!(" ───── | ─────────────");
println!(" N₁ | N₂");
println!(" [matched] | [source → verdict]");
println!();
println!(" The complete proof in 6 trits:");
println!(" [N·N] = what was matched • [P·P·P] = the passing pattern • [P] = verdict");
println!();
println!(" In bytes (little-endian):");
print!(" ");
for b in &n3_bytes {
print!("{:02X} ", b);
}
println!();
println!();
println!(" ┌──────────────────────────────────────┐");
println!(" │ N₃ = {:<29}│", n3_val);
println!(" │ {:<36}│", "The certificate. 6 trits. 2 bytes.");
println!(" └──────────────────────────────────────┘");
println!();
println!("{}", bar);
println!("THE VERDICT → Q₁");
println!("{}", bar);
println!();
println!(" Apply the KOT governance to the certificate word [P·P·P].");
println!();
println!(" ⟨KOT⟩ [P · P · P] = {}", cert_val);
println!(" ↓ rule fires: {} → +1", cert_val);
println!(" ⟨KOT⟩ +1");
println!();
println!(" The sign of +1 is P = 10 = {}.", q1_bits);
println!();
println!(" ┌──────────────────────────────────────┐");
println!(" │ Q₁ = {:<29}│", q_chain);
println!(" │ {:<36}│", "The computation was optimal.");
println!(" └──────────────────────────────────────┘");
println!();
println!("{}", bar);
println!("THE SELF-CERTIFICATION → Q₂");
println!("{}", bar);
println!();
println!(" Now we ask: is the proof itself correct?");
println!(" We apply the same KOT governance to Q₁'s certificate.");
println!();
println!(" Q₁ passed with certificate [P·P·P] = {}.", cert_val);
println!(" That certificate is itself a value in this system.");
println!(" We can check it the same way we checked the computation.");
println!();
println!(" ⟨KOT⟩ [P · P · P] = {}", cert_val);
println!(" ↓ rule fires: {} → +1", cert_val);
println!(" ⟨KOT⟩ +1");
println!();
println!(" The sign of +1 is P = 10 = {}.", q2_bits);
println!();
println!(" ┌────────────────────────────────────────────────────────┐");
println!(" │ Q₂ = {:<45}│", q_chain);
println!(
" │ {:<52}│",
"The proof of the computation is itself correct."
);
println!(" └────────────────────────────────────────────────────────┘");
println!();
println!("{}", bar);
println!("THE FIXED POINT");
println!("{}", bar);
println!();
println!(" Q₁ = {}", q_chain);
println!(" Q₂ = {}", q_chain);
println!();
println!(" Checking the proof again would give P.");
println!(" And again. And again. It does not change.");
println!();
println!(" This is the fixed point: P · P = P");
println!(" The axiom applied to itself gives itself.");
println!(" The system is stable under self-inspection.");
println!();
println!("{}", bar);
println!("ALL FIVE NUMBERS");
println!("{}", bar);
println!();
println!(" N₁ = {:>24} the trace", n1_val);
println!(" N₂ = {:>24} the standard", n2_val);
println!(" N₃ = {:>24} the certificate", n3_val);
println!(" Q₁ = {} the verdict", q_chain);
println!(" Q₂ = {} the verification", q_chain);
println!();
println!(" The proof that e1·e1 = -1 was computed correctly");
println!(" is the number {}.", n3_val);
println!(" It fits in 2 bytes.");
println!(" The verdict is {}.", q_chain);
}