A 16×16 multiplication table that encodes quoting, evaluation, branching, recursion, an 8-state counter, and IO — all as lookups in the same table. 83 Lean theorems, zero sorry. The project asks: can a finite algebra with a single binary operation be forced by axioms to contain its own representation layer? The answer is yes. Axiom-driven SAT search finds the constraints, Lean verifies the witness. I should be upfront: Claude wrote most of the Lean proofs and Z3 search scripts. My role was the ontological framework, the axiom design, and deciding what to search for and why. The AI-human split was roughly: I provided the "what should exist and why," Claude provided the "here's the code that proves/finds it." Every Lean theorem compiles independently regardless of who typed it. Universal results (hold for all satisfying algebras, not just this table): every model is rigid, judgment and synthesis provably cannot commute, and the tester's acceptance partition carries irreducible information that structure alone can't determine. The specific table fits in 256 bytes and can be recovered from a shuffled black-box oracle in 62 probes. https://github.com/stefanopalmieri/Kamea