Two
plain-language theorem explainer
The two-point type of Martin-Löf type theory is identified with Lean's Boolean type: exactly two closed inhabitants, false and true. Downstream PRC and constants work cite it whenever a binary choice, bit, or two-element discrete space is needed. The declaration is a pure abbreviation with no proof obligations.
Claim. Write $2$ (or $\mathbb{B}$) for the canonical two-element type of Martin-Löf type theory / CIC. In this development it is identified with Lean's Boolean type, whose closed terms are $\mathsf{false}$ and $\mathsf{true}$.
background
The module sits in the Primitive Recognition Calculus (PRC) type-theory parse layer. That layer reads the distinction calculus into a small type theory so that recognition acts, cost, and arithmetic can be stated with ordinary constructors and eliminators rather than ad hoc encodings.
The two-element type is the standard discrete bit of MLTT/CIC: a type with exactly two canonical closed terms. Here it is not re-axiomatized; it is Lean's built-in Bool, so pattern matching, decidable equality, and Boolean algebra are inherited for free.
Nearby siblings (canonicity, no-confusion, and the type-theory system that embeds the distinction calculus) treat this type as the discrete two-point space against which expressiveness and non-degeneracy of the parse are checked. Upstream "canonical" objects in arithmetic, traces, and dyadic protocols are separate; they only share the naming habit of fixing a preferred representative.
proof idea
There is no proof. The declaration is a one-line abbreviation equating the PRC name for the two-element type with Lean's Boolean type. All subsequent reasoning about inhabitants, cases, and decidability is ordinary Boolean reasoning in Lean.
why it matters
A named two-point type is the discrete substrate for binary choices throughout the monolith: path-space actions at the cost minimum, positivity of the fundamental tick $\tau_0$, $\alpha^{-1}$ band witnesses, planetary gap-skip ratios on the $\varphi$-ladder, and 3D domain-coarsening cost comparisons all pull this abbreviation (forty use sites in the graph head alone).
In the Recognition framework it is the type-theoretic stand-in for a single distinction outcome (yes/no, left/right, on/off) before continuous J-cost and the forcing chain (T5–T8) enter. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live upstream in the unified forcing chain. Its job is to keep the PRC parse honest: the type theory that realizes $\Delta$ must contain a genuine two-element type, not a collapsed or infinite surrogate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.