boolLogicSystem_embeds_delta
plain-language theorem explainer
Classical two-valued logic realizes the primitive δ distinction: there is a PRC embedding of the endpoint/trace core into the Bool carrier. Anyone arguing that the Law of Logic already contains Recognition's minimal distinction cites this witness. The proof is a one-line application of the general expressive-system embedding theorem to the Bool instance and its expressiveness certificate.
Claim. There exists a PRC embedding into the formal system whose tokens are the Booleans with $false \neq true$: endpoint tokens map to those two values, finite traces map to expression lengths, distinction is inequality of tokens, and trace extension is the length order. Equivalently, the two-valued logical carrier is nonempty as a PRC embedding target.
background
Primitive Recognition Calculus (PRC) isolates a minimal distinction core $\delta$: two endpoints (left/right) and finite traces that extend by length. A PRC embedding into a formal system $F$ is a pair of maps (endpoints $\to$ tokens, traces $\to$ expressions) that preserve the endpoint distinction and the trace-extension order.
The module builds concrete formal-system witnesses via ofTwoDistinct: any type with two unequal primitives becomes a system whose tokens are the type's elements, expressions are natural numbers (trace lengths), distinction is inequality, and extension is $\le$ on lengths. The Bool witness is exactly that construction on $false$ and $true$.
Upstream, any expressive formal system admits a PRC embedding (FormalSystemEmbeddingTarget_proved packages PRCEmbeddingInto.ofExpressive). Expressiveness for the two-token systems is discharged by the matching ofTwoDistinct_expressive lemma, so Bool is already certified expressive before this theorem is invoked.
proof idea
Term-mode one-liner. Apply the general theorem that every expressive formal system is a PRC embedding target, specializing to the Bool system and feeding the already-proved expressiveness certificate for that system. No case analysis on endpoints or traces is local to this proof; those obligations live inside the general constructor and the two-distinct expressiveness lemma.
why it matters
This is Item 4 (concrete) in the inevitability instances: the Law of Logic's own carrier contains the $\delta$ core because distinguishing true from false is already the primitive distinction. Downstream it is the first conjunct of named_foundations_embed_delta, which widens the claim to four structurally different foundations (logic, Peano $0\neq 1$, set-theoretic $\emptyset\neq{\emptyset}$, type-theoretic $\mathbf{2}$), showing the distinction is not a Bool notation artifact.
It also feeds named_foundations_not_degenerate: non-emptiness of the embedding implies the system is non-degenerate, hence realizes $\delta$ on the dichotomy side. In the broader Recognition forcing picture this anchors the claim that any foundation expressive enough to tell two primitives apart already embeds the PRC core, before cost functionals (J), $\phi$, or the eight-tick octave enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.