Config
plain-language theorem explainer
A configuration of n independent binary distinctions is a map from the n channels to a Boolean side. Anyone building cost-from-distinction, additivity, or calibration arguments cites this as the concrete carrier type. It is a one-line type abbreviation, not a proved statement.
Claim. For each natural number $n$, a configuration of $n$ channels is a function $\mathrm{Fin}\, n \to \{\mathrm{true},\mathrm{false}\}$: each channel is assigned one of two sides.
background
In the multi-distinction geometry layer of Primitive Recognition Calculus, the basic object is a finite collection of independent binary distinctions (channels). Each channel has two sides; a global assignment of sides is a configuration.
The type is the set of maps from the finite index set of size $n$ into Booleans. Downstream, CostFromDistinction abstracts this carrier into a ConfigSpace with empty configuration, join, consistency, and independence, then equips it with cost functions whose additivity and calibration properties force the recognition-work constraint.
Sibling operators in the same module (difference operators that flip one channel while holding others fixed, vertex/edge incidence) act on this type; the present abbreviation only names the underlying assignment space.
proof idea
Pure definitional abbreviation: Config n is definitionally equal to Fin n → Bool. No proof obligations, tactics, or lemmas.
why it matters
This is the concrete configuration type that CostFromDistinction instantiates. Downstream results include ConfigSpace and CostFunction on Config, the empty-join identities additive_emp_left and additive_emp_right, strict additivity for independent inconsistent joins, three-fold additivity as the induction step, and Calibration (a distinguished inconsistent α with positive cost δ). Those theorems turn independent binary distinctions into an additive cost calculus that underwrites the recognition-work constraint and, further up the chain, the J-cost uniqueness step (T5) of the forcing chain. Without a fixed carrier for n-channel side assignments, the monoid and independence axioms have nothing to act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.