HasAlgorithmicSpec
plain-language theorem explainer
A state space admits an algorithmic specification when some algorithm enumerates bitstrings that decode onto every state. Exclusivity and zero-parameter arguments cite this to mark frameworks with no free continuous knobs. The body is pure existence: a generator plus a decoder that jointly cover the whole space.
Claim. A type $S$ has an algorithmic specification if there exist an algorithmic bitstring generator and a partial decoder $\mathrm{decode} : \{0,1\}^* \to S_\bot$ such that for every state $s \in S$ there is a finite code produced by the generator with $\mathrm{decode}(\mathrm{code}) = s$.
background
This module supplies shared framework vocabulary for the NoAlternatives and necessity developments, isolating core definitions so those proofs do not import each other circularly. The local setting is an abstract physics framework: a state space, evolution rules, observable extraction, and predictive capability.
An algorithmic specification is the discrete enumerability half of that interface. Sibling AlgorithmicSpec is the generator object (a machine that, on input $n$, may emit a bitstring). The predicate here only asks that some such generator, paired with a decoder from bit lists into the state type, hits every state. Continuous parameter surfaces and real-valued knobs are deliberately outside this notion; they appear later when zero-parameter status is defined.
Upstream foundation material (gap derivation, finite-dimensional Hamiltonian emergence, primitive recognition traces) motivates why RS itself is expected to be algorithmically presentable, but this definition does not depend on those theorems mathematically: it is pure type-level coverage by a generator.
proof idea
Definition, not a proved theorem. The proposition is the nested existence statement: there is an AlgorithmicSpec, and a decoder List Bool → Option StateSpace, such that every state is witnessed by some natural $n$ and some code with spec.generates n = some code and successful decode. No tactics or lemmas are applied; the body is the Prop itself.
why it matters
This is the gate used by HasZeroParameters: a physics framework has zero parameters precisely when its state space satisfies algorithmic specification (no adjustable reals in the presentation). Downstream, the parameter-surface development cites that link to prove the one-parameter framework does not have zero parameters, via exclusion of a real knob once algorithmic zero-parameter status is assumed.
In the Recognition exclusivity program this is the discrete half of "no alternatives": frameworks that cannot be enumerated algorithmically sit outside the zero-parameter class that RS claims for itself (forcing chain T0–T8, RCL, phi-fixed structure). It does not yet prove RS uniqueness; it only supplies the shared predicate those uniqueness and necessity arguments share.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.