Data transformation correctness is a fundamental challenge in data engineering: how can we verify that pipelines produce correct results before executing on production data? Existing practice relies on iterative testing over materialized data. A common cause of errors is the absence of formal reasoning about grain -- the level of detail of data -- so transformations inadvertently change granularity, yielding pathologies like fan traps (metric duplication) and chasm traps (data loss). We introduce grain theory, a type-theoretic framework that elevates grain to a composable property of any algebraic data type. It has two phases. First, a denotation of data: grain itself, defined by irreducibility and isomorphism, with no reference to functional dependencies; three grain relations forming a bounded lattice whose axioms recover Armstrong's on product types; the entity key as a derived grain; and grain-determined behavioral classes -- together the type-level triple (G[R], EK[R], BC[R]). Second, a denotation of transformations: every transformation $h$ has a grain lift $\varphi(h)$. For collections of product types under the relational algebra we prove an equi-join grain inference theorem and present CalcG, a decidable algorithm that composes grain lifts across a pipeline DAG. The central theorem -- the grain homomorphism -- ties the phases together: grain projection commutes with transformation, and grain lifts compose ($\varphi(h_2 \circ h_1) = \varphi(h_2) \circ \varphi(h_1)$). Grain-correctness is therefore verifiable at design time, before any code or query runs. As corollaries, fan traps emerge as schema-detectable grain-relation violations; chasm traps localize to a specific ordering-chain pattern; and behavioral-class violations, such as point-in-time queries on the wrong collection type, become compile-time type errors. All theorems are mechanically verified in Lean 4.

翻译：数据转换的正确性是数据工程中的一个基本挑战：如何在生产数据上执行之前验证管道是否能产生正确的结果？现有实践依赖于对物化数据的迭代测试。错误的常见原因在于缺乏对粒度（即数据的详细程度）的形式化推理，导致转换在无意中改变粒度，从而产生诸如扇形陷阱（度量重复）和峡谷陷阱（数据丢失）等问题。我们引入了粒度理论，这是一个类型论框架，它将粒度提升为任何代数数据类型的可组合属性。该理论包含两个阶段。第一阶段是数据的外延：粒度本身，由不可约性和同构性定义，且不涉及函数依赖；形成有界格的三种粒度关系，其公理在积类型上恢复了阿姆斯特朗公理；作为派生粒度的实体键；以及由粒度决定的行为类——共同构成类型层级三元组（G[R], EK[R], BC[R]）。第二阶段是转换的外延：每个转换 $h$ 都有一个粒度提升 $\varphi(h)$。针对关系代数下的积类型集合，我们证明了等值连接粒度推断定理，并提出了CalcG算法，该算法是可判定的，能够组合管道有向无环图中的粒度提升。核心定理——粒度同态——将两个阶段联系起来：粒度投影与转换可交换，且粒度提升可组合（$\varphi(h_2 \circ h_1) = \varphi(h_2) \circ \varphi(h_1)$）。因此，粒度正确性可以在设计时进行验证，即在任何代码或查询运行之前。作为推论，扇形陷阱表现为模式可检测的粒度关系违反；峡谷陷阱定位到特定的排序链模式；而行为类违反（例如对错误集合类型执行时间点查询）则变为编译时类型错误。所有定理均在Lean 4中经过了机械化验证。