This paper presents a finite modal semantics where truth is closed under admissible continuation, then refined by discounted value, and finally certified by residual tests. The admissibility kernel is the classical greatest fixed point of a one-step predecessor expressing that some choice cell has all compatible successors inside a set. Certified choices are exactly local witnesses; the discounted value transformer is defined only over those witnesses; value-refined modal bisimulation is the coarsest local equivalence preserving formulas, kernel, certified choices, Bellman values, greedy sets, residual certificates, and public release certificates. A canonical pseudometric refines this equivalence: it is the unique fixed point of a Hausdorff-lifted choice-matching transformer over certified choices; its zero set is the value-refined bisimulation, and the optimal discounted value is one-Lipschitz with respect to it. Any approximate quotient incurs only a distance-bounded value error. Branching choice-cell and locus presentations place choice inside the model; the transition presentation is a conservative retraction. The same engine is applied to a public share-alike release fragment: attribution as label preservation, same-license propagation as derivative closure, no downstream restriction as admissibility, and the BY-SA witness as a residual-stable certificate. Finite examples show that altering the order of truth, admissibility, value, quotienting, public derivation, and certification changes the semantics.

翻译：本文提出一种有限模态语义，其中真值在可容许延续下封闭，随后通过折扣值精化，最后经残差测试认证。可容许核是单步前驱算子的经典最大不动点，该算子表达某个选择单元与集合内部所有兼容后继相关联。认证选择恰为局部见证；折扣值变换器仅定义于这些见证之上；值精化模态互模拟是保持公式、核、认证选择、贝尔曼值、贪婪集、残差证书及公共发布证书的最粗局部等价关系。一个标准伪度量精化该等价关系：它是基于认证选择上Hausdorff提升的选择匹配变换器的唯一不动点；其零集即值精化互模拟，最优折扣值关于该零集满足1-李普希兹性质。任何近似商仅引入有界距离值误差。分支选择单元与位点表示将选择置于模型内部；转移表示为保守收缩变换。相同引擎应用于公共共享相同许可证发布片段：归属即标签保持，同许可传播即衍生闭包，无下游限制即可容许性，BY-SA见证即为残差稳定证书。有限示例表明：真值、可容许性、值、商化、公共派生与认证的顺序改变将导致语义变化。