H0mework

首发论文 · 2026-10-07

状态不是历史，源才是

过程同一性、责任承接与最小修订

The State Is Not the History, the Source Is: Identity, Responsibility, and Minimal Revision in Processes

正文 PDF补充材料arXiv 版DOI 10.5281/zenodo.23210084
  • 26条主张
  • 127个 Lean 模块
  • 1589个声明
  • ✓ 内核检查全部通过
00κ
纸带：源程序 prog κ(T)钉板：左为 T，右为 read(prog T)；钉高即根标签 a、b、c表盘：读数 ev = fold κ(T)定理 3.9。每棵树的整树程序逐行打孔：每个语法节点一行，变量与双线性节点各打一个计费孔。第一读头累计计费孔，r(prog T) = β(T) = 2、5、8、11、14，只由树形决定。κ ≡ 0 时，表盘对每棵树都读 0；第二读头从不求值，探针跳过映射通道，仍逐棵重建原树。把 κ 切到节点计数：只有映射通道和表盘改变。

摘要

提问给过程留下一个必须处置的需求；即使几个读数彼此吻合，答案仍须说明它属于哪一次运行。本文沿同一读数、同一源对象、同一次发生、同一笔责任的四级同一性，构造一条由源亲自走完的正向链：原发生交出完整源程序，程序被实际执行，也能被独立逆读；执行生成自己的责任行并逐步付款；结清之后，实际动作提出下一问。

展开全文

第一环把读数与源分开。任意根树与任意构造子函数生成一个整树程序：执行迹的长度恰为由树语法生成的预算，只读语法的解析器从程序恢复整棵树；即使构造子恒取零、所有树的执行值都相同，程序仍单射地保存全树。在此之上，推导与模律生成的关系恰为求值核；两个源词在历史中同一，当且仅当每一拍的（旧值，效应）差都由该拍关系解释；演化等式覆盖完成载体的每个元素。换一种实现时，共同发生生成唯一比较。

第二环让责任从源中出生。原发生上登记的完整环境与表达式无需任何旧承担者，便生成一条新的数学责任行：预算是剩余的原语计算数，每一步实际执行都是严格付款，预算耗尽处到达局部结算，完成值等于原表达式的求值；已付执行迹同时是关系收据，全部旧账作为同源余项保留。对一般责任，给定覆盖每个同债当前的总律，真实付款同样生成有限结算历史与终账回执。

第三环让回答提出下一问。结清后，实际动作把已付关系放回当前的真实环境：新请求的值恰是原词在这次更新下的效应，预算严格为正，首步即一次新的责任出生；现成的询问运行时沿这些递归帧逐拍运行，无需外部的未来请求表。旧理论对一项需求既无表达也无合法实现时，扎根失败生成最小扩充：在账、关联与主张三个坐标上，每个容许扩充经唯一忠实映射接收它；任一有类型修订都把这个方向送入新根的首次写入，固定两拍实例的第二拍由同一新根直接回答。

下一问并非空手出发。同一个源程序在执行效应的同时折叠这次访问的完整时间，保留两段历史与作用差的逆判据；全部作用者的读数共同恢复全词模型；任意源程序的已付查询都在同根、同访问处生成新的责任准入，物理与低层两种类型的库存越过准入后被逐项读回；默认运行亲自执行这一源自产请求，连同旧、新两棵子树逐节点付款。问题因此不只等待答案：它的执行、结算与失败都在提出下一问。定理与构造以 Lean 4 形式化；完整书面证明见正文与补充材料，形式化范围见附录 D。

关键词：过程同一性；增量计算；源程序执行；语义关系核；忠实实现；责任账；最小修订；依赖类型；形式化

主张与证明

每条主张都登记在逐主张映射中。展开一条，可以看到它的陈述、在论文中的位置，以及证明它的 Lean 模块与复现程序。

  1. core.C23整树程序：执行、计费与独立逆读配图§3.4

    任意Root、Carrier与任意atOccurrence:Root→List Carrier→Carrier：整树生成程序，执行值为fold的原生单基，预算由树语法β生成，执行迹长度=β；只读语法的parser恢复整棵树；atOccurrence恒零时程序仍单射。装入询问后值、出处、代价同时读出。

    位置：§3.4 命题3.7、定义3.8、定理3.9；§6.5 命题6.11；§10.1

    Lean 模块 · 7

  2. core.C3固定过程后继与历史§2.1

    任意fixed-law process：stateAt为完整living current的单射表示；successor精确认回root编译结果并保law surface；相同current后继相同；任意fuel生成历史。

    位置：§2.1 定义2.1、命题2.2

    Lean 模块 · 2

  3. core.C9原生状态的自由载体与任意二元运算§2.2–§2.4

    ∀固定SourceNativeLivingRootProcess：δ:State→Freeℤ(State)单射，Aδ(s)=δ(successor s)；任意原read唯一线性延拓并与作用对易；任意f:X→Y→Z生成双加性lift、mixed effect与normalize；Field的nextWitness保原tick.next。

    位置：§2.2–§2.4 命题2.3、定义2.4、命题2.5

    Lean 模块 · 3

  4. core.C7效应、混合项与Type中推导§3.1–§3.3

    任意sorts、加法交换群、变量环境；有限Expr的递归effect与有序mixedTerms给eval(old+inc)=eval(old)+effect，双线性节点保左右与joint三项；normalize在Type中生成Derivation env e (const(eval e env))。

    位置：§3.1–§3.3 定义3.1–3.2、命题3.3–3.6

    Lean 模块 · 3

  5. core.C8关系核、完成载体与逐元素演化§4

    任意交换环R与R-模、固定环境：range(relationMap)=ker(evaluation)；固定runtime、实际readMaterial与加性环境投影：两词在completion同像⇔每stage的(old,effect)差属于该stage生成关系范围；successor覆盖全部completion元素；Fock实现中原word的Fibre见证沿生成后继延展。

    位置：§4 定理4.4、4.6、4.7、命题4.8

    Lean 模块 · 7

  6. core.C10忠实实现与唯一比较§5

    固定SourceNativeLivingRootClosure：规范Process有FaithfulRealization；任意忠实process任意event恢复规范发生与全部安装投影、event=emitted；任意两忠实实现经共同occurrence生成整个编译相容的双向表示；任意候选逐current事件映射逐点等于生成比较。

    位置：§5 定义5.1、命题5.2、定理5.3

    Lean 模块 · 2

  7. core.C1生命周期三律§6.1

    任意词汇V、NativeResponsibilityProcess P、合法edge与slot：fresh allocation⇒admitted；newly live⇒admitted或reopened；live→nonlive⇒obligationTerminal；Run.history_eq保序历史。

    位置：§6.1 命题6.1

    Lean 模块 · 1

  8. core.C12债务激活与逐事件整账编译§6.2–§6.3

    ∀world N与DebtActivationLaw：扩世界support=base×Option DebtState，inactive纤维恢复全部旧行，active纤维恢复旧行加唯一law-owned债行；固定lower root/current的OccurrenceIndexedSourceAt生成LedgerWriteEvolution、LedgerTerminalEvolution或同行U7审计。目标6实例：2+4→3+3行动债1→0付款与目标终账分开读。

    位置：§6.2–§6.3 定义6.2–6.3、命题6.4–6.5、表2

    Lean 模块 · 3

  9. core.C2同债总律生成有限结算§6.4

    固定process与origin debt：不增—严格降—不增付款宏复合严格下降，续行关系良基、无自返、零预算无付款；给覆盖全部同债current的Noetherian总emit后，每个current构造有限GeneratedHistory、准确target、Settlement与Receipt。

    位置：§6.4 定义6.6、定理6.7、注6.8

    Lean 模块 · 1

  10. core.C22无旧承担者的责任出生与付款§6.5

    任意old authoritative root、origin及该origin原occurrence上的Raw Env/Expr reader，生成数学source、编译器、完整patch、重构证书与living process：数学行由实际Step新生、旧账为同源余项；预算B−k，k<B真实付款，k=B局部结算，完成值=ev_ρ(e)，已付迹关系像e−const(ev e)∈ker。

    位置：§6.5 定义6.9、定理6.10

    Lean 模块 · 7

  11. core.C11总处置、残差扩充与因果审计§7.1–§7.3

    固定living root、完备复Hilbert H、已安装RecognitionAt：每步总处置六选一；选中RootedPassiveResidual生成同支撑自由残差coface与因果审计转移：旧行恒同、新行得权威、两端发生保留、整账与next认回。

    位置：§7.1–§7.3 命题7.1、定义7.2、命题7.3–7.5

    Lean 模块 · 4

  12. core.C25依赖步的源程序供给§7.3

    固定完备复Hilbert H、已安装RecognitionAt与exact visit：settle全处置；全生成与联合残差两支自产完整对齐构造子树T、OwnerFree已付状态与执行值、原材料及全部β(T)+1阶段材料；执行值=δ_{τ(T)}，计费=β(T)；整账与next认回。

    位置：§7.3 命题7.6

    Lean 模块 · 1

  13. core.C26原登记输入进入共享运行时§7.3

    任意old inquiry state、同root已安装Recognition及原SourceNativeRootInquiryInputAt：全生成与联合残差两支同时生成inputState/queryInput，reader直接读原Query.raw，实际Math/Frame/Shared runtime由此产生；独立消费者恢复整树、normal值与长度=原树预算的paid Trace；所有count的math whole/原material与所有offset的query/answer/next保持；其余分支返回原Feed。

    位置：§7.3 定理7.7(1)(2)

    Lean 模块 · 2

  14. core.C27原后继供应下一运行§7.3

    输入仅为原living root、exact visit、同root完整Recognition与原U7/calculus：每个continuing分支取原successor.next_eq生成下一actual visit并重读exposure/history；下一selected得到真实source runtime或准确Feed；前拍完整packet/residual同时保持；两拍整账与canonical next由同root认回；新低Source Inquiry/Frame只收source root/visit/calculus/raw reader。

    位置：§7.3 定理7.7(3)

    Lean 模块 · 4

  15. core.C13最小扩充、唯一因子化与首次写入§8.1–§8.3

    ∀RootedActualExpressibilityFailure：生成whole-network最小coface，旧support/identity/ledger构造性retract、旧事实与定理保留，新方向无旧原像；∀AdmissibleCofaceRevisionAt唯一FaithfulCofaceMorphism；typed revision的映射把新方向送到首次写入的新行；字段接地下旧新两行取得答案—后继；容量复合结合律。

    位置：§8.1–§8.3 定义8.1、命题8.2–8.3、定理8.4、定义8.5、定理8.6–8.7、命题8.8

    Lean 模块 · 2

  16. core.C4规范询问运行时§8.4

    任意SourceNativeInquiryEngineProcess与其激活律递归生成stateAt n；每拍answer、receipt、next来自engine.ask；同一激活态token等于canonical tick。

    位置：§8.4 运行时段

    Lean 模块 · 1

  17. core.C5两拍修订实例§8.4

    固定唯一query的非空实现：旧Bool支撑、预算2、空表达理论；coface新行预算0；Nat写入n↦n+1经精确接地，首次写入0→1，目标处编译到2；首拍公开cofaceAnswer，宏后继revised 2且不等于旧微后继；第二拍新根直接答PUnit.unit，后继3。

    位置：§8.4 命题8.9、表4、图5

    Lean 模块 · 1

  18. core.C6一次性接口无自主运行时§8.4

    任意RootInquiryStatePresentation：IsEmpty (SourceNativeInquiryRuntime state.oneShotProcess)。

    位置：§8.4 命题8.10

    Lean 模块 · 1

  19. core.C24实际动作生成下一问§8.5

    任意初始询问帧：残差请求e⊖e′的值=ev_ρ′(e)−ev_ρ′(e′)，旧值0，等于已付迹关系证书在增量下的效应；r(e⊖e′)=r(e)+r(e′)+2>0，首步为责任准入；递归帧构成现成询问运行时全部节点，擦除单射，查询纤维单点；只有执行步发射同债付款回执。

    位置：§8.5 定义8.11、定理8.12、例8.13、图6

    Lean 模块 · 6

  20. core.C28完整时间与原作用树由同一程序生成§9.1

    任意原root、完整temporal visit与已安装Recognition：finite/sealed cofinal/post-cofinal材料的Code保current与全部history，encode/decode互逆，Code.next认原actual successor；两history的continuation生成共同闭包、双completion map与准确零纤维、双evaluator及原normed action；一个有序tree programme的Outcome同时保原effect、完整temporal receipt树与common/evaluator/action，独立parser恢复全节点；target作用差分的观察/像两残差给真实逆判据，原词与exposure树经同发生保到literal下一source。

    位置：§9.1 定义9.1、定理9.2

    Lean 模块 · 15

  21. core.C29全作用者、全词与全未来恢复进入真实执行§9.2

    原source/target两树全部trace成员生成actor动作与H读口；完整allword Model的核=全部词联合读数核，whole carrier由原completion生成；每letter的E与point给有序effect history，总词残差=后续E运输各步残差之和；全部trace位置（含重复payload）生成node H/Gram；coarse×全部future H、integral/cofinal/coarse三面各自共同核为0，在实际像上真双逆并保每个词作用；paid AST与同一Trace消费。

    位置：§9.2 定理9.3

    Lean 模块 · 14

  22. core.C30已付查询自产下一内容与通用母准入§9.3

    同actual query的paid old＋effect生成born下一内容，原history(stage)经源作用读出history(stage+2)；对任意原Frame、source-owned Programme与独立LowVar，actual query完整State/Trace/同发生owner及下一query环境自产ResidualRequest、正syntax预算firstStep、同root/visit的debtAdmission；原whole首目的地、全部旧projection、literal next、runtime current/全offset next与no-refill/Noetherian直接生成；同queryFrame的原生shift/full packet回同一母准入。

    位置：§9.3 定义9.4、定理9.5

    Lean 模块 · 13

  23. core.C31typed库存越过母准入并实际再消费§9.3

    任意原Frame/source-owned Programme/独立LowVar：同supplied occurrence的physical与low Raw/paid Result/完整Trace保原类型；逐变量binding保全部Expr/relation求值；母target的inherited typed outcome消元取得stock；完整written、逐发生Fin坐标及mathNext/nextBorn两支自产下一库存query；全词cofinal、原native packet与完整reverse由同actual query/whole/literal next消费。

    位置：§9.3 定理9.6

    Lean 模块 · 8

  24. core.C32同源词—State作用保完整有偿历史§9.3

    同原runtime/source自产操作formal word×完整sealed State的ℤ双线性原值pair；binding与sourceAction生成全carrier covariance、canonical coimage action与任意次迭代；每个prefix的原AST执行、完整Trace与exposure保留；batch原坐标有偿执行，callFrame/raw/query/receipt自产有限snapshot并恢复原迭代query与完整epoch Past，下一request/whole/next直接消费。

    位置：§9.3 定理9.7

    Lean 模块 · 8

  25. core.C33默认主运行执行源自产请求§9.4

    原Joint及Branch的实际root/reader产生初frame与seed，programme.reader直接执行同supplied occurrence的occurrenceRaw；Shared actual query/input/answer/next由同seed/initial/count生成；新paid exposure、原inverse与Past交下一库存；Branch的core与relation两AST形成Fin2 batch，源action、paid与完整substituted Trace进入初stock。

    位置：§9.4 定理9.8(1)

    Lean 模块 · 7

  26. core.C34原新actor与child操作进入默认Born§9.4

    同actual core自产Fresh.Complete old/next actor与canonical packet，Stage0 seed事件生成原word/completion point；原Plan及全exposure节点作用生成child AST/paid State/Trace；一次typed主AST实际执行原query加已选old/next child；source-dependent decoder读当次environment的原binding，把完整child作用送true Born；default live runtime逐stage消费方程、inverse、付款、whole与next。

    位置：§9.4 定理9.8(2)(3)

    Lean 模块 · 9