H0mework

First-release paper · 2026-10-07

The State Is Not the History, the Source Is

Identity, Responsibility, and Minimal Revision in Processes

状态不是历史，源才是：过程同一性、责任承接与最小修订

Paper PDFSupplementarXiv versionDOI 10.5281/zenodo.23210084
  • 26claims
  • 127Lean modules
  • 1589declarations
  • ✓ all kernel checks passed
00κ
The tape: prog κ(T), the sourcePegboards: T on the left, read(prog T) on the right; peg height is the root label a, b, cDial: the reading ev = fold κ(T)Theorem 3.9. Each tree's whole-tree program is punched row by row: one row per syntax node, a cost hole on every variable and bilinear node. The first head totals the cost holes, r(prog T) = β(T) = 2, 5, 8, 11, 14, fixed by the tree's shape alone. With κ ≡ 0 the dial reads 0 for every tree; the second head never evaluates, its pins skip the map channel, and it still rebuilds each tree exactly. Flip κ to count nodes: only the map channel and the dial change.

Abstract

A question leaves a demand for a process to discharge; even when several readings agree, an answer must still say which run it belongs to. Through four levels of identity—same reading, same source object, same occurrence, same obligation—we construct a positive chain that the source walks by itself: the original occurrence hands over a complete source program, the program is actually executed and can be read back independently, the execution gives birth to its own responsibility row and pays it step by step, and after settlement the actual action asks the next question.

Read the full abstract

The first link separates readings from sources. Any rooted tree and any constructor function generate a whole-tree program: the execution trace has exactly the budget generated by the tree’s syntax, and a syntax-only parser recovers the whole tree from the program; even when the constructor is constantly zero and every tree executes to the same value, the program still keeps the whole tree injectively. On top of this, the relations generated by derivations and module laws are exactly the evaluation kernel; two source words are the same in history iff at every tick their (old value, effect) difference is explained by that tick’s relations; and the evolution equation covers every element of the completion carrier. When implementations change, the common occurrence generates the unique comparison.

The second link lets responsibility be born from the source. A complete environment and expression registered at the original occurrence generate a new mathematical responsibility row without any prior bearer: its budget is the number of remaining primitive computations, every actual execution step is a strict payment, local settlement is reached where the budget runs out, and the completed value equals the evaluation of the original expression; the paid trace is at once a relation receipt, and the whole old ledger is kept as a same-source remainder. For general responsibilities, given a master law covering every same-debt current, genuine payments likewise generate finite settlement histories and terminal receipts.

The third link lets an answer ask the next question. After settlement, the actual action puts the paid relation back into the current actual environment: the value of the new request is exactly the effect of the original word under this update, its budget is strictly positive, and its first step is the birth of a new responsibility; the existing inquiry runtime runs through these recursive frames tick by tick, with no external table of future requests. When the old theory can neither express nor lawfully realize a demand, the rooted failure generates a minimal extension: on the ledger, incidence and claim coordinates, every admissible extension receives it through a unique faithful map; every typed revision sends this direction into the new root’s first write, and in a fixed two-tick instance the second tick is answered directly by the same new root.

The next question does not set out empty-handed. The same source program folds the complete time of this visit while it executes the effect, and keeps both histories together with an inverse criterion for the action difference; the read-outs of all actors jointly recover the all-word model; the paid query of an arbitrary source program generates a new obligation admission at the same root and visit, and physical and low-level inventories of two types cross the admission and are read back item by item; the default run itself executes this source-generated request, together with its old and next subtrees, paying node by node. A question therefore does not merely wait for an answer: its execution, its settlement and its failure all ask the next question. The theorems and constructions are formalized in Lean 4; complete written proofs are given in the text and the Supplement, and the scope of the formalization is given in Appendix D.

Keywords: process identity; incremental computation; source-program execution; semantic relation kernel; faithful realization; responsibility ledger; minimal revision; dependent types; formalization

Claims and proofs

Every claim is registered in the claim map. Open one to see its statement, where it appears in the paper, and the Lean modules and replay programs that prove it. The English statements are translated from the registered Chinese.

  1. core.C23Whole-tree programs: execution, charging and independent read-backFigure§3.4

    For any Root, Carrier and any atOccurrence : Root → List Carrier → Carrier: the whole tree generates a program whose execution value is the native basis element of the fold; the budget is generated by the tree syntax β and the execution trace has length β; a syntax-only parser recovers the whole tree; when atOccurrence is constantly zero the program is still injective. Installed in an inquiry, value, provenance and cost are read out together.

    Location: §3.4 Proposition 3.7, Definition 3.8, Theorem 3.9; §6.5 Proposition 6.11; §10.1

    Lean modules · 7

  2. core.C3Successor and history of a fixed process§2.1

    For any fixed-law process: stateAt is an injective representation of the complete living current; successor recovers the root compilation result exactly and preserves the law surface; equal currents have equal successors; any fuel generates a history.

    Location: §2.1 Definition 2.1, Proposition 2.2

    Lean modules · 2

  3. core.C9Free carriers of native states and arbitrary binary operations§2.2–§2.4

    For every fixed SourceNativeLivingRootProcess: δ : State → Free ℤ (State) is injective and Aδ(s) = δ(successor s); every original read extends uniquely to a linear map that commutes with the action; every f : X → Y → Z generates a biadditive lift, mixed effects and normalize; the Field's nextWitness preserves the original tick.next.

    Location: §2.2–§2.4

    Lean modules · 3

  4. core.C7Effects, mixed terms and derivations in Type§3.1–§3.3

    For any sorts, additive commutative groups and variable environment: the recursive effect and the ordered mixedTerms of a finite Expr give eval(old+inc) = eval(old) + effect, with bilinear nodes keeping the left, right and joint terms; normalize generates, in Type, Derivation env e (const (eval e env)).

    Location: §3.1–§3.3

    Lean modules · 3

  5. core.C8Relation kernel, completion carrier and elementwise evolution§4

    For any commutative ring R, R-modules and a fixed environment: range(relationMap) = ker(evaluation). For a fixed runtime, the actual readMaterial and an additive environment projection: two words have the same image in the completion iff at every stage their (old, effect) difference lies in the relation range generated at that stage; the successor covers every element of the completion; in the Fock realization the Fibre witness of the original word extends along the generated successor.

    Location: §4 Theorems 4.4, 4.6, 4.7, Proposition 4.8

    Lean modules · 7

  6. core.C10Faithful realization and the unique comparison§5

    For a fixed SourceNativeLivingRootClosure: the canonical Process has a FaithfulRealization; every event of every faithful process recovers the canonical occurrence and all installed projections, with event = emitted; any two faithful realizations generate, through the common occurrence, a two-way representation compatible with the whole compilation; any candidate current-by-current event map equals the generated comparison pointwise.

    Location: §5

    Lean modules · 2

  7. core.C1The three lifecycle laws§6.1

    For any vocabulary V, NativeResponsibilityProcess P, and legal edge and slot: fresh allocation ⇒ admitted; newly live ⇒ admitted or reopened; live → nonlive ⇒ obligationTerminal; Run.history_eq preserves the ordered history.

    Location: §6.1 Proposition 6.1

    Lean modules · 1

  8. core.C12Debt activation and event-by-event whole-ledger compilation§6.2–§6.3

    For every world N and DebtActivationLaw: the extended world has support base × Option DebtState; the inactive fibre recovers all old rows and the active fibre recovers the old rows plus a unique law-owned debt row. For a fixed lower root and current, OccurrenceIndexedSourceAt generates LedgerWriteEvolution, LedgerTerminalEvolution or a same-row U7 audit. In the target-6 instance, 2+4 → 3+3, the action-debt payment 1 → 0 and the target's terminal ledger are read separately.

    Location: §6.2–§6.3

    Lean modules · 3

  9. core.C2The same-debt master law generates finite settlement§6.4

    For a fixed process and origin debt: the non-increasing–strictly-decreasing–non-increasing payment macro-composite strictly decreases; the continuation relation is well-founded and irreflexive, and a zero budget admits no payment. Given a Noetherian master emit covering every same-debt current, each current constructs a finite GeneratedHistory, its exact target, a Settlement and a Receipt.

    Location: §6.4 Definition 6.6, Theorem 6.7, Remark 6.8

    Lean modules · 1

  10. core.C22A responsibility born without a prior bearer, and its payment§6.5

    For any old authoritative root, origin, and Raw Env/Expr reader on that origin's original occurrence: it generates a mathematical source, compiler, complete patch, reconstruction certificate and living process. The mathematical row is newly born from actual Steps and the old ledger is a same-source remainder; the budget is B − k, with a genuine payment for k < B and local settlement at k = B; the completed value is ev_ρ(e), and the relation image of the paid trace is e − const(ev e) ∈ ker.

    Location: §6.5 Definition 6.9, Theorem 6.10

    Lean modules · 7

  11. core.C11Master disposition, residual extension and causal audit§7.1–§7.3

    For a fixed living root, a complete complex Hilbert space H and an installed RecognitionAt: every step's master disposition selects exactly one of six cases; selecting RootedPassiveResidual generates a free residual coface on the same support and a causal-audit transfer: old rows stay identical, new rows gain authority, the occurrences at both ends are kept, and the whole ledger and next are recovered.

    Location: §7.1–§7.3

    Lean modules · 4

  12. core.C25Source-program feed of a dependent step§7.3

    For a fixed complete complex Hilbert space H, an installed RecognitionAt and an exact visit: settle is a total disposition; both the full-generation and the joint-residual branches produce by themselves the complete aligned constructor subtree T, an OwnerFree paid state and execution value, the original material and all β(T)+1 stage materials; execution value = δ_{τ(T)} and charge = β(T); the whole ledger and next are recovered.

    Location: §7.3 Proposition 7.6

    Lean modules · 1

  13. core.C26The originally registered input enters the shared runtime§7.3

    For any old inquiry state, an installed Recognition at the same root and the original SourceNativeRootInquiryInputAt: both the full-generation and the joint-residual branches generate inputState/queryInput, the reader reads the original Query.raw directly, and the actual Math/Frame/Shared runtime arises from it; an independent consumer recovers the whole tree, the normal value and a paid Trace whose length equals the original tree budget; for every count the math whole and original material, and for every offset the query/answer/next, are kept; the remaining branches return the original Feed.

    Location: §7.3 Theorem 7.7(1)(2)

    Lean modules · 2

  14. core.C27The original successor supplies the next run§7.3

    The only inputs are the original living root, an exact visit, a complete Recognition at the same root and the original U7/calculus: every continuing branch takes the original successor.next_eq to generate the next actual visit and rereads exposure/history; the next selected branch obtains a genuine source runtime or the exact Feed; the previous tick's complete packet/residual is kept as well; the two-tick whole ledger and canonical next are recovered by the same root; the new lower Source Inquiry/Frame receives only the source root, visit, calculus and raw reader.

    Location: §7.3 Theorem 7.7(3)

    Lean modules · 4

  15. core.C13Minimal extension, unique factorization and the first write§8.1–§8.3

    For every RootedActualExpressibilityFailure: it generates the minimal whole-network coface; the old support, identity and ledger retract constructively, old facts and theorems are kept, and the new direction has no old preimage. Every AdmissibleCofaceRevisionAt has a unique FaithfulCofaceMorphism; the map of a typed revision sends the new direction to the new row of its first write; under field grounding the old and new rows obtain their answer and successor; capacity composition is associative.

    Location: §8.1–§8.3

    Lean modules · 2

  16. core.C4The canonical inquiry runtime§8.4

    Any SourceNativeInquiryEngineProcess and its activation law recursively generate stateAt n; each tick's answer, receipt and next come from engine.ask; the token of the same activation state equals the canonical tick.

    Location: §8.4 runtime paragraph

    Lean modules · 1

  17. core.C5The two-tick revision instance§8.4

    A non-empty realization of a fixed unique query: old Bool support, budget 2, an empty expression theory; the new coface row has budget 0; the Nat write n ↦ n+1 is grounded exactly, the first write is 0 → 1 and compiles to 2 at the target; the first tick publishes cofaceAnswer, the macro successor is revised 2 and differs from the old micro successor; on the second tick the new root answers PUnit.unit directly, with successor 3.

    Location: §8.4 Proposition 8.9, Table 4, Figure 5

    Lean modules · 1

  18. core.C6A one-shot interface has no autonomous runtime§8.4

    For any RootInquiryStatePresentation: IsEmpty (SourceNativeInquiryRuntime state.oneShotProcess).

    Location: §8.4 Proposition 8.10

    Lean modules · 1

  19. core.C24The actual action generates the next question§8.5

    For any initial inquiry frame: the residual request e ⊖ e′ has value ev_ρ′(e) − ev_ρ′(e′) and old value 0, equal to the effect of the paid trace's relation certificate under the increment; r(e ⊖ e′) = r(e) + r(e′) + 2 > 0 and the first step is a responsibility admission; the recursive frames form every node of the existing inquiry runtime, erasure is injective and the query fibre is a singleton; only execution steps emit same-debt payment receipts.

    Location: §8.5 Definition 8.11, Theorem 8.12, Example 8.13, Figure 6

    Lean modules · 6

  20. core.C28Complete time and the original action tree generated by one program§9.1

    For any original root, complete temporal visit and installed Recognition: the Code of finite/sealed cofinal/post-cofinal material keeps the current and the whole history, encode/decode are mutually inverse, and Code.next recovers the original actual successor; the continuations of the two histories generate a common closure, two completion maps with the exact zero fibre, two evaluators and the original normed action; the Outcome of one ordered tree programme keeps the original effect, the complete temporal receipt tree and common/evaluator/action at once, and an independent parser recovers every node; the observation and image residuals of the target action difference give a genuine inverse criterion, and the original word and exposure tree are carried through the same occurrence to the literal next source.

    Location: §9.1 Definition 9.1, Theorem 9.2

    Lean modules · 15

  21. core.C29All actors, all words and all futures recovered into actual execution§9.2

    All trace members of the original source and target trees generate actor actions and H read-outs; the kernel of the complete all-word Model equals the kernel of the joint readout of all words, and the whole carrier is generated by the original completion; each letter's E and point give an ordered effect history, and the total word residual is the sum of the step residuals transported by the subsequent E's; every trace position (repeated payloads included) generates node H/Gram; coarse × all future H, and the integral, cofinal and coarse faces, each have common kernel 0, with a genuine two-sided inverse on the actual image that keeps every word action; the paid AST and the same Trace are consumed.

    Location: §9.2 Theorem 9.3

    Lean modules · 14

  22. core.C30A paid query produces its next content, and the universal mother admission§9.3

    The paid old value plus effect of the same actual query generates the born next content, and the original history(stage) is read out as history(stage+2) through the source action. For any original Frame, source-owned Programme and independent LowVar: the actual query's complete State/Trace, same-occurrence owner and next query environment produce by themselves a ResidualRequest, a firstStep with positive syntax budget and a debtAdmission at the same root and visit; the original whole first destination, all old projections, the literal next, the runtime current/next at every offset and no-refill/Noetherian are generated directly; the native shift and full packet of the same queryFrame return to the same mother admission.

    Location: §9.3 Definition 9.4, Theorem 9.5

    Lean modules · 13

  23. core.C31Typed inventory crosses the mother admission and is actually consumed again§9.3

    For any original Frame, source-owned Programme and independent LowVar: the physical and low Raw, paid Result and complete Trace of the same supplied occurrence keep their original types; per-variable binding keeps every Expr/relation evaluation; eliminating the inherited typed outcome of the mother target yields the stock; the complete written record, the per-occurrence Fin coordinates and both the mathNext and nextBorn branches produce the next inventory query by themselves; the all-word cofinal, the original native packet and the complete reverse are consumed by the same actual query, whole and literal next.

    Location: §9.3 Theorem 9.6

    Lean modules · 8

  24. core.C32The same-source word–State action keeps the complete paid history§9.3

    The same original runtime/source produces by itself the ℤ-bilinear original-value pairing of formal operation words × complete sealed States; binding and sourceAction generate whole-carrier covariance, the canonical coimage action and iterates of any order; every prefix keeps its original AST execution, complete Trace and exposure; batches execute with payment at original coordinates, and callFrame/raw/query/receipt produce a finite snapshot by themselves that recovers the original iterated query and the complete epoch Past, consumed directly by the next request, whole and next.

    Location: §9.3 Theorem 9.7

    Lean modules · 8

  25. core.C33The default main run executes the source-generated request§9.4

    The actual root/reader of the original Joint and Branch produces the initial frame and seed, and programme.reader directly executes the occurrenceRaw of the same supplied occurrence; the Shared actual query/input/answer/next are generated by the same seed/initial/count; the new paid exposure, the original inverse and Past pass to the next inventory; the core and relation ASTs of the Branch form a Fin 2 batch, and the source action, payment and complete substituted Trace enter the initial stock.

    Location: §9.4 Theorem 9.8(1)

    Lean modules · 7

  26. core.C34Original and new actor and child operations enter the default Born§9.4

    The same actual core produces by itself the Fresh.Complete old/next actor and the canonical packet; the Stage 0 seed event generates the original word and completion point; the original Plan and the actions of all exposure nodes generate the child AST, paid State and Trace; one typed main AST actually executes the original query together with the selected old/next child; a source-dependent decoder reads the original binding of the current environment and sends the complete child action to the true Born; the default live runtime consumes, stage by stage, the equations, inverse, payment, whole and next.

    Location: §9.4 Theorem 9.8(2)(3)

    Lean modules · 9