We introduce TTS, a dependent type theory in which semantic composition is represented by horn filling and distinctions between possible completions are witnessed relative to explicit measurement regimes. TTS replaces globally canonical composition with regime-indexed indiscernibility and constructive apartness, allowing filler spaces to be classified as canonical when all completions are observationally connected and forked when two warranted completions are positively separated. Separation witnesses enter the calculus only through measurement contexts recording actual instrument outputs, yielding conservativity, provenance, and a no-fork-from-the-empty-record result. We prove that forks persist under refinement while canonicity may fail, and characterize exactly when an identification made by one regime can consistently coexist with a separation made by another. This framework supports a geometric account of Fregean sense as a choice of filler, reference as the boundary constraining that choice, and hyperintensional difference as measured apartness, while providing a falsifiable bridge to stratified representation spaces and branching behaviour in language-model generation.

翻译：我们提出TTS，一种依赖类型论，其中语义组合由horn填充表示，而可能完成之间的区分相对于明确的度量机制得到见证。TTS用机制索引的不可区分性和构造性分离取代了全局规范组合，允许填充空间被分类为：当所有完成在观察上相连时为规范空间，当两个受保证的完成被正向分离时为分叉空间。分离见证仅通过记录实际仪器输出的度量上下文进入演算，从而得到保守性、来源性以及“无空记录分叉”结果。我们证明分叉在精化下保持，而规范性可能失效，并精确刻画了一个机制做出的识别何时能与另一机制做出的分离一致共存。该框架为弗雷格意义（作为填充的选择）、指称（作为约束该选择的边界）以及超内涵差异（作为度量的分离）提供了几何解释，同时为语言模型生成中的分层表示空间和分叉行为提供了可证伪的桥梁。