AlgorithmicSpec
plain-language theorem explainer
An algorithmic specification is a finite binary description paired with a partial enumeration of state encodings. Exclusivity and discrete-necessity arguments cite it as the carrier type for "frameworks that can be listed by an algorithm." It is a plain two-field structure (forward-declared to break import cycles), with no proof obligations.
Claim. An algorithmic specification consists of a finite binary string (the description) together with a map sending each natural number $n$ to an optional binary word (an enumeration of candidate state encodings).
background
The shared Framework module holds only core carrier types used by both NoAlternatives and the necessity proofs, so those developments need not import each other. An algorithmic specification is the discrete stand-in for "a program that lists states": a finite bitstring description, plus a generator that on input $n$ may return a bitstring code or fail.
Downstream, a state space is said to have an algorithmic specification when there exist such a generator and a decoder so that every state appears as the decode of some generated code. The structure is a forward declaration from DiscreteNecessity, kept here solely to avoid circular imports. Upstream edges into winding-order and active-edge constants are incidental name collisions, not conceptual premises of this carrier.
proof idea
No proof. The declaration is a structure with two fields: a finite List Bool description and a generator ℕ → Option (List Bool). Field types are ordinary Mathlib/core types; there are no axioms, instances, or tactic blocks.
why it matters
This carrier is the sole ingredient of HasAlgorithmicSpec, which asserts that a state space is surjectively covered by some algorithmic specification via a decoder. That predicate is the discrete half of the exclusivity story: frameworks admitted into the comparison class must be algorithmically enumerable, so continuous or non-constructive alternatives fall outside the class before any forcing-chain comparison (T0–T8, RCL, eight-tick octave) begins.
By living in the shared Framework module it lets NoAlternatives and DiscreteNecessity share one definition without mutual imports. It does not itself force discreteness of physics; it only names the data that later necessity theorems quantify over.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.