sprawling-kernel 0.0.12

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.
-- Copyright (c) 2026 2youg1 and the sprawling contributors

/-!
# kernel::share

规定 `kernel::share`（`crates/kernel/src/share.rs`）：守恒的份额。本文件是 `crates/kernel/Spec.lean` 的一个分部；下面每一节保留它在 kernel 规格里的标签 §8-n，别处引作 `crates/kernel/Spec.lean §8-n`。
-/

/-!
### 8-32 kernel::share（形状 2 value）

```rust
pub struct Share(/* u64 私有：十亿分之一 */);
pub const WHOLE_PPB: u64 = 1_000_000_000;
impl Share {
    pub const WHOLE: Share;                 // 唯一原点
    pub const NONE:  Share;                 // 加不出来，故可公开
    pub fn ppb(self) -> u64;
    pub fn split(self, weights: &[u32]) -> Result<Vec<Share>, AxError>;   // 取走自己，分出恰好等于自己的诸份
}
pub fn gather(parts: &[Share]) -> Share;    // 自由函数，不是 Add
```

- **守恒不是被检查的规则，而是类型唯一能表达的事。** 份额只有两种来路：整份计划，或者**分掉另一份得到的一片**。`split` 按值取走输入，于是「凭空多出一份」拼不出来（trybuild `forge_share`）。没有构造器、没有算术、没有 `Deserialize`——**从文件里读回来的数字必须先从整体里分出来才能成为份额**，这正是 `PlanTree::build` 每次自根重分的理由：守恒是重新推导出来的，不是被信任的。
- **这样就解掉了自评偏差**：一个 Agent 怎么切自己那一支都行，但它切不出比父节点更多的份。**封顶取代仲裁**，也就不需要「权重从哪来」的第二权威。
- **十亿分之一而不是分数**：两份份额在任何机器上以同样方式比较与相加，反复细分不会把分母撑大，判定路径上没有浮点（ARCHITECTURE §10 规则 6）。整除余数按**先来先得**发给靠前的几份——这是一条规则而不是一次舍入，于是同一份计划在任何机器上分法相同。
- **`gather` 是自由函数而不是 `Add`**：它是「一根枝的叶子加起来是多少」这件事，不是谁都可以随手做的算术。混了两份计划的调用方会得到饱和在整份上的结果，那是诚实答案。
-/

/-! D25 一份空计划的根份额归这栋楼的 Mayor，`plan` 因此有 `add`

**决定**：计划的根就是计划本身，不是表里的一行：`PlanTree::build` 的 `divide` 把 `Share::WHOLE` 分给顶层各行，空计划的根持有整份而没有一行可分。根的持有者是这栋楼的 Mayor（`hall/mayor`）；`plan` 工具多一个动作 `add`，带 `parts`（与 `split` 同一个参数），每一份在根下成为一个顶层行，编号接在最后一个顶层行之后（`kernel::spine::append_top_level`），新行的份额照旧由 `PlanTree::build` 自根重分。在一个节点下加活就是 `split`：只有握着那一行的 run 能分它（collab D6），所以 `add` 不点名节点。`Kernel.Share.Root` 证明：从空计划出发，任何一串 add／split 之后叶子之和恒为整份。只有根的持有者能 `add`，别的 run 得到的拒词叫它认领一行再 `split`，或给 `hall/mayor` 发信。没有新的事件种类：加出的行不写 `roadmap_*` 行（`collab::ClaimEffect::Added` 的 `kind` 为 `None`），随计划文件的写盘入账。

**理由**：份额只有两种来路——整份计划或分掉另一份（§8-32）——而整份从来没有交给任何一方，所以空的 `Roadmap.md` 写不进第一行。根份额交给这栋楼的 Mayor，理由是 Mayor 持有这栋楼的计划文件，而派活的 JOB 是从计划里分出来的一支，不能先于计划存在。

**被否**：①根份额归派活的 JOB：空计划里还没有可派的活；②`add` 不经份额、直接写行：守恒就有了一条绕过 `split` 的路。

**重开参数**：User 改定根份额的持有者时，只改「谁持根」这一条判定（`plan` 的 `add` 授权），份额的算术不动。
-/

namespace Kernel.Share.Root

/-- 计划的一片叶子：持有者与它持有的十亿分之一数。持有者的身份在这条性质里只需能比较相等。 -/
structure Leaf (Holder : Type) where
  holder : Holder
  ppb : Nat

/-- 一份计划此刻的叶子，按行序。 -/
abbrev Leaves (Holder : Type) := List (Leaf Holder)

/-- 叶子持有的份额之和。 -/
def held {Holder : Type} (leaves : Leaves Holder) : Nat :=
  (leaves.map Leaf.ppb).sum

/-- 一份空计划（D25）：一个根，持有整份，持有者是这栋楼的 Mayor。 -/
def empty {Holder : Type} (whole : Nat) (mayor : Holder) : Leaves Holder :=
  [⟨mayor, whole⟩]

/-- 一步改动：`plan add` 与 `split` 都是把一片叶子 `x` 换成若干片，新片之和恰为 `x`——
`Share::split` 取走自己、分出恰好等于自己的诸份（§8-32），`add` 是在 `x` 下加子节点后自 `x` 重分。 -/
inductive Step {Holder : Type} : Leaves Holder → Leaves Holder → Prop where
  | divide (pre post parts : Leaves Holder) (x : Leaf Holder) (exact : held parts = x.ppb) :
      Step (pre ++ x :: post) (pre ++ parts ++ post)

/-- 若干步改动组成的一条轨迹。 -/
inductive Trace {Holder : Type} : Leaves Holder → Leaves Holder → Prop where
  | stay (s : Leaves Holder) : Trace s s
  | step {s t u : Leaves Holder} : Step s t → Trace t u → Trace s u

theorem held_append {Holder : Type} (a b : Leaves Holder) : held (a ++ b) = held a + held b := by
  simp [held, List.map_append, List.sum_append]

theorem held_cons {Holder : Type} (x : Leaf Holder) (rest : Leaves Holder) :
    held (x :: rest) = x.ppb + held rest := by
  simp [held]

/-- 一步改动不改变叶子之和。 -/
theorem step_conserves {Holder : Type} {s t : Leaves Holder} (move : Step s t) : held t = held s := by
  cases move with
  | divide pre post parts x exact =>
    rw [held_append, held_append, held_append, held_cons, exact, Nat.add_assoc]

/-- 从空计划出发的任何一条 add／split 轨迹上，叶子之和恒为整份。 -/
theorem every_trace_from_the_empty_plan_holds_the_whole {Holder : Type} (whole : Nat)
    (mayor : Holder) {s : Leaves Holder} (trace : Trace (empty whole mayor) s) : held s = whole := by
  have conserved : ∀ {a b : Leaves Holder}, Trace a b → held b = held a := by
    intro a b path
    induction path with
    | stay => rfl
    | step move _ rest => rw [rest, step_conserves move]
  rw [conserved trace]
  simp [held, empty]

/-- 空计划的根恰有一个持有者，它是这栋楼的 Mayor，持有整份。 -/
theorem the_empty_plan_has_one_root_held_by_the_mayor {Holder : Type} (whole : Nat)
    (mayor : Holder) : empty whole mayor = [⟨mayor, whole⟩] ∧
      (empty whole mayor).map Leaf.holder = [mayor] := by
  exact ⟨rfl, rfl⟩

end Kernel.Share.Root