1. 核心概念词典的精细化

生成性基础：迈向一个时间性的数学本体论》
"同伦类型论通过将证明解释为路径，为数学基础注入了革命性的几何直观。然而，我们主张，这一洞见被其仍然依赖的静态与无限的本体论预设所限制。本文提出生成性基础——一个将HoTT的几何见解与有限时间公理相结合的新范式。我们引入一个原始的、有限的时间类型，并将数学对象重新构想为在时间中生成实例的规则。我们证明，连续性、无限性乃至宇宙层级本身，都可以通过规则同伦和隐性频率转换的概念自然涌现。这一框架不仅解决了HoTT中的若干概念困境，更为数学在认知科学和物理基础中的应用开辟了新径。"

演示一：自然数的"祛魅"

传统HoTT：

data Nat : U₀ where

  zero : Nat

  succ : Nat → Nat

-- 承诺了一个完整的、实际的无限集合

我们的框架：

-- 时间是最基础的假设

postulate Time : U₀

postulate t_max : Time

-- 自然数作为在时间中生成的规则

NatRule : (t : Time) → U₀

NatRule t = Fin (toℕ t)  -- 在时间t，我们只有直到t的自然数

-- 我们并不拥有"所有"自然数，但我们拥有生成任意大自然数的能力

can_generate_large : Π (n : &#8469;), Σ (t : Time), (n < to&#8469; t)
"我们不再需要承诺一个完成了的无限集合 &#8469;。我们只承诺一个过程，通过它，对于任何你想要的有限界，我都能在有限时间内生成满足条件的自然数。这更贴近我们真实的数学实践和物理现实。"

路径的"物理化"

一条路径 p : a ≡ b 是一个从连续区间 I 到类型的映射。

我们的框架： 一条路径是两个规则输出通过一系列离散的协调步骤建立的等价关系。

-- 离散路径：一系列协调的转换

data DiscretePath {A : Time → U&#8320;} (x : A t&#8320;) (y : A t_n) : U&#8320; where

  refl : DiscretePath x x

  step : Π {t t' : Time}

        {a : A t} {b : A t'}

        (f : Converter t t' a b)  -- 隐性频率转换器

        (p : DiscretePath b y)

        → DiscretePath a y

"连续性不是数学的起点，而是数学过程在极高'时间分辨率'下涌现的终点。我们不是在假设连续统，而是在建构连续性的现象。"
实数连续统的建构

传统HoTT的困境：

[list][*]

仍然需要选择：戴德金分割（依赖幂集）或柯西序列（依赖无限序列）

[*]

两种方法都依赖于某种形式的实无限

[*]

与计算语义存在张力

[/list]

我们的优雅方案：

-- 一个"实数"是一个生成任意精度近似值的规则

record RealNumber : U&#8321; where

  field

    generator : Π (ε : &#8474;&#8330;)  -- 对于任何正有理精度ε

                → Σ (t : Time)  -- 在某个时间t内

                → Σ (q : &#8474;)     -- 生成一个有理数q

                → (error_bound : | real_value - q | < ε)

  -- 隐性频率转换器确保不同精度下输出的一致性

  field

    consistency : Π (ε&#8321; ε&#8322; : &#8474;&#8330;) (q&#8321; q&#8322; : &#8474;)

                → generator ε&#8321; ≡ (t&#8321;, q&#8321;)

                → generator ε&#8322; ≡ (t&#8322;, q&#8322;)

                → | q&#8321; - q&#8322; | < ε&#8321; + ε&#8322;

"我们不再讨论'实数的完整集合'，我们只讨论可以按需生成实数近似值的规则。我们不再问'实数是什么'，而是问'我们如何计算实数'。这不仅仅是构造主义，这是将数学重新奠基在交互过程而非静态存在之上。"