qpell.com

QPELL is a project concerned with formal structure in discrete computation.

Q-Lean is a Lean-verified semantic kernel developed within this project, defining memory and computation in terms of observable behavior rather than internal representation.

Version 0.3 provides a closed and axiom-free foundation covering deterministic recall, observational equivalence, non-destructive deletion, and reversible state evolution in a non-metric setting.

Executable systems are treated as projections of this kernel and are not used to justify or extend its semantics.