leanified/CoreReader/Engineering/Values.lean

返回主张速览 · 声明与证明

哲学 0.2.1 · 已考虑的 Core 0.1.2。阅读视图来自本仓库公开的目标清单、读者稿和 Lean 文件；页面布局不改变其中的判定。

展开 Lean 与逐行解读 · 201 行

Lean逐行解读

L1import CoreReader.Adopted

导入 CoreReader.Adopted，使其声明及传递依赖可用；此行不新增命题。

L2import CoreReader.Engineering.Domain

导入 CoreReader.Engineering.Domain，使其声明及传递依赖可用；此行不新增命题。

L4namespace CoreReader.Engineering

开启 CoreReader.Engineering 命名空间，后续声明归入其中。

L6open CoreReader.Logic CoreReader.Evidence CoreReader.Adopted

允许不带完整限定名引用 CoreReader.Logic CoreReader.Evidence CoreReader.Adopted 中的声明；不改变其含义。

L8inductive CoreCommitment | generation | consistency | reflexivity | grounds | choice

定义生成、一致性、反身性、依据与选择五个 Core 承诺标识。

L9  deriving DecidableEq, Repr

自动派生 DecidableEq, Repr：提供这些构造子的可判定相等与可打印表示。

L11def coreCommitments : List CoreCommitment :=

coreCommitments 是全部已表示承诺标识的有限列表。

L12  [.generation, .consistency, .reflexivity, .grounds, .choice]

按显示顺序各列出五个构造子一次。

L14/- Initial adoption is explicit. The following reasons neither infer adoption

注释指出采纳是明确起始选择；理由不推导采纳本身。

L15from facts nor claim that every alternative value position is untenable. -/

注释既不从事实推导采纳，也不声称所有替代价值均不可成立。

L16def coreAdopted (_ : CoreCommitment) : Bool := true

每个承诺都被明确标记为已采纳；此布尔选择不是从事实前提推导的。

L18inductive AdoptionReason

AdoptionReason 是具体理由数据的类型族，本身不是证明。

L19  | plannedChange (release : Nat) (direction : Change)

plannedChange 记录自然数版本与 Change 方向。

L20  | incompatibleOrders (input : List Nat)

incompatibleOrders 保存用于比较输出顺序的实际输入列表。

L21  | ownMethodCounterexample (items size : Nat)

ownMethodCounterexample 保存项目数与运行规模。

L22  | unsupportedScope (items observedSize extendedSize : Nat)

unsupportedScope 对固定项目数区分观测规模与扩展规模。

L23  | statusBudgetContrast (statusSelected : Candidate) (capacity : Nat)

statusBudgetContrast 记录按地位选出的候选项与自然数容量。

L24  deriving DecidableEq, Repr

自动派生 DecidableEq, Repr：提供这些构造子的可判定相等与可打印表示。

L26def reasonFor : CoreCommitment → AdoptionReason

为每个 Core 承诺分配一个具体理由值。

L27  | .generation => .plannedChange 2 .designRevision

生成为计划版本 2 与 designRevision。

L28  | .consistency => .incompatibleOrders [2, 1, 2]

一致性使用顺序敏感输入 [2, 1, 2]。

L29  | .reflexivity => .ownMethodCounterexample 21 5

反身性使用 21 项与运行规模 5。

L30  | .grounds => .unsupportedScope 21 10 5

依据比较 21 项在规模 10 的观测与规模 5 的扩展。

L31  | .choice => .statusBudgetContrast .maximal 12

选择将 maximal 与理解容量 12 比较。

L33/- Each factual reason has contents specific to the principle's purpose. The

注释介绍针对各原则目的的事实理由。

L34context is the very continuing activity and its current requirements/grounds.

注释将理由语境固定为此持续活动及实际需求、证据。

L35Matching a constructor alone is insufficient: the represented facts must hold. -/

注释要求实际理由内容成立，不能仅匹配构造子名称。

L36abbrev ReasonRelevant : CoreCommitment → AdoptionReason → Candidate → Prop

ReasonRelevant 是原则、结构化理由及所选设计上的命题，检查实际理由内容。

L37  | .generation, .plannedChange release direction, _ =>

对生成及计划改变理由，此分支不依赖所选设计。

L38      DirectionGround.plan release [direction, .migration] ∈ currentContinuing.evidence ∧

包含该方向与迁移的精确版本计划必须出现在当前证据中。

L39      credible currentContinuing.evidence direction ∧ Continuing currentContinuing.activity

该方向必须可信，且当前活动必须持续。

L40  | .consistency, .incompatibleOrders input, _ =>

对一致性，使用不兼容顺序理由中携带的输入。

L41      currentContinuing.required.orderRequired = true ∧

实际当前需求必须要求保持顺序。

L42      orderedUnique input ≠ sortedUnique input

保序去重与排序去重必须在此输入上不同。

L43  | .reflexivity, .ownMethodCounterexample items size, _ =>

对反身性，使用理由中的项目数与受质疑规模。

L44      staticBatch items 10 = liveBatch items 10 ∧ staticBatch items size ≠ liveBatch items size

要求旧规模 10 一致，而受质疑规模不一致。

L45  | .grounds, .unsupportedScope items observedSize extendedSize, _ =>

对依据，比较理由中的观测规模与扩展规模。

L46      staticBatch items observedSize = liveBatch items observedSize ∧

静态与实时预测必须在观测规模一致。

L47      staticBatch items extendedSize ≠ liveBatch items extendedSize

它们必须在提议的扩展规模不一致。

L48  | .choice, .statusBudgetContrast candidate capacity, selected =>

对选择，区分受比较的候选项与实际所选设计。

L49      capacity = currentContinuing.limits.capacity .understanding ∧

所述容量必须等于当前理解容量。

L50      capacity < abstractionComplexity candidate ∧ abstractionComplexity selected ≤ capacity

受比较候选项超出容量，而实际选择不超出容量。

L51  | _, _, _ => False

任何不匹配的原则、理由构造子组合均返回 False。

L53abbrev valueScope (selected : Candidate) : Prop := abstractionComplexity selected ≤ 3

价值程序披露的范围为抽象复杂度不超过 3 的设计。

L55/- A small operational experiment explains each adopted safeguard's purpose.

注释介绍解释每项保障目的的小型操作实验。

L56These consequences are limited to the stated experiment, not a total value score.

注释将后果限于该实验，排除综合价值评分。

L57The disabled branch supplies a real contrast for this application policy. -/

注释指出禁用分支是此应用政策内的实际对照。

L58def safeguardExperiment (principle : CoreCommitment) (enabled : Bool)

safeguardExperiment 改变指定保障的启用布尔值。

L59    (selected : Candidate) : Bool :=

它还接收实际所选设计，并返回操作性布尔结果。

L60  match principle with

按原则选择实验；这不是综合价值度量。

L61  | .generation =>

生成分支衡量可信计划改变是否可用。

L62      let allowed : List Change := if enabled then [.designRevision, .migration] else []

启用时允许 designRevision 与 migration，禁用时允许列表为空。

L63      allowed.contains .designRevision && decide (credible currentContinuing.evidence .designRevision)

仅当 designRevision 被允许且当前可信时通过。

L64  | .consistency =>

一致性分支衡量是否拒绝不兼容的同时要求。

L65      let firstDemand := orderedUnique [2, 1, 2]

以保序去重计算第一个要求。

L66      let secondDemand := sortedUnique [2, 1, 2]

以排序去重在同一输入上计算第二个要求。

L67      let permitsBoth := if enabled then firstDemand == secondDemand else true

启用检查仅在两个要求相等时同时允许；禁用则无条件同时允许。

L68      !permitsBoth

拒绝同时允许时，此实验成功。

L69  | .reflexivity =>

反身性分支对实际批次数预测进行自身测试。

L70      let selfTests := if enabled then [(21, 10), (21, 5)] else [(21, 10)]

启用时包含旧规模及受质疑规模；禁用时仅保留旧规模。

L71      selfTests.any (fun point => staticBatch point.1 point.2 != liveBatch point.1 point.2)

某个已列案例的静态与实时预测不等时通过。

L72  | .grounds =>

依据分支测试获许可的输入范围。

L73      let licensed := if enabled then [10] else [10, 5]

启用时仅许可规模 10；禁用时把许可扩展为 10 与 5。

L74      licensed.all (fun size => staticBatch 21 size == liveBatch 21 size)

固定项目数 21，要求每个获许可规模的预测相等。

L75  | .choice =>

选择分支衡量是否符合理解容量。

L76      let selectedByRule := if enabled then selected else .maximal

启用时选传入设计；禁用保障时选 maximal。

L77      decide (abstractionComplexity selectedByRule ≤ currentContinuing.limits.capacity .understanding)

判定规则实际选出的设计是否符合当前理解容量。

L79def criticismFor : CoreCommitment → String

为每个原则分配可修订性、批评回应字符串。

L80  | .generation => "Reconsider this reason if the committed change or continuing maintenance ends."

生成回应把已承诺改变或持续维护的终止列为重新考虑条件。

L81  | .consistency => "Reconsider the comparison if the parties deliberately revise the observable order contract."

一致性回应允许在有意修订顺序合约后重新考虑比较。

L82  | .reflexivity => "This counterexample concerns the stated batch rule; it does not validate all self-assessment."

反身性回应把反例限于此批处理规则，不推广到全部自评估。

L83  | .grounds => "A new input condition requires its own support; success at size ten does not cover size five."

依据回应拒绝在没有各自支持时把规模 10 的成功扩展到规模 5。

L84  | .choice => "If objectives or budgets change, compare the actual alternatives and reasons again."

选择回应要求在目标或预算变化时重新比较。

L86def governancePosition (principle : CoreCommitment) : ValuePosition Candidate where

对一个原则，构造 Candidate 上的 ValuePosition，明确采纳及有界支持理由。

L87  Position := Bool

价值立场的备选项为启用、禁用布尔状态。

L88  Outcome := Bool

实验结果类型为 Bool。

L89  adopted := true

明确采纳启用的价值立场。

L90  selected _ := coreAdopted principle

对每个设计，所选立场为该原则的采纳标记。

L91  outcome selected enabled := safeguardExperiment principle enabled selected

结果以设计与启用立场运行同一原则的实验。

L92  objective result := result = true

目标是实验成功，以 true 表示。

L93  constraints selected _ := valueScope selected

无论布尔立场如何，约束均要求设计满足 valueScope。

L94  starting := singleton valueScope

起始理论仅含 valueScope 命题。

L95  reasons := [fun selected _ => ReasonRelevant principle (reasonFor principle) selected]

唯一理由要求对同一原则、所选设计具有实际相关性。

L96  limits := valueScope

应用限制同样为 valueScope。

L97  relevantCriticism _ := True

所有 Candidate 值均视为相关批评；未编码更窄过滤。

L98  response _ := some (criticismFor principle)

每项批评均得到该原则的固定回应字符串。

L100theorem adoptionReasonRelevant (principle : CoreCommitment) (selected : Candidate)

为范围内的每个原则与所选设计证明理由相关性。

L101    (scope : valueScope selected) : ReasonRelevant principle (reasonFor principle) selected := by

前提把所选复杂度限制到 3；结论采用其精确 reasonFor 值。

L102  cases principle

拆分五种原则构造子。

L103  · dsimp only [ReasonRelevant, reasonFor]; decide

对生成，展开理由内容并计算计划成员资格、可信性与持续性。

L104  · dsimp only [ReasonRelevant, reasonFor]; decide

对一致性，展开并计算顺序要求及不同输出。

L105  · dsimp only [ReasonRelevant, reasonFor]; decide

对反身性，展开并计算旧规模成功与受质疑预测失败。

L106  · dsimp only [ReasonRelevant, reasonFor]; decide

对依据，展开并计算观测相等与扩展不等。

L107  · refine ⟨rfl, by decide, ?_⟩

对选择，证明容量身份与 maximal 超限，留下所选设计的界限。

L108    exact Nat.le_trans scope (by decide)

把所选复杂度 ≤ 3 与 3 ≤ 12 传递组合，得到所需界限。

L110theorem safeguardEnabled (principle : CoreCommitment) (selected : Candidate)

证明披露范围内每个原则的已启用实验均成功。

L111    (scope : valueScope selected) : safeguardExperiment principle true selected = true := by

保留范围前提，并陈述实际布尔值等于 true。

L112  cases principle

按五个原则分情况计算各自不同的实验。

L113  · dsimp only [safeguardExperiment]; decide

对生成，展开启用的改变列表并判定可信性测试。

L114  · dsimp only [safeguardExperiment]; decide

对一致性，展开启用的比较并判定对不兼容要求的拒绝。

L115  · dsimp only [safeguardExperiment]; decide

对反身性，展开两个测试并判定存在失败预测。

L116  · dsimp only [safeguardExperiment]; decide

对依据，展开获许可规模 10 列表并判定测试成功。

L117  · apply decide_eq_true

把选择实验的布尔结果转为底层容量命题。

L118    exact Nat.le_trans scope (by change 3 ≤ 12; decide)

利用范围及计算得到的 3 ≤ 12 证明该容量命题。

L120theorem safeguardDisabled (principle : CoreCommitment) (selected : Candidate) :

禁用保障对每个原则、所选设计均失败，无需范围前提。

L121    safeguardExperiment principle false selected = false := by

以计算出的实验值恰等于 false 陈述失败。

L122  cases principle <;> simp only [safeguardExperiment, Bool.false_eq_true, ↓reduceIte] <;> decide

拆分原则，化简禁用分支并判定五个有限结果。

L124theorem governanceValueProcedure (principle : CoreCommitment) :

逐原则验证实际治理价值程序。

L125    ValueProcedure (governancePosition principle) := by

目标是同一 governancePosition 的 ValueProcedure。

L126  refine ⟨by simp [governancePosition], ?_, ?_, ?_⟩

构造非空理由，留下相容性、目标与约束、回应义务。

L127  · refine ⟨.evolvable, (modelsSingleton _ _).2 (by change 3 ≤ 3; decide),

选择 evolvable 为起始理论见证，并证明其满足单元素范围理论。

L128      (by change 3 ≤ 3; decide), rfl, ?_⟩

证明其应用限制及选择身份，留下理由有效性。

L129    intro reason member

引入属于该立场理由列表的任意理由。

L130    cases List.mem_singleton.mp member

单元素成员资格将其确定为实际相关性理由。

L131    exact adoptionReasonRelevant principle .evolvable (by change 3 ≤ 3; decide)

在 evolvable 的复杂度界 3 ≤ 3 上应用已证相关性定理。

L132  · intro selected _ scope _

对程序前提下的任意设计，保留其范围证明。

L133    exact ⟨safeguardEnabled principle selected scope, scope⟩

以已启用实验成功及同一范围证明满足目标和约束。

L134  · intro selected _ _

在回应前提下引入任意批评案例。

L135    exact ⟨criticismFor principle, rfl, by cases principle <;> decide⟩

提供固定批评回应、其存储身份及由有限分情况证明的非空性。

L137theorem governanceGrounded (principle : CoreCommitment) :

governanceGrounded 为每个已表示原则的价值承诺提供依据。

L138    valueSpecification (governancePosition principle) :=

结论为精确治理立场的 valueSpecification。

L139  grounds012Singleton _ (governanceValueProcedure principle)

把已验证 ValueProcedure 包装进采纳版 Core 0.1.2 的单元素依据构造。

L141/- Factual relevance, rationale experiments and value adoption are separate.

注释区分事实相关性、理由实验与价值采纳。

L142Swapping a reason or altering the input makes the finite rationale fail. -/

注释引入通过替换理由或改变输入得到的失败案例。

L143theorem governanceRationaleLimits :

governanceRationaleLimits 展示实际失败，并区分支持与采纳。

L144    ¬ ReasonRelevant .consistency (reasonFor .generation) .evolvable ∧

生成理由因构造子不匹配而不相关于一致性。

L145    ¬ ReasonRelevant .reflexivity (.ownMethodCounterexample 21 10) .evolvable ∧

规模 10 的所谓自身反例失败，因为旧预测在那里一致。

L146    ¬ ReasonRelevant .generation (.plannedChange 9 .addition) .evolvable ∧

未支持的版本 9 新增计划不满足生成理由要求。

L147    ¬ valueScope .maximal ∧

maximal 位于复杂度不超过 3 的价值范围以外。

L148    (∀ principle, safeguardExperiment principle false .evolvable = false) ∧

每个禁用保障实验在 evolvable 上均失败。

L149    (∀ principle, (governancePosition principle).commitment .presentSimple) := by

与此同时，每个治理承诺在 presentSimple 上也被采纳。

L150  refine ⟨by change ¬ False; decide, by decide, by decide, by change ¬ (30 ≤ 3); decide,

计算三个理由不相关案例及 maximal 的 30 > 3 范围失败。

L151    fun principle => safeguardDisabled principle .evolvable, fun _ => rfl⟩

逐原则使用 safeguardDisabled，最后的全称采纳项由身份反身性成立。

L153/- This additional value priority is a real selection between the same designs.

注释把附加价值优先性表述为在相同设计之间的实际选择。

L154Both scopes retain all necessary domain conditions and no cost exception.

注释指出共同语境的必要条件及无成本例外；下文 limits 字段显式检查持续性与可信性。

L155The present-simple stance values less abstraction now without claiming that it

注释说明简单立场重视较低的当前抽象，并开始限定其能力主张。

L156has the better successor-maintainer capability. The other stance values that capability. -/

注释不为简单立场声称更强继任者能力，而把该目标归于另一立场。

L157def selectionObjective (adopted : Candidate) (outcome : Nat × Nat) : Prop :=

selectionObjective 把所采纳设计及复杂度、工作量二元组映射到其选定目标命题。

L158  match adopted with

目标随明确采纳的候选项改变。

L159  | .presentSimple => outcome.1 ≤ 1

presentSimple 重视当前抽象复杂度不超过 1。

L160  | .evolvable => outcome.2 ≤ 6

evolvable 重视设计修订工作量不超过 6。

L161  | .maximal => outcome.1 ≤ 1

maximal 分支也使用复杂度不超过 1；下文不证明 maximal 的程序成功。

L163def selectionPosition (adopted : Candidate) : ValuePosition Candidate where

以所采纳候选项为参数构造独立的选择 ValuePosition。

L164  Position := Candidate

其备选立场为实际 Candidate 设计。

L165  Outcome := Nat × Nat

结果是复杂度与修订工作量组成的自然数对。

L166  adopted := adopted

直接保存传入的已采纳候选项。

L167  selected := id

每个世界的所选立场就是自身，由恒等函数给出。

L168  outcome _ candidate := (abstractionComplexity candidate, changeWork candidate .designRevision)

衡量所选立场的复杂度与实际 designRevision 工作量。

L169  objective := selectionObjective adopted

采用由已采纳设计索引的目标。

L170  constraints _ candidate := abstractionComplexity candidate ≤ currentContinuing.limits.capacity .understanding

以实际理解容量约束该立场的复杂度。

L171  starting := singleton (fun candidate => candidate = adopted)

起始理论要求世界等于已采纳设计。

L172  reasons := [fun _ candidate =>

仅有一个理由函数，忽略世界参数并检查立场。

L173    abstractionComplexity candidate = (if adopted = .presentSimple then 1 else 3) ∧

采纳 presentSimple 时要求复杂度 1，否则要求复杂度 3。

L174    changeWork candidate .designRevision = (if adopted = .presentSimple then 17 else 6)]

采纳 presentSimple 时要求修订工作量 17，否则为 6。

L175  limits _ := Continuing currentContinuing.activity ∧

程序限制要求当前活动持续。

L176    credible currentContinuing.evidence .designRevision

还要求实际证据中 designRevision 可信。

L177  relevantCriticism _ := True

每个候选项都视为相关批评。

L178  response _ := some (if adopted = .presentSimple then

每项批评均得到按是否采纳 presentSimple 选取的回应。

L179    "The successor lacks the private-layout path; this choice does not claim evolution priority and must be reconsidered if that value is adopted."

简单设计回应承认继任者缺少私有布局路径，并说明不主张演化优先性。

L180    else "The six-step design-revision path does not establish every change is cheap or every forecast is correct.")

可演化回应限制六步结果的范围，不据此断言所有改变低成本或预测正确。

L182theorem selectionValueProcedure (adopted : Candidate)

验证某个已采纳候选项的选择价值程序。

L183    (ordinary : adopted = .presentSimple ∨ adopted = .evolvable) :

假设采纳的是两种普通设计之一。

L184    ValueProcedure (selectionPosition adopted) := by

结论为该采纳的实际 ValueProcedure。

L185  rcases ordinary with rfl | rfl

拆分并代入 presentSimple 与 evolvable 两种采纳。

L186  · refine ⟨by simp [selectionPosition], ?_, ?_, ?_⟩

对 presentSimple，证明理由非空并留下三个实质程序义务。

L187    · refine ⟨.presentSimple, (modelsSingleton _ _).2 rfl, ?_, rfl, ?_⟩

选择 presentSimple 本身作为相容见证，以反身性完成选择身份。

L188      · change Continuing currentContinuing.activity ∧ credible currentContinuing.evidence .designRevision

把见证限制显化为实际持续性及可信 designRevision。

L189        decide

计算这些固定语境事实。

L190      · intro reason member

引入简单立场单元素列表中的理由。

L191        cases List.mem_singleton.mp member

把该理由替换为唯一成员。

L192        decide

计算简单设计复杂度 1 及修订工作量 17。

L193    · intro selected _ _ allReasons

引入任意程序前提，为简单采纳保留 allReasons。

L194      have actual := allReasons _ (List.mem_singleton.mpr rfl)

从 allReasons 提取实际唯一理由。

L195      change abstractionComplexity .presentSimple = 1 ∧ changeWork .presentSimple .designRevision = 17 at actual

把理由显化为已采纳 presentSimple 的复杂度 1、工作量 17 两个具体等式。

L196      change abstractionComplexity .presentSimple ≤ 1 ∧

把简单设计目标显化为复杂度不超过 1。

L197        abstractionComplexity .presentSimple ≤ currentContinuing.limits.capacity .understanding

第二个合取项为同一设计的理解容量约束。

L198      exact ⟨by rw [actual.1]; exact Nat.le_refl _, by rw [actual.1]; decide⟩

按实际复杂度等式重写，目标由 ≤ 反身性、容量由计算完成。

L199    · intro selected _ _

对任意相关批评进入简单设计回应义务。

L200      refine ⟨_, rfl, ?_⟩

选择已存回应及其反身等式，留下非空性。

L201      simp

化简固定回应以证明非空。

L202  · refine ⟨by simp [selectionPosition], ?_, ?_, ?_⟩

对 evolvable，证明理由非空并留下同样三个程序义务。

L203    · refine ⟨.evolvable, (modelsSingleton _ _).2 rfl, ?_, rfl, ?_⟩

选择 evolvable 本身作为相容见证，并以反身性证明选择身份。

L204      · change Continuing currentContinuing.activity ∧ credible currentContinuing.evidence .designRevision

显化可演化见证的持续性及可信修订限制。

L205        decide

在 currentContinuing 中计算这些限制。

L206      · intro reason member

引入可演化立场单元素理由列表中的理由。

L207        cases List.mem_singleton.mp member

将其确定为唯一实际理由。

L208        decide

计算可演化设计复杂度 3 及修订工作量 6。

L209    · intro selected _ _ allReasons

引入可演化立场的程序前提，保留 allReasons。

L210      have actual := allReasons _ (List.mem_singleton.mpr rfl)

从此前提提取唯一实质理由。

L211      change abstractionComplexity .evolvable = 3 ∧ changeWork .evolvable .designRevision = 6 at actual

显化已采纳可演化立场的复杂度 3 与 designRevision 工作量 6。

L212      change changeWork .evolvable .designRevision ≤ 6 ∧

把可演化目标显化为工作量不超过 6。

L213        abstractionComplexity .evolvable ≤ currentContinuing.limits.capacity .understanding

保留对同一设计的实际理解容量约束。

L214      exact ⟨by rw [actual.2]; exact Nat.le_refl _, by rw [actual.1]; decide⟩

以工作量等式完成目标，以复杂度等式完成容量检查。

L215    · intro selected _ _

对任意相关批评进入可演化回应义务。

L216      refine ⟨_, rfl, ?_⟩

选择已存可演化回应，留下其非空性。

L217      simp

化简回应字符串以证明非空。

L219theorem selectionGrounded (adopted : Candidate)

selectionGrounded 为所采纳选择包装价值依据。

L220    (ordinary : adopted = .presentSimple ∨ adopted = .evolvable) :

两种普通设计的假设仍然显式保留。

L221    valueSpecification (selectionPosition adopted) :=

结论恰针对 selectionPosition adopted。

L222  grounds012Singleton _ (selectionValueProcedure adopted ordinary)

以已证明的选择程序作为已履行的单元素价值面向。

L224end CoreReader.Engineering

关闭 CoreReader.Engineering 命名空间；不另行断言数学主张。