feat(proofs): extend type safety — or/sub/mul operators + capability preorder#80
Merged
Merged
Conversation
…preorder Tier 1 + Tier 3 extensions on the now-verified WokeLang.lean, each machine- checked under Lean 4.30.0 (lean-proofs CI gate), still sorry-free, no axioms. Tier 1 (base operators) — HasType + Step rules + full progress/preservation: - `or` (logical, mirrors `and`) - `sub`, `mul` (integer, mirror `add`) Tier 3 (capability lattice): - `capSubsumes_refl`, `capSubsumes_trans` — capability subsumption is a preorder. Deliberately the order shape echo-types' `DecorationStructure` requires (≤-refl/≤-trans), keeping WokeLang on-path for a future echo layer. Also checked echo-types `main` for design compatibility (AUDIT.md): the echo layer is a Mode-indexed decoration ON TOP of the base type system (the Ephapax L3 precedent), so these base extensions are orthogonal/compatible. Still open in Tier 1: comparisons (lt/gt/le/ge), div/mod (panic), float, arrays. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
hyperpolymath
marked this pull request as ready for review
June 14, 2026 04:23
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Builds on the now-verified
WokeLang.lean(#79) by extending the type-safety proofs — Tier 1 (base operators) + Tier 3 (capability lattice) fromAUDIT.md. Every addition is machine-checked under Lean 4.30.0 by thelean-proofsCI gate, still sorry-free, no axioms.Tier 1 — base operators
Each adds a
HasTyperule +Steprule and fullprogress/preservationcoverage (including the congruence and error-propagation cases):or(logical) — mirrors the provenand.sub,mul(integer) — mirror the provenadd.Tier 3 — capability lattice
capSubsumes_refl,capSubsumes_trans— capability subsumption is a preorder.This is deliberately the order shape echo-types'
DecorationStructurerequires (≤-refl/≤-trans), keeping WokeLang's capability lattice on-path for a future echo/loss layer.Echo-types design compatibility
Per your request, I checked echo-types
mainbefore extending, and documented it inAUDIT.md. The precedent isEchoEphapaxBridge: Ephapax (a linear-typed language) portsEchoLinear+EchoResidueinto its prover as a separate L3 layer. So the echo/loss layer is aMode-indexed decoration on top of the base type system — these base-operator extensions are orthogonal and compatible, and the capability preorder is a stepping stone toward it.Verification
Still open in Tier 1 (next increment)
Ordering comparisons (
lt/gt/le/ge),div/mod(divide-by-zero →errorpanic, reusing the proven panic fragment), float variants, andarraytyping.https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
Generated by Claude Code