unaryEncode
plain-language theorem explainer
Unary encoding sends each natural number n to the Boolean list of length n filled with true. Verification and exclusivity arguments cite it when they need a concrete, length-faithful code for naturals inside algorithmic specifications of state spaces. The body is the standard list replicate of true.
Claim. The unary encoding of a natural number $n$ is the Boolean list consisting of exactly $n$ copies of $\mathsf{true}$.
background
The module supplies shared framework definitions for NoAlternatives and necessity proofs, isolating core notions so those developments do not import each other circularly.
An algorithmic specification is a generator that, on input $n$, optionally emits a Boolean code; a state space has an algorithmic spec when every state is the decode of some generated code. Unary encoding is the simplest length-faithful map $\mathbb{N}\to\mathrm{List},\mathrm{Bool}$ used to build or transport such codes.
The companion fact that the encoded list has length $n$ is immediate from the definition and is marked simp for downstream rewriting.
proof idea
Pure definition: apply list replicate of the Boolean true, $n$ times. No lemmas or tactics; noncomputable only because the ambient framework mixes classical choice elsewhere.
why it matters
Feeds the predicate that a state space admits an algorithmic specification (every state is decode of some generated Boolean code) and the simp lemma equating encoded length with $n$. That length identity is the first step in transporting algorithmic specs along equivalences with $\mathbb{N}$, which is how exclusivity arguments show competing frameworks are enumerable on the same footing as Recognition Science. It is scaffolding for the verification layer, not a physics forcing step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.