IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCTypeTheoryParse
Formal bridge from Martin-Löf type theory (CIC) into the Primitive Recognition Calculus. It packages Lean's Bool as the canonical two-point type, builds a type-theory system object, and proves that system is expressive, non-degenerate, and embeds the distinction structure Delta. Downstream foundation parsers cite it to treat type theory as a concrete realization of PRC distinction. The argument is mostly definitional packaging plus short canonicity and no-confusion lemmas.
claimLet $\mathbf{2}$ be the canonical two-element type (with closed terms $\mathsf{ff},\mathsf{tt}$). The module defines a type-theory system $\mathsf{TT}$ over $\mathbf{2}$ and asserts: canonicity and no-confusion for $\mathbf{2}$; $\mathsf{TT}$ is expressive and expression-reflexive; $\mathsf{TT}$ is non-degenerate; $\mathsf{TT}$ embeds the distinction structure $\Delta$; and type theory realizes $\Delta$.
background
Primitive Recognition Calculus treats distinction as the primitive act: a system must be able to separate alternatives without collapsing them. The upstream module PRCDistinctionDichotomy supplies that dichotomy structure (call it $\Delta$): a minimal two-sided split with non-confusion of the sides.
This module takes the standard constructive setting of Martin-Löf type theory / CIC and reads it in those terms. The carrier is Lean's Bool, presented as the canonical two-element type $\mathbf{2}$ whose closed inhabitants are false and true. Canonicity says every closed term of $\mathbf{2}$ is definitionally one of those two; no-confusion says the two constructors are distinct.
Around that carrier the module assembles a small system object $\mathsf{TT}$ (expressive power, embedding of $\Delta$, expression-reflexivity, non-degeneracy). The point is not a full metatheory of type theory, but a parse: type theory already contains a faithful model of the PRC distinction seed.
proof idea
Definition-heavy module with short supporting lemmas rather than a single deep proof. Two is an alias for Bool as $\mathbf{2}$. Canonicity and no-confusion are the standard Bool case-split / constructor-distinctness facts, packaged for PRC consumption.
ttSystem packages the type-theory side as a system record. The named properties (ttSystem_expressive, ttSystem_embeds_delta, ttSystem_exprReflexive, ttSystem_not_degenerate) are then discharged by unfolding that record against the Bool dichotomy and the upstream $\Delta$ interface. The capstone type_theory_realizes_delta composes those facts into the single claim that CIC/MLTT realizes the distinction structure.
why it matters in Recognition Science
Recognition Science needs a clean hand-off from abstract distinction (PRC) to a concrete formal calculus that working foundations already trust. This module is that hand-off: it shows ordinary type theory is not an alien language but a realization of $\Delta$.
It is imported by PRCFoundationsParsed, which assembles the parsed foundation layer used higher in the Primitive Recognition Calculus stack. Without the embed/realize lemmas here, later modules cannot cite type theory as a witness that the distinction dichotomy is inhabited in a standard constructive setting.
Relative to the forcing chain (T0–T8), this sits upstream of physics extraction: it stabilizes the logical substrate on which cost, $\phi$, and the eight-tick structure are later forced. It does not itself force $J$, $\varphi$, or dimension; it only certifies that the distinction seed has a type-theoretic model.
scope and limits
- Does not prove full canonicity or normalization for all of MLTT/CIC, only the two-point type.
- Does not construct physics constants, J-cost, or the phi ladder.
- Does not claim type theory is the unique realization of Delta.
- Does not discharge downstream parsed-foundation theorems beyond the import edge.
- Does not address classical two-valued logic outside the constructive Bool model.