leanified/CoreReader/Evidence.lean

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

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

展开 Lean 与逐行解读 · 721 行

Lean逐行解读

L1import CoreReader.Logic

导入 CoreReader.Logic，使其已检查声明可供本模块使用；这一行不提出新的哲学结论。

L2import CoreReader.Agency

导入 CoreReader.Agency，使其已检查声明可供本模块使用；这一行不提出新的哲学结论。

L4namespace CoreReader.Evidence

打开命名空间 CoreReader.Evidence，使后续声明获得这一模块限定名。

L5open CoreReader.Logic

允许不加限定使用 CoreReader.Logic 中的名称；这改变名称解析，不增加假设。

L6open CoreReader.Agency

允许不加限定使用 CoreReader.Agency 中的名称；这改变名称解析，不增加假设。

L8/- An observation records the outcome of a specified test on the represented world. -/

说明 Record 的预定范围。对应声明涉及：记录给定世界的布尔测试及其记录结果，不包含测量出处或真实性验证。 该注释用于解释，不是证明前提。

L9structure Record (W : Type) where

声明数据接口 Record。记录给定世界的布尔测试及其记录结果，不包含测量出处或真实性验证。

L10  test : W → Bool

保存读取实际被表示世界的指定布尔测试。

L11  observed : Bool

保存将与该测试比较的已观测布尔结果。

L12/- Compatible worlds reproduce the actual contents of every recorded observation. -/

说明 Compatible 的预定范围。对应声明涉及：每条记录的测试结果都必须与记录值一致；空列表允许任意世界。 该注释用于解释，不是证明前提。

L13def Compatible {W : Type} (records : List (Record W)) (w : W) : Prop :=

定义 Compatible。每条记录的测试结果都必须与记录值一致；空列表允许任意世界。

L14  ∀ r, r ∈ records → r.test w = r.observed

要求每条列出记录在 w 的真实测试等于该记录的观测结果。

L15/- Inferential support requires the same claim in every evidence-compatible world. -/

说明 Supports 的预定范围。对应声明涉及：主张在所有记录兼容世界成立；这是模型内蕴涵，不是统计置信度。 该注释用于解释，不是证明前提。

L16def Supports {W : Type} (records : List (Record W)) (claim : Claim W) : Prop :=

定义 Supports。主张在所有记录兼容世界成立；这是模型内蕴涵，不是统计置信度。

L17  ∀ w, Compatible records w → claim w

要求同一主张在与全部记录相容的每个世界成立；没有相容世界时，该蕴含本身可能空真。

L18/- Articulation identifies concepts, premises, reason contents and an application limit. -/

说明 Articulation 的预定范围。对应声明涉及：保存概念字符串、假设理论、理由列表和限度谓词。 该注释用于解释，不是证明前提。

L19structure Articulation (W : Type) where

声明数据接口 Articulation。保存概念字符串、假设理论、理由列表和限度谓词。

L20  concepts : List String

保存可识别概念名称；字符串本身不确立语义充分性。

L21  assumptions : Theory W

保存作为表述假设陈述的实际理论。

L22  reasons : List (Claim W)

把理由内容保存为针对同一世界类型的命题。

L23  limits : Claim W

保存这些理由的真实应用限度谓词。

L24/- Nonempty identifiable concepts and reasons are procedural articulation requirements. -/

说明 Articulated 的预定范围。对应声明涉及：只要求概念与理由列表非空，不单独保证相关性或充分性。 该注释用于解释，不是证明前提。

L25def Articulated {W : Type} (a : Articulation W) : Prop :=

定义 Articulated。只要求概念与理由列表非空，不单独保证相关性或充分性。

L26  a.concepts ≠ [] ∧ a.reasons ≠ []

只要求概念与理由列表非空；这一程序条件弱于匹配且已履行的 Grounds。

L27/- This application model interprets an adopted option through its actual outcomes and stated goals/constraints. -/

说明 ValuePosition 的预定范围。对应声明涉及：表示采纳选项、实际选择、选项相关结果及理由、目标、约束、起点、范围和批评响应；这是明示应用适配模型。 该注释用于解释，不是证明前提。

L28structure ValuePosition (W : Type) where

声明数据接口 ValuePosition。表示采纳选项、实际选择、选项相关结果及理由、目标、约束、起点、范围和批评响应；这是明示应用适配模型。

L29  Position : Type

给出该价值立场从中采纳某一项的选项类型。

L30  Outcome : Type

给出用于解释各选项效果的后果类型。

L31  adopted : Position

规定被采纳的选项，与世界实际选择哪个选项分开。

L32  selected : W → Position

从各世界读取实际选择的选项。

L33  outcome : W → Position → Outcome

解释各世界中各选项的真实后果，而不保存任意支持标签。

L34  objective : Outcome → Prop

把被采纳目标规定为后果上的谓词；该字段不证明其价值权威。

L35  constraints : W → Position → Prop

规定与目标一同检查、依赖世界和选项的约束。

L36  starting : Theory W

保存起点理论；JointAdoption 将要求它与采纳及理由具有真实共同模型。

L37  reasons : List (W → Position → Prop)

保存同时按世界与选项参数化的理由，因此切换采纳选项会改变受评理由。

L38  limits : Claim W

规定该价值评估程序主张结论的范围。

L39  relevantCriticism : Claim W

识别哪些世界存在相关批评；这是明确的应用谓词。

L40  response : W → Option String

保存各世界的可选文本回应；回应存在不证明批评已被充分回答。

L41/- The adopted position's claim is derived from the same selected option used by the outcome interpretation. -/

说明 ValuePosition.commitment 的预定范围。对应声明涉及：承诺主张表示世界选择了所采纳选项，不再是可独立重贴的任意主张字段。 该注释用于解释，不是证明前提。

L42def ValuePosition.commitment {W : Type} (v : ValuePosition W) : Claim W :=

定义 ValuePosition.commitment。承诺主张表示世界选择了所采纳选项，不再是可独立重贴的任意主张字段。

L43  fun w => v.selected w = v.adopted

通过实际选择等于同一采纳选项，导出承诺主张。

L44/- Assessed consequences concern this adopted option's actual outcome, objective and constraints. -/

说明 ValuePosition.consequence 的预定范围。对应声明涉及：以目标及约束检查该采纳选项的模型结果。 该注释用于解释，不是证明前提。

L45def ValuePosition.consequence {W : Type} (v : ValuePosition W) : Claim W :=

定义 ValuePosition.consequence。以目标及约束检查该采纳选项的模型结果。

L46  fun w => v.objective (v.outcome w v.adopted) ∧ v.constraints w v.adopted

根据同一采纳选项的真实后果满足目标及真实约束，导出受评后果。

L47/- Articulated reasons specialize the actual option-indexed premises to the adopted option. -/

说明 ValuePosition.activeReasons 的预定范围。对应声明涉及：把每个选项相关理由实例化到采纳选项，用于根据表达。 该注释用于解释，不是证明前提。

L48def ValuePosition.activeReasons {W : Type} (v : ValuePosition W) : List (Claim W) :=

定义 ValuePosition.activeReasons。把每个选项相关理由实例化到采纳选项，用于根据表达。

L49  v.reasons.map (fun reason w => reason w v.adopted)

把每个按选项索引的理由特化到采纳选项，形成其实际表述的世界谓词。

L50/- A joint witness excludes inconsistent starts and impossible adoption states. -/

说明 JointAdoption 的预定范围。对应声明涉及：要求存在一个世界，同时满足起点理论、范围、实际采纳及全部该选项理由。 该注释用于解释，不是证明前提。

L51def JointAdoption {W : Type} (v : ValuePosition W) : Prop :=

定义 JointAdoption。要求存在一个世界，同时满足起点理论、范围、实际采纳及全部该选项理由。

L52  ∃ w, Models v.starting w ∧ v.limits w ∧ v.commitment w ∧

要求起点假设、应用限度与实际采纳具有一个共同世界。

L53    ∀ reason, reason ∈ v.reasons → reason w v.adopted

在同一见证处，要求针对该采纳选项的全部列出理由共同成立。

L54/- This declared option/outcome adapter checks joint reasons for an assessed consequence; it is not a necessary deductive form for all value justification. -/

说明 ValueProcedure 的预定范围。对应声明涉及：要求非空理由、联合采纳见证、起点和范围内联合理由支持该选项后果，以及非空批评响应；不证明终极价值正确性。 该注释用于解释，不是证明前提。

L55def ValueProcedure {W : Type} (v : ValuePosition W) : Prop :=

定义 ValueProcedure。要求非空理由、联合采纳见证、起点和范围内联合理由支持该选项后果，以及非空批评响应；不证明终极价值正确性。

L56  v.reasons ≠ [] ∧ JointAdoption v ∧

以理由非空与完整共同采纳见证开始 ValueProcedure。

L57  (∀ w, Models v.starting w → v.limits w →

对满足真实起点理论与限度的每个世界，施加后续条件后果要求。

L58    (∀ reason, reason ∈ v.reasons → reason w v.adopted) → v.consequence w) ∧

用采纳选项的全部理由合取蕴含其真实后果；不要求单条理由充分。

L59  (∀ w, v.limits w → v.relevantCriticism w → ∃ answer, v.response w = some answer ∧ answer ≠ "")

在限度内，每项相关批评必须有指定的非空回应；这里检查回应记录，而非说服力。

L60/- A facet carries its specific contents; several different facets can have the same conclusion. -/

说明 Facet 的预定范围。对应声明涉及：区分经验、推论、价值三个面向；同一主张可有多个面向。 该注释用于解释，不是证明前提。

L61inductive Facet (W : Type) where

声明可选构造 Facet。区分经验、推论、价值三个面向；同一主张可有多个面向。

L62  | empirical (records : List (Record W)) (scope conclusion uncertainty : Claim W)

经验方面保存真实测试记录，以及范围、结论与所述不确定性谓词。

L63  | inferential (assumptions : Theory W) (conclusion : Claim W)

推论方面保存真实前提理论及待从中蕴含的结论。

L64  | value (position : ValuePosition W)

价值方面保存完整的选项与后果立场，包括起点理论、理由、限度及批评回应。

L65/- The claim referred to by each assessment facet is explicit. -/

说明 Facet.claim 的预定范围。对应声明涉及：抽取经验或推论结论，价值面向则抽取其立场承诺。 该注释用于解释，不是证明前提。

L66def Facet.claim {W : Type} : Facet W → Claim W

定义 Facet.claim。抽取经验或推论结论，价值面向则抽取其立场承诺。

L67  | .empirical _ _ p _ => p

把经验方面自身结论 p 读为主张；记录、范围与不确定性仍为评估输入。

L68  | .inferential _ p => p

把推论方面自身结论 p 读为主张，与前提理论分开。

L69  | .value v => v.commitment

价值方面的主张是实际选择等于自身采纳选项，通过 v.commitment 导出。

L70/- These disclosed semantic adapters implement selected nature-specific checks; passing them does not establish all real empirical or value adequacy. -/

说明 FacetDischarged 的预定范围。对应声明涉及：经验要求非空范围见证及支持，推论要求假设可满足且蕴涵结论，价值使用声明的程序接口。 该注释用于解释，不是证明前提。

L71def FacetDischarged {W : Type} : Facet W → Prop

定义 FacetDischarged。经验要求非空范围见证及支持，推论要求假设可满足且蕴涵结论，价值使用声明的程序接口。

L72  | .empirical records scope p uncertainty =>

进入经验履行情况，使用该方面真实记录、范围、结论 p 与不确定性谓词。

L73      (∃ w, Compatible records w ∧ scope w) ∧

对经验方面，要求存在与记录相容且在范围内的世界，排除空经验域。

L74      Supports records (fun w => scope w → p w) ∧ Supports records uncertainty

要求记录支持范围内结论及明确规定的不确定性谓词。

L75  | .inferential assumptions p => Satisfiable assumptions ∧ Entails assumptions p

推论履行要求真实假设具有非空模型，且同一假设语义蕴含 p。

L76  | .value v => ValueProcedure v

价值履行恰为同一立场声明的 ValueProcedure，不是终极价值充分性的证明。

L77/- This model's semantic adapter identifies the actual assumptions, reason content and limit of a facet. -/

说明 FacetArticulated 的预定范围。对应声明涉及：要求表达中的假设、理由和限度与对应面向精确对齐。 该注释用于解释，不是证明前提。

L78def FacetArticulated {W : Type} (a : Articulation W) : Facet W → Prop

定义 FacetArticulated。要求表达中的假设、理由和限度与对应面向精确对齐。

L79  | .empirical records scope _ _ =>

在经验表述情况下，读取假设、理由与限度必须匹配的真实记录与范围。

L80      a.assumptions = singleton (Compatible records) ∧ a.reasons = [Compatible records] ∧ a.limits = scope

这一经验适配器把表述假设及理由与实际记录相容性等同，并把表述限度与经验范围等同。

L81  | .inferential assumptions _ =>

在推论情况下，以该方面真实假设理论作为表述参照。

L82      a.assumptions = assumptions ∧ a.reasons = [Models assumptions] ∧ a.limits = (fun _ => True)

这一推论适配器保留准确前提理论，将其模型条件表述为理由，并使用不受限的附加限度。

L83  | .value v => a.assumptions = v.starting ∧ a.reasons = v.activeReasons ∧ a.limits = v.limits

要求价值表述准确使用该立场的起点理论、采纳选项有效理由与限度。

L84/- A canonical articulation exposes this adapter; the source does not mandate this particular representation of grounds. -/

说明 canonicalArticulation 的预定范围。对应声明涉及：按面向构造固定概念标签及与该面向对齐的假设、理由和限度。 该注释用于解释，不是证明前提。

L85def canonicalArticulation {W : Type} : Facet W → Articulation W

定义 canonicalArticulation。按面向构造固定概念标签及与该面向对齐的假设、理由和限度。

L86  | .empirical records scope _ _ =>

从所选方面真实记录列表与范围构造经验规范表述。

L87      ⟨["recorded test outcomes", "observation conditions"], singleton (Compatible records), [Compatible records], scope⟩

构造命名测试结果与条件的经验表述，以实际相容性主张为前提和理由，原范围为限度。

L88  | .inferential assumptions _ =>

从该方面真实前提理论构造推论规范表述。

L89      ⟨["stated assumptions", "semantic consequence"], assumptions, [Models assumptions], fun _ => True⟩

从同一理论及其真实模型谓词构造推论表述，不增加限度。

L90  | .value v =>

使用同一完整立场 v 构造价值表述。

L91      ⟨["adopted position", "reasons and consequences"], v.starting, v.activeReasons, v.limits⟩

从真实起点理论、采纳选项理由与原限度构造价值表述。

L92/- Canonical articulation is connected to the very facet whose grounds it identifies. -/

说明 canonicalFacetArticulated 的预定范围。对应声明涉及：逐个面向用自反等式证明规范表达与原面向对齐。 该注释用于解释，不是证明前提。

L93theorem canonicalFacetArticulated {W : Type} (f : Facet W) :

陈述经检查的结果 canonicalFacetArticulated。逐个面向用自反等式证明规范表达与原面向对齐。

L94    FacetArticulated (canonicalArticulation f) f := by

断言规范表述与同一方面具有语义连接；证明检查各方面构造子。

L95  cases f <;> exact ⟨rfl, rfl, rfl⟩

按三个方面构造子分类；各规范表述恰有对应分支要求的假设、理由与限度，三个等式均由自反性成立。

L96/- A discharged facet has nonempty canonical reason articulation, including the value procedure's reason requirement. -/

说明 canonicalArticulated 的预定范围。对应声明涉及：由已完成面向证明规范表达的概念与理由非空。 该注释用于解释，不是证明前提。

L97theorem canonicalArticulated {W : Type} (f : Facet W) (h : FacetDischarged f) :

陈述经检查的结果 canonicalArticulated。由已完成面向证明规范表达的概念与理由非空。

L98    Articulated (canonicalArticulation f) := by

给定该方面已履行，要求其规范概念与理由非空。

L99  cases f with

分别检查经验、推论与价值方面的规范表述。

L100  | empirical records scope p uncertainty => simp [Articulated, canonicalArticulation]

在这一经验或推论分支中，规范概念列表和理由列表明确非空；化简验证两个表述要求。

L101  | inferential assumptions p => simp [Articulated, canonicalArticulation]

在这一经验或推论分支中，规范概念列表和理由列表明确非空；化简验证两个表述要求。

L102  | value v =>

在价值分支，前提 h 为 ValueProcedure v；其中理由非空必须确立规范有效理由非空。

L103      refine ⟨by simp [canonicalArticulation], ?_⟩

对价值方面给出规范概念非空性，留下有效理由列表非空的义务。

L104      simpa [canonicalArticulation, ValuePosition.activeReasons] using h.1

利用通过检查的价值程序中的理由非空性；将理由特化到采纳选项保持非空。

L105/- This model of the Grounds obligation binds each actual facet to its claim and articulation. Its disclosed FacetDischarged adapters do not replace all source-level assessment responsibilities or prove real adequacy. -/

说明 Grounds 的预定范围。对应声明涉及：要求非空面向清单、覆盖声明适用面、同一主张、表达对齐及各面向检查；不是现实充分性的统一判定器。 该注释用于解释，不是证明前提。

L106def Grounds {W : Type} (claim : Claim W) (articulations : Facet W → Articulation W)

定义 Grounds。要求非空面向清单、覆盖声明适用面、同一主张、表达对齐及各面向检查；不是现实充分性的统一判定器。

L107    (actualApplicable : Facet W → Prop) (facets : List (Facet W)) : Prop :=

独立于有限列表接收 actualApplicable，使覆盖成为明确义务，而非从列表成员关系推定。

L108  facets ≠ [] ∧ (∀ facet, actualApplicable facet → facet ∈ facets) ∧

要求方面列表非空，并包含每个满足 actualApplicable 的方面。

L109  ∀ facet, facet ∈ facets → facet.claim = claim ∧ Articulated (articulations facet) ∧

对每个列出方面，要求主张准确相同，并有属于该方面的非空表述。

L110    FacetArticulated (articulations facet) facet ∧ FacetDischarged facet

还要求语义匹配真实前提、理由与限度，并通过其声明的适配器履行。

L111/- The achievement obligation requires grounds for this very claim, without making observation a universal prerequisite. -/

说明 AchievementAccountability 的预定范围。对应声明涉及：将成就主张交给同一Grounds接口，不另提供现实成就证明。 该注释用于解释，不是证明前提。

L112def AchievementAccountability {W : Type} (achievement : Claim W) (articulations : Facet W → Articulation W)

定义 AchievementAccountability。将成就主张交给同一Grounds接口，不另提供现实成就证明。

L113    (actualApplicable : Facet W → Prop) (facets : List (Facet W)) : Prop :=

成就问责接收与 Grounds 相同的实际适用性谓词及方面列表。

L114  Grounds achievement articulations actualApplicable facets

直接以同一成就主张的 Grounds 定义问责，不增加普遍观测要求。

L115/- The concrete achievement claim refers to each transition's own before/after states. -/

说明 transitionAchievement 的预定范围。对应声明涉及：把成就定义为同一模型变化前后状态的理解或构造扩展。 该注释用于解释，不是证明前提。

L116def transitionAchievement : Claim TransitionCase :=

定义 transitionAchievement。把成就定义为同一模型变化前后状态的理解或构造扩展。

L117  fun transition => Expanded (transitionBefore transition) (transitionAfter transition)

成就主张为所选变化自身前后状态之间的真实扩展。

L118/- This observation inspects an actually constructed successor and its output under that transition's input condition. -/

说明 transitionPerformanceRecord 的预定范围。对应声明涉及：在两个变化模型中，测试同一后状态是否包含在该输入输出一的successor。 该注释用于解释，不是证明前提。

L119def transitionPerformanceRecord : Record TransitionCase :=

定义 transitionPerformanceRecord。在两个变化模型中，测试同一后状态是否包含在该输入输出一的successor。

L120  ⟨fun transition => (transitionAfter transition).constructed.any

表现测试检查该变化后状态中实际建构的操作。

L121    (fun operation => operation == .successor && decide (operation.run (transitionInput transition) = 1)), true⟩

只有后继操作存在且确实把共同变化输入变为 1 时，测试才记录 true。

L122/- The positive report test reads its asserted operation, input and output; it does not verify their presence in the after-state. -/

说明 transitionReportRecord 的预定范围。对应声明涉及：仅记录报告宣称的操作、输入与输出，不直接记录成就是否实现。 该注释用于解释，不是证明前提。

L123def transitionReportRecord : Record TransitionCase :=

定义 transitionReportRecord。仅记录报告宣称的操作、输入与输出，不直接记录成就是否实现。

L124  ⟨fun transition =>

开始构造一条读取实际变化公告的记录。

L125    let report := transitionAnnouncement transition

把 report 绑定到为同一变化生成的公告。

L126    report.reportedNewOperation == .successor && report.input == 0 && report.expectedOutput == 1, true⟩

测试其所述后继操作、输入 0 与预期输出 1；记录积极公告，不据此确定操作存在。

L127/- Only the genuine extension matches the operation/performance observation in this two-transition model. -/

说明 transitionPerformanceCompatible 的预定范围。对应声明涉及：穷尽膨胀与扩展两类，证明实际表现记录识别能力扩展。 该注释用于解释，不是证明前提。

L128theorem transitionPerformanceCompatible :

陈述经检查的结果 transitionPerformanceCompatible。穷尽膨胀与扩展两类，证明实际表现记录识别能力扩展。

L129    ∀ transition, Compatible [transitionPerformanceRecord] transition ↔ transition = .extend := by

主张匹配真实积极表现记录当且仅当所选变化为 extend。

L130  intro transition

固定任意实际变化 inflate 或 extend，以证明记录相容性等价关系。

L131  constructor

证明两个方向：表现相容性推出 extend，extend 则提供相容性。

L132  · intro h

假定该变化匹配真实积极表现记录。

L133    have observed := h transitionPerformanceRecord (List.mem_singleton.mpr rfl)

把相容性应用于真实单元素表现记录，得到该变化的观测测试结果。

L134    cases transition

把实际变化分为 inflate 与 extend，两者后状态的操作内容不同。

L135    · cases observed

inflate 状态缺少后继操作，因此其表现测试不可能等于记录的 true。

L136    · rfl

extend 情况通过自反性满足所需变化身份。

L137  · intro h; cases h

反方向中，代入变化等于 extend 的假设。

L138    intro record hr; have hr' := List.mem_singleton.mp hr; subst record

单元素记录列表的成员关系把任意记录确定为这一准确变化记录；先代入，再检查测试。

L139    rfl

计算真实 extend 表现记录；其零输入后继测试等于记录的 true。

L140/- A compatible performance observation establishes the same transition's report content and hence its represented expansion. -/

说明 transitionSupported 的预定范围。对应声明涉及：从表现识别、实际新增操作及报告内容，证明每个兼容变化都发生扩展。 该注释用于解释，不是证明前提。

L141theorem transitionSupported : Supports [transitionPerformanceRecord] transitionAchievement := by

陈述经检查的结果 transitionSupported。从表现识别、实际新增操作及报告内容，证明每个兼容变化都发生扩展。 后续策略块证明这一显式类型。

L142  intro transition compatible

任取变化及其与真实表现记录的相容性，证明同一变化发生扩展。

L143  have h := (transitionPerformanceCompatible transition).1 compatible

用 transitionPerformanceCompatible 把每个与表现证据相容的变化确定为 extend。

L144  subst transition

用 extend 替换变化，使剩余成就主张针对其真实扩展后状态。

L145  have reportTrue : (transitionAnnouncement .extend).claim := by

针对真实前后状态检查同一系统生成的 extend 报告：后继操作确为新增建构，并把输入 0 变为输出 1。

L146    simp [transitionAnnouncement, transitionAfter, transitionInput,

针对真实前后状态检查同一系统生成的 extend 报告：后继操作确为新增建构，并把输入 0 变为输出 1。

L147      Announcement.claim, GeneratingSystem.report, generatingSystem, extendedState, baseState, Operation.run]

针对真实前后状态检查同一系统生成的 extend 报告：后继操作确为新增建构，并把输入 0 变为输出 1。

L148  exact announcementClaimImpliesExpansion _ reportTrue

将 announcementClaimImpliesExpansion 应用于已核实报告内容，得到同一变化的 Expanded 主张。

L149/- The actual scope is the shared input-zero condition, with no probabilistic inference introduced. -/

说明 transitionFacet 的预定范围。对应声明涉及：把表现记录、零输入范围及精确扩展主张组成经验面向。 该注释用于解释，不是证明前提。

L150def transitionFacet : Facet TransitionCase :=

定义 transitionFacet。把表现记录、零输入范围及精确扩展主张组成经验面向。

L151  .empirical [transitionPerformanceRecord] (fun transition => transitionInput transition = 0)

从表现记录构造经验方面，并采用准确的输入 0 变化范围。

L152    transitionAchievement (fun _ => True)

其结论为同一变化的成就，不确定性谓词明确为 True。

L153/- The empirical assessment has a real compatible witness and supports this scoped achievement. -/

说明 transitionFacetDischarged 的预定范围。对应声明涉及：以扩展为非空见证，提供真实模型支持和恒真不确定性条件。 该注释用于解释，不是证明前提。

L154theorem transitionFacetDischarged : FacetDischarged transitionFacet := by

陈述经检查的结果 transitionFacetDischarged。以扩展为非空见证，提供真实模型支持和恒真不确定性条件。 后续策略块证明这一显式类型。

L155  refine ⟨⟨.extend, (transitionPerformanceCompatible _).2 rfl, rfl⟩, ?_, ?_⟩

提供 extend 作为非空经验见证，包含相容表现证据与共同输入 0 范围；留下范围内支持及不确定性检查。

L156  · intro transition compatible _; exact transitionSupported transition compatible

已证的变化支持为任意相容变化提供成就结论，因此也在所选范围内成立。

L157  · intro _ _; trivial

明确不受限的不确定性谓词为 True，因此该适配器组件直接成立；并未推得定量不确定性界限。

L158/- Every applicable facet of this specified achievement has matching articulation and actual discharged evidence. -/

说明 transitionAccountable 的预定范围。对应声明涉及：用同一成就主张、范围、规范表达及已检查面向建立成就Grounds。 该注释用于解释，不是证明前提。

L159theorem transitionAccountable :

陈述经检查的结果 transitionAccountable。用同一成就主张、范围、规范表达及已检查面向建立成就Grounds。

L160    AchievementAccountability transitionAchievement canonicalArticulation

陈述真实变化成就谓词的问责，并采用规范表述。

L161      (fun facet => facet = transitionFacet) [transitionFacet] := by

声明 transitionFacet 为唯一适用方面，并使用准确的单元素证据组合。

L162  refine ⟨by simp, ?_, ?_⟩

把问责拆为方面列表非空、覆盖实际适用性，以及各列出方面的匹配表述与履行。

L163  · intro facet hf; subst facet; exact List.mem_singleton.mpr rfl

适用性假设把方面确定为规定的唯一方面，因此它属于该单元素列表。

L164  · intro facet hf; have hf' := List.mem_singleton.mp hf; subst facet

单元素成员关系把当前方面确定为规定方面；代入后检查其准确主张与依据。

L165    exact ⟨rfl, canonicalArticulated _ transitionFacetDischarged,

组合主张相同、规范表述非空、表述与同一方面的语义连接，以及 transitionFacetDischarged。

L166      canonicalFacetArticulated _, transitionFacetDischarged⟩

组合主张相同、规范表述非空、表述与同一方面的语义连接，以及 transitionFacetDischarged。

L167/- Both actual transitions issue the same positive report about their own identified state pair. -/

说明 transitionReportCompatible 的预定范围。对应声明涉及：证明两种变化都能产生相同的宣称操作、输入和输出记录。 该注释用于解释，不是证明前提。

L168theorem transitionReportCompatible (transition : TransitionCase) :

陈述经检查的结果 transitionReportCompatible。证明两种变化都能产生相同的宣称操作、输入和输出记录。

L169    Compatible [transitionReportRecord] transition := by

陈述该变化的积极报告记录与变化自身相容，也包括 inflate。

L170  intro record hr; have hr' := List.mem_singleton.mp hr; subst record

单元素记录列表的成员关系把任意记录确定为这一准确变化记录；先代入，再检查测试。

L171  rfl

报告测试只检查真实的积极公告内容，两种变化中的公告内容计算结果相同。

L172/- Inflation is a concrete report-compatible counterworld, so the positive report alone does not support the same achievement claim. -/

说明 transitionReportDoesNotSupport 的预定范围。对应声明涉及：以库存膨胀变化作为符合自述却未实现成就的反模型。 该注释用于解释，不是证明前提。

L173theorem transitionReportDoesNotSupport :

陈述经检查的结果 transitionReportDoesNotSupport。以库存膨胀变化作为符合自述却未实现成就的反模型。

L174    Compatible [transitionReportRecord] .inflate ∧ ¬ transitionAchievement .inflate ∧

要求 inflate 匹配报告，却未满足同一成就谓词。

L175    ¬ Supports [transitionReportRecord] transitionAchievement := by

因此断言积极报告记录不能在全部相容变化上支持该成就。

L176  have noExpansion : ¬ transitionAchievement .inflate := by

展开 inflate 变化：理解和建构操作集合均未改变，因此不存在 Expanded 要求的新操作见证。

L177    simp [transitionAchievement, transitionBefore, transitionAfter, Expanded, baseState, inflatedState]

展开 inflate 变化：理解和建构操作集合均未改变，因此不存在 Expanded 要求的新操作见证。

L178  exact ⟨transitionReportCompatible _, noExpansion, fun h => noExpansion (h _ (transitionReportCompatible _))⟩

组合 inflate 处的积极报告相容性与扩展主张为假；任何假定支持应用于此都会产生矛盾。

L179/- These concrete obligations, positive evidence and negative report case all refer to the same state-pair and input semantics. -/

说明 ConcreteAchievementExample 的预定范围。对应声明涉及：组合同对象成就责任与获支持扩展，以及不获支持膨胀自述，并保留前后状态和输入身份。 该注释用于解释，不是证明前提。

L180def ConcreteAchievementExample : Prop :=

定义 ConcreteAchievementExample。组合同对象成就责任与获支持扩展，以及不获支持膨胀自述，并保留前后状态和输入身份。

L181  AchievementAccountability transitionAchievement canonicalArticulation

具体实例包含真实变化成就的实际问责。

L182    (fun facet => facet = transitionFacet) [transitionFacet] ∧

其实际适用性谓词与列表确定同一个变化方面。

L183  Compatible [transitionPerformanceRecord] .extend ∧

要求 extend 满足真实表现观测。

L184  Supports [transitionPerformanceRecord] transitionAchievement ∧ transitionAchievement .extend ∧

要求成就具有语义支持，且在 extend 处为真。

L185  (Compatible [transitionReportRecord] .inflate ∧ ¬ transitionAchievement .inflate ∧

还保留与报告相容但该成就为假的 inflate 世界。

L186    ¬ Supports [transitionReportRecord] transitionAchievement) ∧

陈述由此得到的仅凭报告支持失败。

L187  (∀ transition, (transitionAnnouncement transition).before = transitionBefore transition ∧

对每种变化，把报告前状态绑定到真实变化前状态。

L188    (transitionAnnouncement transition).after = transitionAfter transition ∧

把报告后状态绑定到同一变化的真实后状态。

L189    (transitionAnnouncement transition).input = transitionInput transition ∧ transitionInput transition = 0)

把报告输入绑定到真实变化输入，并明确把该条件固定为 0。

L190/- The concrete example jointly inhabits accountability, evidence compatibility, actual gain, and the report-only countermodel. -/

说明 concreteAchievementExample 的预定范围。对应声明涉及：组合实际表现支持、自述反模型和精确状态与输入联系。 该注释用于解释，不是证明前提。

L191theorem concreteAchievementExample : ConcreteAchievementExample := by

陈述经检查的结果 concreteAchievementExample。组合实际表现支持、自述反模型和精确状态与输入联系。 后续策略块证明这一显式类型。

L192  refine ⟨transitionAccountable, (transitionPerformanceCompatible _).2 rfl, transitionSupported,

在具体实例中组合真实成就的问责、extend 表现相容性与语义支持。

L193    transitionSupported .extend ((transitionPerformanceCompatible _).2 rfl),

将同一支持应用于 extend 见证，确立该处的实际扩展。

L194    transitionReportDoesNotSupport, ?_⟩

纳入与报告相容的 inflate 反例，留下前后状态与输入相同的关系证明。

L195  intro transition; exact ⟨rfl,rfl,rfl,rfl⟩

对任一变化，所有报告与状态连接及输入 0 的关系均由定义本身成立。

L196/- Semantic evidence yields truth only at a world that actually satisfies those evidence conditions. -/

说明 achievementNeedsSupport 的预定范围。对应声明涉及：对任意实际主张应用所给兼容性与支持，并另附已检查的具体变化实例。 该注释用于解释，不是证明前提。

L197theorem achievementNeedsSupport {W : Type} (achievement : Claim W) (records : List (Record W))

陈述经检查的结果 achievementNeedsSupport。对任意实际主张应用所给兼容性与支持，并另附已检查的具体变化实例。

L198    (actual : W) (reliableHere : Compatible records actual) (support : Supports records achievement) :

假定所选实际世界匹配全部记录，且这些记录已经支持成就。

L199    achievement actual ∧ ConcreteAchievementExample :=

得出该实际世界中的成就为真，并附带另行构造的具体成就实例。

L200  ⟨support actual reliableHere, concreteAchievementExample⟩

把已假定支持应用于实际证据相容世界，并将该局部真值与另行证明的具体成就实例组合。

L201/- Weakening a conclusion preserves support; this makes no claim about weakening the evidence. -/

说明 supportWeakening 的预定范围。对应声明涉及：同一证据支持p且p在每个世界推出q时，也支持较弱结论q。 该注释用于解释，不是证明前提。

L202theorem supportWeakening {W : Type} (records : List (Record W)) (p q : Claim W)

陈述经检查的结果 supportWeakening。同一证据支持p且p在每个世界推出q时，也支持较弱结论q。

L203    (support : Supports records p) (weaker : ∀ w, p w → q w) : Supports records q :=

假定 p 已获支持且逐世界有 p 蕴含 q；使用相同记录得出 q 已获支持。

L204  fun w hw => weaker w (support w hw)

在每个相容世界 w，先用不变记录得出 p，再应用给定蕴含 weaker 得到 q。

L205/- Discarding the only informative observation loses support for the unchanged switch claim. -/

说明 evidenceWeakeningCanLoseSupport 的预定范围。对应声明涉及：真布尔观察支持世界为真，删除该记录后假世界成为反例。 该注释用于解释，不是证明前提。

L206theorem evidenceWeakeningCanLoseSupport :

陈述经检查的结果 evidenceWeakeningCanLoseSupport。真布尔观察支持世界为真，删除该记录后假世界成为反例。

L207    Supports ([⟨id, true⟩] : List (Record Bool)) (fun w => w = true) ∧

单一恒等观测支持布尔世界为 true。

L208    ¬ Supports ([] : List (Record Bool)) (fun w => w = true) := by

删除该观测后记录为空，不能支持未改变的主张。

L209  refine ⟨?_, ?_⟩

分开单条记录支持主张与删除该记录后同一主张不获支持两个目标。

L210  · intro w hw; exact hw ⟨id,true⟩ (by simp)

从相容性读出有信息的恒等测试，它直接表明布尔世界为 true。

L211  · intro h; have bad := h false (by intro r hr; cases hr); cases bad

没有记录时 false 也相容；在该处检验假定支持，否定未改变的真世界主张。

L212/- Restricting the quantified application domain preserves a supported universal conclusion. -/

说明 scopeRestriction 的预定范围。对应声明涉及：在narrow包含于wide的明确前提下，将支持结论的量词域缩窄。 该注释用于解释，不是证明前提。

L213theorem scopeRestriction {W X : Type} (records : List (Record W)) (p : W → X → Prop)

陈述经检查的结果 scopeRestriction。在narrow包含于wide的明确前提下，将支持结论的量词域缩窄。

L214    (wide narrow : X → Prop) (included : ∀ x, narrow x → wide x)

接收广域与窄域，并假定每个窄域输入均属于广域。

L215    (support : Supports records (fun w => ∀ x, wide x → p w x)) :

假定相同记录支持广域中每个输入上的 p。

L216    Supports records (fun w => ∀ x, narrow x → p w x) :=

得出窄域中每个输入上的支持；证据与谓词 p 都不改变。

L217  fun w hw x hx => support w hw x (included x hx)

对相容世界与窄域输入 x，included 将窄域成员关系转为广域成员关系，再在该处应用原广域支持。

L218/- Actual applicability, rather than an optional classifier label, determines facet responsibility. -/

说明 Duties 的预定范围。对应声明涉及：要求每个声明适用的面向完成其相应检查。 该注释用于解释，不是证明前提。

L219def Duties {W : Type} (applicable : Facet W → Prop) : Prop :=

定义 Duties。要求每个声明适用的面向完成其相应检查。

L220  ∀ f, applicable f → FacetDischarged f

要求每个实际适用方面通过其自身履行条件。

L221def LabeledDuties {W : Type} (_labels : List String) (applicable : Facet W → Prop) : Prop :=

定义 LabeledDuties。完全忽略标签，保留由适用性决定的义务。

L222  Duties applicable

把带标签责任定义为原有适用性责任；标签不提供豁免。

L223/- Combining applicable facets requires both sets of substantive duties. -/

说明 assessmentUnion 的预定范围。对应声明涉及：用析取分支证明适用面向并集的义务等价于分别履行两部分。 该注释用于解释，不是证明前提。

L224theorem assessmentUnion {W : Type} (a b : Facet W → Prop) :

陈述经检查的结果 assessmentUnion。用析取分支证明适用面向并集的义务等价于分别履行两部分。

L225    Duties (fun f => a f ∨ b f) ↔ Duties a ∧ Duties b := by

将两个适用性谓词并集的责任等同于两组责任均履行。

L226  constructor

证明并集适用性谓词的责任与两个组成部分同时履行责任之间的两个方向。

L227  · intro h; exact ⟨fun f hf => h f (Or.inl hf), fun f hf => h f (Or.inr hf)⟩

利用对应析取嵌入，把并集责任分别限制到各适用方面谓词。

L228  · rintro ⟨ha,hb⟩ f (hf|hf); exact ha f hf; exact hb f hf

拆出两组责任，把实际适用性分为左右情况，并用对应责任履行同一方面。

L229/- Omitting or changing labels does not remove an applicable duty. -/

说明 labelsCannotWaive 的预定范围。对应声明涉及：标签不进入义务定义，因此改变标签不改变义务。 该注释用于解释，不是证明前提。

L230theorem labelsCannotWaive {W : Type} (xs ys : List String) (a : Facet W → Prop) :

陈述经检查的结果 labelsCannotWaive。标签不进入义务定义，因此改变标签不改变义务。

L231    LabeledDuties xs a ↔ LabeledDuties ys a := Iff.rfl

只改变标签列表不改变责任命题；该等价由自反性成立。

L232/- The observed switch is the outcome itself, not a record identifier. -/

说明 switchRecord 的预定范围。对应声明涉及：记录布尔恒等测试结果为真。 该注释用于解释，不是证明前提。

L233def switchRecord : Record Bool := ⟨id, true⟩

定义 switchRecord。记录布尔恒等测试结果为真。

L234theorem switchCompatible (w : Bool) : Compatible [switchRecord] w ↔ w = true := by

陈述经检查的结果 switchCompatible。证明与单条switch观察相容等价于布尔世界为真。 后续策略块证明这一显式类型。

L235  constructor

证明与单元素开关记录相容，当且仅当真实布尔世界为 true。

L236  · intro h; exact h switchRecord (by simp)

把记录相容性应用于唯一指定测试，恢复其真实观测等式。

L237  · intro hw r hr; simp only [List.mem_singleton] at hr; cases hr; exact hw

反方向中，单元素成员关系把任意列出记录确定为该测试，其等式即为给定观测前提。

L238theorem switchSupported : Supports [switchRecord] (fun w : Bool => w = true) :=

陈述经检查的结果 switchSupported。从兼容性等价关系抽取被记录的真值结论。 给出的证明项使用所示构造见证或先前引理，而不增加公理。

L239  fun w hw => (switchCompatible w).1 hw

使用 switchCompatible 的正向蕴含，从同一世界真实记录相容性提取 world=true。

L240/- The candidate action has specific benefit and cost outcomes; its inactive alternative has neither. -/

说明 optionBenefit 的预定范围。对应声明涉及：选择true时收益为四，否则为零。 该注释用于解释，不是证明前提。

L241def optionBenefit (selected : Bool) : Nat := if selected then 4 else 0

定义 optionBenefit。选择true时收益为四，否则为零。

L242def optionCost (selected : Bool) : Nat := if selected then 3 else 0

定义 optionCost。选择true时成本为三，否则为零。

L243/- The report describes each option's actual cost and benefit; it does not itself assert which option ought to be selected. -/

说明 optionReport 的预定范围。对应声明涉及：陈述与选项对应的成本和收益事实，不使用无关根据标记。 该注释用于解释，不是证明前提。

L244def optionReport (selected : Bool) : Prop :=

定义 optionReport。陈述与选项对应的成本和收益事实，不使用无关根据标记。

L245  optionCost selected ≤ 3 ∧ optionBenefit selected = (if selected then 4 else 0)

选项报告断言真实成本至多为 3，以及开启收益为 4、关闭收益为 0。

L246/- The on position connects its own selected option to that option's benefit/cost outcome. -/

说明 switchPosition 的预定范围。对应声明涉及：采纳true选项，使用实际成本收益、成本小于收益目标、预算约束和范围内批评响应。 该注释用于解释，不是证明前提。

L247def switchPosition : ValuePosition Bool where

定义 switchPosition。采纳true选项，使用实际成本收益、成本小于收益目标、预算约束和范围内批评响应。

L248  Position := Bool

使用布尔选项表示开启与关闭。

L249  Outcome := Nat × Nat

以自然数对表示各后果的真实收益与成本。

L250  adopted := true

明确采纳开启选项；采纳本身不是从算术推导的。

L251  selected := id

直接从布尔世界读取实际选择。

L252  outcome := fun _ option => (optionBenefit option, optionCost option)

从同一真实选项计算收益与成本。

L253  objective := fun result => result.2 < result.1

采纳真实收益严格超过真实成本这一目标。

L254  constraints := fun _ option => optionCost option ≤ 3

按固定预算 3 检查实际选项成本。

L255  starting := singleton (fun w => w = true)

假定实际布尔选择为开启；不把受评收益结论加入起点理论。

L256  reasons := [fun _ option => optionReport option]

以按选项索引的真实成本与收益报告为唯一理由。

L257  limits := fun _ => True

此例使用不受限世界范围；起点假设与理由内容仍约束程序。

L258  relevantCriticism := fun w => w = false

把实际选择关闭的世界标记为相关批评情况。

L259  response := fun w => if w then some "benefit exceeds cost within budget" else some "reconsider if the budget no longer permits this cost"

给两个世界提供不同非空信息，包括在批评情况下重新考虑预算。

L260theorem switchValueProcedure : ValueProcedure switchPosition := by

陈述经检查的结果 switchValueProcedure。提供一致采纳见证，由实际成本收益理由得到目标与约束，并检查两个布尔情形的响应。 后续策略块证明这一显式类型。

L261  refine ⟨by simp [switchPosition], ?_, ?_, ?_⟩

拆分 switchPosition 的理由非空、共同采纳见证、全部理由支持后果，以及回应批评的义务。

L262  · refine ⟨true, (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

选择世界 true，满足起点选择、不受限限度与采纳选项，留下实际理由待检查。

L263    intro reason hr

任取 switchPosition 列表中的理由；下一步将在采纳的开启见证处确定其真实 optionReport 内容。

L264    have hr' : reason = (fun (_ : Bool) (option : Bool) => optionReport option) := List.mem_singleton.mp hr

单元素成员关系把任意理由确定为针对该立场采纳选项的 optionReport；代入这一实际理由。

L265    subst reason

单元素成员关系把任意理由确定为针对该立场采纳选项的 optionReport；代入这一实际理由。

L266    exact ⟨by decide, rfl⟩

检查采纳的开启选项满足已记录成本界限与所述收益值。

L267  · intro w _ _ allReasons

对处于所述起点与限度条件的任意世界，假定全部有效理由合取。

L268    have evidence := allReasons (fun (_ : Bool) (option : Bool) => optionReport option) (List.mem_singleton.mpr rfl)

从理由合取提取实际 optionReport 理由，而不是引入独立支持标签。

L269    change optionReport true at evidence

展开被采纳的选项：该证据针对开启选项。

L270    have benefitAboveBudget : 3 < optionBenefit true := by rw [evidence.2]; decide

利用已报告收益等式证明开启选项收益大于 3。

L271    exact ⟨Nat.lt_of_le_of_lt evidence.1 benefitAboveBudget, evidence.1⟩

组合成本至多为 3 与收益大于 3，证明成本小于收益，并保留同一成本界限作为约束。

L272  · intro w _ _; cases w <;> simp [switchPosition]

检查两个布尔世界，在需要回应批评时提供已记录的非空回应。

L273/- Adopting the other option updates the adopted starting state too, so rejection cannot be blamed on an inconsistent start. -/

说明 oppositePosition 的预定范围。对应声明涉及：把采纳选项改为false并更新起点选择，保留同一结果模型和目标。 该注释用于解释，不是证明前提。

L274def oppositePosition : ValuePosition Bool :=

定义 oppositePosition。把采纳选项改为false并更新起点选择，保留同一结果模型和目标。

L275  { switchPosition with adopted := false, starting := singleton (fun w => w = false) }

把采纳选项与起点选择都改为关闭，同时保留真实后果与理由解释。

L276/- The alternative has a joint adoption witness but its actual zero benefit/cost fails the adopted strict-benefit objective. -/

说明 oppositePositionRejected 的预定范围。对应声明涉及：false可被联合采纳，但不满足原成本小于收益目标，故程序检查拒绝。 该注释用于解释，不是证明前提。

L277theorem oppositePositionRejected : JointAdoption oppositePosition ∧ ¬ ValueProcedure oppositePosition := by

陈述经检查的结果 oppositePositionRejected。false可被联合采纳，但不满足原成本小于收益目标，故程序检查拒绝。 后续策略块证明这一显式类型。

L278  have witness : JointAdoption oppositePosition := by

在世界 false 为相反的关闭立场构造真实共同采纳见证；后续拒绝因此不依赖空域。

L279    refine ⟨false, (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

在世界 false 为相反的关闭立场构造真实共同采纳见证；后续拒绝因此不依赖空域。

L280    intro reason hr

在相反立场的 false 世界见证处任取列出理由，再检查关闭选项真实报告。

L281    have hr' : reason = (fun (_ : Bool) (option : Bool) => optionReport option) := List.mem_singleton.mp hr

单元素成员关系把任意理由确定为针对该立场采纳选项的 optionReport；代入这一实际理由。

L282    subst reason

单元素成员关系把任意理由确定为针对该立场采纳选项的 optionReport；代入这一实际理由。

L283    exact ⟨by decide, rfl⟩

关闭选项自身的报告为真：零成本满足界限，零收益符合所述报告。

L284  refine ⟨witness, ?_⟩

保留非空共同见证，另行否定相反价值程序的履行。

L285  intro h

假定相反关闭立场满足完整 ValueProcedure，以从零收益后果导出矛盾。

L286  have allReasons : ∀ reason, reason ∈ oppositePosition.reasons → reason false oppositePosition.adopted := by

在应用后果要求之前，先在相反立场的实际 false 世界见证处组合其全部理由。

L287    intro reason hr

任取相反立场真实理由，在其非空 false 世界反例处组合全部理由。

L288    have hr' : reason = (fun (_ : Bool) (option : Bool) => optionReport option) := List.mem_singleton.mp hr

单元素成员关系把任意理由确定为针对该立场采纳选项的 optionReport；代入这一实际理由。

L289    subst reason

单元素成员关系把任意理由确定为针对该立场采纳选项的 optionReport；代入这一实际理由。

L290    exact ⟨by decide, rfl⟩

关闭选项自身的报告为真：零成本满足界限，零收益符合所述报告。

L291  have bad := h.2.2.1 false ((modelsSingleton _ _).2 rfl) trivial allReasons

将假定的相反程序之联合理由后果条款，应用于同一起点与限度见证及其全部真实理由。

L292  exact Nat.lt_irrefl 0 bad.1

其假定目标要求关闭选项零成本严格小于零收益，与严格小于的非自反性矛盾。

L293/- Contradictory starting assumptions and an impossible selected/adopted equality are separate inadmissible variants. -/

说明 contradictoryStartingPosition 的预定范围。对应声明涉及：把起点换为恒假单项理论，使联合采纳见证不存在。 该注释用于解释，不是证明前提。

L294def contradictoryStartingPosition : ValuePosition Bool :=

定义 contradictoryStartingPosition。把起点换为恒假单项理论，使联合采纳见证不存在。

L295  { switchPosition with starting := singleton (fun _ => False) }

把起点理论替换为不可能的单元素主张 False。

L296def impossibleAdoptionPosition : ValuePosition Bool :=

定义 impossibleAdoptionPosition。始终选择false却仍采纳true，使联合采纳不可能。

L297  { switchPosition with selected := fun _ => false }

保留采纳的开启选项，却使所有实际选择为关闭，因此无法共同采纳。

L298/- The common-world witness rejects both contradiction and an impossible commitment instead of proving them vacuously. -/

说明 inadmissibleValuePositionsRejected 的预定范围。对应声明涉及：通过必需的联合见证分别拒绝不一致起点和不可能采纳。 该注释用于解释，不是证明前提。

L299theorem inadmissibleValuePositionsRejected :

陈述经检查的结果 inadmissibleValuePositionsRejected。通过必需的联合见证分别拒绝不一致起点和不可能采纳。

L300    ¬ ValueProcedure contradictoryStartingPosition ∧ ¬ ValueProcedure impossibleAdoptionPosition := by

分别否定矛盾起点假设与不可能实际采纳的程序。

L301  constructor

分开矛盾起点理论与不可能选择、采纳组合两个拒绝证明。

L302  · intro h; obtain ⟨w,hw,_,_,_⟩ := h.2.1

从假定满足程序的矛盾起点立场中提取共同采纳见证。

L303    exact (modelsSingleton _ _).1 hw

单元素起点理论在该见证处要求 False，直接否定其模型证明。

L304  · intro h; obtain ⟨w,_,_,hw,_⟩ := h.2.1

从假定的共同见证中提取无法实现的实际选择与采纳组合之间的相等关系。

L305    cases hw

所需采纳等式令不同布尔选项相等，因此该见证不存在。

L306/- Removing the reasons leaves only a position and assertion, which fails this value procedure. -/

说明 unsupportedPosition 的预定范围。对应声明涉及：复制实际价值立场但删除理由，使非空理由要求失败。 该注释用于解释，不是证明前提。

L307def unsupportedPosition : ValuePosition Bool := { switchPosition with reasons := [] }

定义 unsupportedPosition。复制实际价值立场但删除理由，使非空理由要求失败。

L308def switchEmpirical : Facet Bool :=

定义 switchEmpirical。以switch观察支持世界为真，范围和不确定性谓词均为真。

L309  .empirical [switchRecord] (fun _ => True) (fun w => w = true) (fun _ => True)

使用真实开关观测、不受限范围与同一已开启主张；不确定性明确为 True。

L310theorem switchEmpiricalDischarged : FacetDischarged switchEmpirical := by

陈述经检查的结果 switchEmpiricalDischarged。给true兼容见证、实际支持及平凡不确定性，完成经验检查。 后续策略块证明这一显式类型。

L311  refine ⟨⟨true, (switchCompatible true).2 rfl, trivial⟩, ?_, ?_⟩

用 true 作为与开关记录和不受限经验范围相容的非空世界。

L312  · intro w hw _; exact switchSupported w hw

同一开关记录的语义支持，在每个相容世界证明范围内的开关主张。

L313  · intro w _; trivial

履行明确为真的不确定性谓词，不增加经验置信度主张。

L314/- A mixed empirical/value position has actual empirical evidence but still lacks its value-reason duty. -/

说明 mixedMissingResponsibility 的预定范围。对应声明涉及：经验面向通过，但同一主张的价值面缺理由，故混合义务整体失败。 该注释用于解释，不是证明前提。

L315theorem mixedMissingResponsibility :

陈述经检查的结果 mixedMissingResponsibility。经验面向通过，但同一主张的价值面缺理由，故混合义务整体失败。

L316    FacetDischarged switchEmpirical ∧

保留真实经验开关方面的成功履行。

L317    ¬ LabeledDuties [] (fun f : Facet Bool => f = switchEmpirical ∨ f = .value unsupportedPosition) := by

即使标签为空也否定全部混合责任，因为真实价值方面同样适用，却缺少已记录理由。

L318  refine ⟨switchEmpiricalDischarged, ?_⟩

保留有效的经验开关方面，另行否定全部混合责任已经履行。

L319  intro h

假定每个实际混合方面均已履行，包括已记录理由列表为空的价值方面。

L320  have bad := (h (.value unsupportedPosition) (Or.inr rfl)).1

从实际适用并集中选取价值方面，并提取理由列表必须非空的条件。

L321  exact bad rfl

该理由列表依定义为空，因此否定的是这一已记录程序要求。

L322/- A fully identified argument may still fail to entail the stated conclusion. -/

说明 uninformativeArgument 的预定范围。对应声明涉及：构造有概念、有恒真理由却无实质假设的表达。 该注释用于解释，不是证明前提。

L323def uninformativeArgument : Articulation Bool :=

定义 uninformativeArgument。构造有概念、有恒真理由却无实质假设的表达。

L324  ⟨["switch state"], emptyTheory, [fun _ => True], fun _ => True⟩

用空假设与 True 理由表述开关概念；这些非空文字不约束开关世界。

L325theorem articulationNotSupport : Articulated uninformativeArgument ∧

陈述经检查的结果 articulationNotSupport。表达非空不代表其空假设蕴涵世界为真。

L326    ¬ Entails uninformativeArgument.assumptions (fun w : Bool => w = true) := by

无信息表述的真实假设不蕴含世界为 true。

L327  exact ⟨⟨by simp [uninformativeArgument], by simp [uninformativeArgument]⟩,

把非空却无信息的概念与理由，和空理论已证的不能蕴含开关主张组合。

L328    consistentIncomplete.2.1⟩

把非空却无信息的概念与理由，和空理论已证的不能蕴含开关主张组合。

L329/- Identifiable but unrelated argument fields cannot replace the actual observation grounds under the connected adapter. -/

说明 unrelatedArticulationRejected 的预定范围。对应声明涉及：虽表达非空且经验面向通过，两者的假设不匹配，不能视为同一根据表达。 该注释用于解释，不是证明前提。

L330theorem unrelatedArticulationRejected :

陈述经检查的结果 unrelatedArticulationRejected。虽表达非空且经验面向通过，两者的假设不匹配，不能视为同一根据表达。

L331    Articulated uninformativeArgument ∧ FacetDischarged switchEmpirical ∧

保留无关表述的程序存在性及开关方面的真实履行。

L332    ¬ FacetArticulated uninformativeArgument switchEmpirical := by

仍否定该无关表述与这一经验方面的语义匹配。

L333  refine ⟨articulationNotSupport.1, switchEmpiricalDischarged, ?_⟩

保留表述与有效开关证据，再单独检验这一无关表述是否真正匹配该方面。

L334  intro h

假定无信息表述尽管前提理论为空，仍与 switchEmpirical 语义匹配。

L335  have relation := congrFun h.1 (Compatible [switchRecord])

在相容性主张自身处，计算假定的表述假设与经验相容性假设相等。

L336  have bad : False := relation.mpr rfl

经验单元素理论包含该相容性主张，而无关空理论不包含；假定的相等推出 False。

L337  exact bad

使用所示局部证据或已证引理完成 unrelatedArticulationRejected 的这一组件；该组件属于下列固定结果：虽表达非空且经验面向通过，两者的假设不匹配，不能视为同一根据表达。

L338/- Repetition of the same unrelated temperature observation leaves the switch state undetermined. -/

说明 temperatureRecord 的预定范围。对应声明涉及：只观测布尔对第一坐标，未观测第二坐标。 该注释用于解释，不是证明前提。

L339def temperatureRecord : Record (Bool × Bool) := ⟨Prod.fst, true⟩

定义 temperatureRecord。只观测布尔对第一坐标，未观测第二坐标。

L340theorem temperatureCompatible (b : Bool) :

陈述经检查的结果 temperatureCompatible。复制第一坐标记录仍允许第二坐标为任意布尔值。

L341    Compatible [temperatureRecord, temperatureRecord] (true,b) := by

对任意输出坐标 b，重复温度记录仍与 (true,b) 相容。

L342  intro r hr

对任意输出坐标 b，重复列表的成员关系仍选取同一温度测试；其观测的第一坐标为 true，而 b 不受约束。

L343  simp at hr

对任意输出坐标 b，重复列表的成员关系仍选取同一温度测试；其观测的第一坐标为 true，而 b 不受约束。

L344  cases hr

对任意输出坐标 b，重复列表的成员关系仍选取同一温度测试；其观测的第一坐标为 true，而 b 不受约束。

L345  rfl

对任意输出坐标 b，重复列表的成员关系仍选取同一温度测试；其观测的第一坐标为 true，而 b 不受约束。

L346/- The world identifies a selected action and its budget; the action costs three units. -/

说明 BudgetWorld 的预定范围。对应声明涉及：世界由行动布尔值和自然数预算组成。 该注释用于解释，不是证明前提。

L347abbrev BudgetWorld := Bool × Nat

引入类型缩写 BudgetWorld。世界由行动布尔值和自然数预算组成。

L348/- A real issued announcement asserts the selected action, but says nothing about affordability. -/

说明 announcement 的预定范围。对应声明涉及：定义固定行动宣告字符串，字符串自身不提供预算依据。 该注释用于解释，不是证明前提。

L349def announcement : String := "activate"

定义 announcement。定义固定行动宣告字符串，字符串自身不提供预算依据。

L350def announcementPosition : ValuePosition BudgetWorld where

定义 announcementPosition。仅用行动自述作为选项理由，却要求实际成本收益及可用预算。

L351  Position := Bool

使用布尔选项表示开启与关闭。

L352  Outcome := Nat × Nat

以自然数对表示各后果的真实收益与成本。

L353  adopted := true

明确采纳开启选项；采纳本身不是从算术推导的。

L354  selected := Prod.fst

从第一坐标读取实际选择，同时让预算独立变化。

L355  outcome := fun _ option => (optionBenefit option, optionCost option)

从同一真实选项计算收益与成本。

L356  objective := fun result => result.2 < result.1

采纳真实收益严格超过真实成本这一目标。

L357  constraints := fun w option => optionCost option ≤ w.2

比较采纳选项真实成本与该世界独立给定的预算。

L358  starting := singleton (fun w => w.1 = true)

固定选择为开启，不增加可负担性或预算假设。

L359  reasons := [fun _ option => announcement = (if option then "activate" else "disable")]

使用真实按选项区分的公告文本作为理由；它不说明可用预算。

L360  limits := fun _ => True

此例使用不受限世界范围；起点假设与理由内容仍约束程序。

L361  relevantCriticism := fun w => w.2 < 3

把预算低于 3 认定为对该成本为 3 行动的相关批评。

L362  response := fun _ => some "reconsider the action when its cost exceeds budget"

记录成本超预算时重新考虑行动的非空信息。

L363/- The zero-budget counterworld satisfies the stated starts, adoption and all announced reasons jointly. -/

说明 announcementHasJointAdoption 的预定范围。对应声明涉及：构造行动为真、预算零且自述理由成立的世界；后续失败不是缺少采纳见证。 该注释用于解释，不是证明前提。

L364theorem announcementHasJointAdoption : JointAdoption announcementPosition := by

陈述经检查的结果 announcementHasJointAdoption。构造行动为真、预算零且自述理由成立的世界；后续失败不是缺少采纳见证。 后续策略块证明这一显式类型。

L365  refine ⟨(true,0), (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

选择已开启且预算为 0 的世界作为共同采纳见证；起点理论固定选择，却不假定可负担性。

L366  intro reason hr

在已开启且零预算的共同见证处任取公告理由。

L367  have hr' : reason = (fun (_ : BudgetWorld) (option : Bool) => announcement = (if option then "activate" else "disable")) :=

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L368    List.mem_singleton.mp hr

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L369  subst reason

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L370  rfl

实际公告等于开启选项的启动文本；这证明公告理由成立，不证明预算约束。

L371/- A nonempty announcement remains true in a jointly admissible zero-budget world but cannot support the action's affordability. -/

说明 announcementNotBudgetReason 的预定范围。对应声明涉及：预算零时，已采纳行动及非空真自述仍不能满足预算后果，故程序不成立。 该注释用于解释，不是证明前提。

L372theorem announcementNotBudgetReason :

陈述经检查的结果 announcementNotBudgetReason。预算零时，已采纳行动及非空真自述仍不能满足预算后果，故程序不成立。

L373    announcementPosition.reasons ≠ [] ∧ announcementPosition.commitment (true,0) ∧

要求公告理由非空，并在已开启且预算 0 处实际采纳。

L374    (∀ reason, reason ∈ announcementPosition.reasons → reason (true,0) announcementPosition.adopted) ∧

在同一零预算世界，全部真实公告理由成立。

L375    ¬ announcementPosition.consequence (true,0) ∧ ¬ ValueProcedure announcementPosition := by

仍否定真实后果及整个价值程序。

L376  refine ⟨by simp [announcementPosition], rfl, ?_, (by intro h; cases h.2), ?_⟩

组合非空公告理由与真实公告，否定零预算后果，留下整个程序失败的证明。

L377  · intro reason hr

为预算 0 处的理由合取，任取真实公告理由列表成员。

L378    have hr' : reason = (fun (_ : BudgetWorld) (option : Bool) => announcement = (if option then "activate" else "disable")) := List.mem_singleton.mp hr

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L379    subst reason

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L380    rfl

实际公告等于开启选项的启动文本；这证明公告理由成立，不证明预算约束。

L381  · intro h

假定公告立场满足 ValueProcedure，以在预算 0 处检验其后果条款。

L382    have allReasons : ∀ reason, reason ∈ announcementPosition.reasons → reason (true,0) announcementPosition.adopted := by

在同一已开启且预算为零的世界收集全部公告理由。

L383      intro reason hr

为该条款提供全部理由，在同一零预算世界任取公告理由。

L384      have hr' : reason = (fun (_ : BudgetWorld) (option : Bool) => announcement = (if option then "activate" else "disable")) := List.mem_singleton.mp hr

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L385      subst reason

根据成员关系，把实际理由确定为按选项索引的公告文本，再特化到采纳的开启选项。

L386      rfl

实际公告等于开启选项的启动文本；这证明公告理由成立，不证明预算约束。

L387    have bad := h.2.2.1 (true,0) ((modelsSingleton _ _).2 rfl) trivial allReasons

把假定程序应用于这一非空的零预算起点、限度实例及其真实公告理由。

L388    cases bad.2

所得成本约束要求成本 3 不超过预算 0，这是不可能的。

L389/- A repeated actual selection observation contains no budget information. -/

说明 actionRecord 的预定范围。对应声明涉及：只观测行动布尔值，不限制预算。 该注释用于解释，不是证明前提。

L390def actionRecord : Record BudgetWorld := ⟨Prod.fst, true⟩

定义 actionRecord。只观测行动布尔值，不限制预算。

L391theorem actionCompatible (budget : Nat) : Compatible [actionRecord, actionRecord] (true,budget) := by

陈述经检查的结果 actionCompatible。两个重复行动记录仍与任意预算相容。 后续策略块证明这一显式类型。

L392  intro r hr; simp at hr; cases hr; rfl

重复列表中的每条行动记录只测试实际已开启坐标，因此任意给定预算仍相容。

L393/- Single and repeated irrelevant observations cannot establish the other outcome or the same action's budget adequacy. -/

说明 measurementRepeatNotSupport 的预定范围。对应声明涉及：用未观测坐标和预算零反例，分别拒绝单次及重复测量对无关结论和价值后果的支持。 该注释用于解释，不是证明前提。

L394theorem measurementRepeatNotSupport :

陈述经检查的结果 measurementRepeatNotSupport。用未观测坐标和预算零反例，分别拒绝单次及重复测量对无关结论和价值后果的支持。

L395    temperatureRecord.test (true,false) = true ∧

即使独立输出坐标为 false，真实温度测试仍返回 true。

L396    Compatible [temperatureRecord,temperatureRecord] (true,false) ∧

在重复温度观测下保留该假输出世界。

L397    Compatible [temperatureRecord,temperatureRecord] (true,true) ∧

在相同重复观测下也保留真输出世界。

L398    ¬ Supports [temperatureRecord] (fun w : Bool × Bool => w.2 = true) ∧

单条温度记录不支持另一输出为 true。

L399    ¬ Supports [temperatureRecord,temperatureRecord] (fun w : Bool × Bool => w.2 = true) ∧

重复该温度记录仍不支持另一输出为 true。

L400    Compatible [actionRecord,actionRecord] (true,0) ∧

重复观测到启动与已开启、预算为 0 相容。

L401    Compatible [actionRecord,actionRecord] (true,3) ∧

相同重复记录也与预算为 3 相容。

L402    ¬ Supports [actionRecord] announcementPosition.consequence ∧

单条启动记录不支持该选项的真实目标与预算后果。

L403    ¬ Supports [actionRecord,actionRecord] announcementPosition.consequence ∧

重复启动记录不能修复这一后果支持缺失。

L404    ¬ ValueProcedure announcementPosition := by

基于公告的价值程序也未满足同一实际选项与约束。

L405  refine ⟨rfl, temperatureCompatible false, temperatureCompatible true, ?_, ?_,

记录观测真实值为 true，以及两个温度相容的输出选择，留下输出主张不获支持的反证。

L406    actionCompatible 0, actionCompatible 3, ?_, ?_, announcementNotBudgetReason.2.2.2.2⟩

保留预算 0 与预算 3 两个行动相容世界及已证的公告程序失败，留下可负担性支持主张的反证。

L407  · intro h

假定单次温度观测支持独立表示的第二输出为 true。

L408    have bad := h (true,false) (by intro r hr; simp only [List.mem_singleton] at hr; cases hr; rfl)

将假定的单记录输出支持应用于 (true,false)：其温度观测为真，另一输出主张却为假。

L409    cases bad

将假定的单记录输出支持应用于 (true,false)：其温度观测为真，另一输出主张却为假。

L410  · intro h; have bad := h (true,false) (temperatureCompatible false); cases bad

同一 (true,false) 反世界仍与重复温度记录相容，因此否定重复数据支持输出的主张。

L411  · intro h

假定单次行动观测支持采纳选项的收益与预算后果。

L412    have bad := h (true,0) (by intro r hr; simp only [List.mem_singleton] at hr; cases hr; rfl)

单次观测到启动与预算 0 相容；假定支持该处后果会迫使不可能的成本约束。

L413    cases bad.2

单次观测到启动与预算 0 相容；假定支持该处后果会迫使不可能的成本约束。

L414  · intro h; have bad := h (true,0) (actionCompatible 0); cases bad.2

重复启动记录仍保留同一零预算反世界，因此仍不支持实际可负担后果。

L415/- Missing reason records fail a procedure; independently, a present announcement fails the explicit budget-support criterion. -/

说明 selfAssertionNotReason 的预定范围。对应声明涉及：组合无理由与非空但无预算依据的自断言反例，并为后者提供联合采纳见证。 该注释用于解释，不是证明前提。

L416theorem selfAssertionNotReason :

陈述经检查的结果 selfAssertionNotReason。组合无理由与非空但无预算依据的自断言反例，并为后者提供联合采纳见证。

L417    (unsupportedPosition.commitment true ∧ ¬ ValueProcedure unsupportedPosition) ∧

缺少理由的立场可以被实际采纳，却未通过其记录程序。

L418    (announcementPosition.reasons ≠ [] ∧ announcementPosition.commitment (true,0) ∧

更强的公告实例具有非空理由，并在预算 0 处实际采纳。

L419      ¬ announcementPosition.consequence (true,0) ∧ ¬ ValueProcedure announcementPosition) ∧

其真实后果及程序仍失败，因为同一采纳选项超出预算。

L420    JointAdoption announcementPosition :=

保留真实共同采纳见证，排除以空起点域解释此失败。

L421  ⟨⟨rfl, fun h => h.1 rfl⟩,

按定义证明 unsupportedPosition.commitment true；若假定存在 ValueProcedure，则其理由非空要求与实际空理由列表矛盾。

L422    ⟨announcementNotBudgetReason.1, announcementNotBudgetReason.2.1,

复用 announcementNotBudgetReason 中非空真实公告理由与采纳等式。

L423      announcementNotBudgetReason.2.2.2.1, announcementNotBudgetReason.2.2.2.2⟩,

还复用同一零预算后果及整个公告程序的失败。

L424    announcementHasJointAdoption⟩

保留 announcementHasJointAdoption，因此该失败不能由空或不一致起点域解释。

L425/- The value procedure is satisfiable although the adopted starting commitment is not entailed by empty facts. -/

说明 valueWithoutSelfProof 的预定范围。对应声明涉及：给出有理由且一致、却不能由空假设推出的立场，并拒绝相反选项、不一致起点和不可能采纳变体。 该注释用于解释，不是证明前提。

L426theorem valueWithoutSelfProof : ValueProcedure switchPosition ∧

陈述经检查的结果 valueWithoutSelfProof。给出有理由且一致、却不能由空假设推出的立场，并拒绝相反选项、不一致起点和不可能采纳变体。

L427    Satisfiable switchPosition.starting ∧

要求开关立场的真实起点理论具有模型。

L428    ¬ Entails (emptyTheory : Theory Bool) switchPosition.commitment ∧

否定从空布尔理论推导其采纳承诺。

L429    (JointAdoption oppositePosition ∧ ¬ ValueProcedure oppositePosition) ∧

相反立场具有共同见证，却未通过后果评估。

L430    (¬ ValueProcedure contradictoryStartingPosition ∧ ¬ ValueProcedure impossibleAdoptionPosition) :=

还拒绝矛盾起点与无法采纳的变体，区分未由自身推得与不一致起点。

L431  ⟨switchValueProcedure, ⟨true, (modelsSingleton _ _).2 rfl⟩, consistentIncomplete.2.1,

组合真实开关程序、作为起点模型的 true 世界，以及采纳主张不由 emptyTheory 蕴含。

L432    oppositePositionRejected, inadmissibleValuePositionsRejected⟩

加入非空相反选项的拒绝，以及矛盾起点与无法采纳两个单独变体。

L433/- The world records the selected option and its actual benefit/cost outcomes. -/

说明 BenefitCostWorld 的预定范围。对应声明涉及：世界保存所选布尔选项及可变收益和成本。 该注释用于解释，不是证明前提。

L434abbrev BenefitCostWorld := Bool × (Nat × Nat)

引入类型缩写 BenefitCostWorld。世界保存所选布尔选项及可变收益和成本。

L435def measuredOutcome (world : BenefitCostWorld) (option : Bool) : Nat × Nat :=

定义 measuredOutcome。true选项返回世界的收益成本对，false结果为零与零。

L436  if option then world.2 else (0,0)

开启选项读取世界真实收益与成本对；关闭选项得到 (0,0)。

L437def benefitReason (world : BenefitCostWorld) (option : Bool) : Prop :=

定义 benefitReason。要求同一选项测得收益为四。

L438  (measuredOutcome world option).1 = 4

收益理由要求实际选项的测得收益等于 4。

L439def costReason (world : BenefitCostWorld) (option : Bool) : Prop :=

定义 costReason。要求该选项测得成本至多三。

L440  (measuredOutcome world option).2 ≤ 3

成本理由要求同一选项的测得成本至多为 3。

L441/- Neither recorded benefit nor recorded cost alone establishes the selected option's joint consequence. -/

说明 jointReasonPosition 的预定范围。对应声明涉及：用相互独立的选项收益与成本理由，共同支持采纳选项目标及预算。 该注释用于解释，不是证明前提。

L442def jointReasonPosition : ValuePosition BenefitCostWorld where

定义 jointReasonPosition。用相互独立的选项收益与成本理由，共同支持采纳选项目标及预算。

L443  Position := Bool

使用布尔选项表示开启与关闭。

L444  Outcome := Nat × Nat

以自然数对表示各后果的真实收益与成本。

L445  adopted := true

明确采纳开启选项；采纳本身不是从算术推导的。

L446  selected := Prod.fst

从世界第一坐标读取选择，与测得收益及成本分开。

L447  outcome := measuredOutcome

使用 measuredOutcome，使受评选项的真实收益与成本来自该世界。

L448  objective := fun result => result.2 < result.1

采纳真实收益严格超过真实成本这一目标。

L449  constraints := fun world option => (measuredOutcome world option).2 ≤ 3

要求该选项测得成本至多为 3。

L450  starting := singleton (fun world => world.1 = true)

假定所选选项为开启，不假定收益或成本结论。

L451  reasons := [benefitReason, costReason]

同时列出 benefitReason 与 costReason；程序将使用其合取。

L452  limits := fun _ => True

此例使用不受限世界范围；起点假设与理由内容仍约束程序。

L453  relevantCriticism := fun world => 3 < world.2.2

把真实测得成本大于 3 识别为相关批评。

L454  response := fun _ => some "reassess the option when its cost exceeds the budget"

记录当该选项真实成本超预算时重新评估它的非空回应。

L455/- These two content constraints jointly establish the consequence in a nonempty adopted world. -/

说明 jointReasonProcedure 的预定范围。对应声明涉及：以收益四成本三构造联合见证，合用两个理由证明成本低于收益且不超预算。 该注释用于解释，不是证明前提。

L456theorem jointReasonProcedure : ValueProcedure jointReasonPosition := by

陈述经检查的结果 jointReasonProcedure。以收益四成本三构造联合见证，合用两个理由证明成本低于收益且不超预算。 后续策略块证明这一显式类型。

L457  refine ⟨by simp [jointReasonPosition], ?_, ?_, ?_⟩

拆分联合理由立场的理由非空、共同见证、基于合取的后果与批评回应。

L458  · refine ⟨(true,(4,3)), (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

用已开启、收益为 4、成本为 3 的世界作为共同的起点、限度与采纳见证。

L459    intro reason hr

在真实 (true,(4,3)) 见证处任取两条理由之一，再拆分成员关系检查各不同理由。

L460    change reason ∈ [benefitReason,costReason] at hr

展开实际的双元素理由列表：benefitReason 与 costReason。

L461    rcases List.mem_cons.mp hr with hr | hr

把理由成员关系分为收益理由，或剩余单元素成本理由。

L462    · subst reason; rfl

代入收益理由，检查见证的测得收益恰为 4。

L463    · have hr' := List.mem_singleton.mp hr

把剩余理由确定为 costReason 并代入。

L464      subst reason

把剩余理由确定为 costReason 并代入。

L465      change 3 ≤ 3; exact Nat.le_refl 3

利用自然数序的自反性检查见证的成本界限 3 ≤ 3。

L466  · intro world _ _ reasons

对任意被接纳世界，假定全部有效理由共同成立，而不要求任一理由单独充分。

L467    have benefit := reasons benefitReason (by change benefitReason ∈ [benefitReason,costReason]; simp)

在该世界与采纳选项处，从理由合取提取实际 benefitReason。

L468    have cost := reasons costReason (by change costReason ∈ [benefitReason,costReason]; simp)

在同一世界与选项处，从同一合取提取 costReason。

L469    change (measuredOutcome world true).1 = 4 at benefit

展开 benefitReason：采纳的开启选项之测得收益等于 4。

L470    change (measuredOutcome world true).2 ≤ 3 at cost

展开 costReason：同一选项的测得成本至多为 3。

L471    refine ⟨?_, cost⟩

保留实际成本约束，只留下收益严格大于成本的目标。

L472    have bigger : 3 < (measuredOutcome world true).1 := by rw [benefit]; decide

把测得收益改写为 4，并检查它大于 3。

L473    exact Nat.lt_of_le_of_lt cost bigger

合成成本至多为 3 与 3 小于收益，使用两个理由确立成本小于收益。

L474  · intro world _ _

对限度内且批评相关的世界，构造针对该选项成本过高的必需回应。

L475    exact ⟨"reassess the option when its cost exceeds the budget", rfl, by decide⟩

提供关于成本超预算时重新评估选项的明确非空回应；这登记回应，不证明其说服充分性。

L476/- Each separate reason has a concrete same-start/limit/adoption counterworld; their conjunction is sufficient. -/

说明 JointReasonsExample 的预定范围。对应声明涉及：表示联合理由程序通过，但任一单独理由都可在后果失败的世界成立。 该注释用于解释，不是证明前提。

L477def JointReasonsExample : Prop :=

定义 JointReasonsExample。表示联合理由程序通过，但任一单独理由都可在后果失败的世界成立。

L478  ValueProcedure jointReasonPosition ∧

要求双理由立场满足完整 ValueProcedure。

L479  (Models jointReasonPosition.starting (true,(4,5)) ∧ jointReasonPosition.limits (true,(4,5)) ∧

固定仅满足收益理由的反世界 (true,(4,5))，它满足同一起点假设与限度。

L480    jointReasonPosition.commitment (true,(4,5)) ∧ benefitReason (true,(4,5)) true ∧

在该世界，实际采纳与收益理由均成立。

L481    ¬ jointReasonPosition.consequence (true,(4,5))) ∧

否定该处受评后果，因为真实成本过高。

L482  (Models jointReasonPosition.starting (true,(0,3)) ∧ jointReasonPosition.limits (true,(0,3)) ∧

在同一起点假设与限度下固定仅满足成本理由的反世界 (true,(0,3))。

L483    jointReasonPosition.commitment (true,(0,3)) ∧ costReason (true,(0,3)) true ∧

在该世界，实际采纳与成本理由成立。

L484    ¬ jointReasonPosition.consequence (true,(0,3)))

否定其受评后果，因为零收益没有超过成本 3。

L485theorem jointReasonsExample : JointReasonsExample := by

陈述经检查的结果 jointReasonsExample。以收益四成本五及收益零成本三分别反驳单个理由充分。 后续策略块证明这一显式类型。

L486  refine ⟨jointReasonProcedure,

以已检查的双理由程序开始组合实例。

L487    ⟨(modelsSingleton _ _).2 rfl, trivial, rfl, rfl, ?_⟩,

提供仅满足收益理由的反世界：收益 4、成本 5，且满足相同起点、限度与采纳条件。

L488    ⟨(modelsSingleton _ _).2 rfl, trivial, rfl, Nat.le_refl 3, ?_⟩⟩

在相同条件下提供仅满足成本理由的反世界：收益 0、成本 3。

L489  · intro h; have bad : 5 ≤ 3 := h.2; omega

仅有收益理由的世界违反成本约束 5 ≤ 3；自然数算术消去该矛盾。

L490  · intro h; have bad : 3 < 0 := h.1; omega

仅有成本理由的世界不可能满足严格目标 3 < 0；算术完成该反例。

L491/- Empirical observations, semantic inference and criticism-responsive reasons coexist without a scalar score. -/

说明 heterogeneousReasons 的预定范围。对应声明涉及：组合经验、推论、价值实例，并加入任一理由单独不足的真实联合理由实例。 该注释用于解释，不是证明前提。

L492theorem heterogeneousReasons :

陈述经检查的结果 heterogeneousReasons。组合经验、推论、价值实例，并加入任一理由单独不足的真实联合理由实例。

L493    FacetDischarged switchEmpirical ∧

纳入真实已履行的经验开关方面。

L494    FacetDischarged (Facet.inferential (singleton (fun w : Bool => w = true)) (fun w => w = true)) ∧

纳入推论方面，其可满足的真世界前提蕴含同一真世界主张。

L495    FacetDischarged (Facet.value switchPosition) ∧ JointReasonsExample := by

在此登记定理中纳入真实开关价值程序与双理由共同支持实例。

L496  refine ⟨switchEmpiricalDischarged, ⟨⟨true, (modelsSingleton _ _).2 rfl⟩, ?_⟩, switchValueProcedure, jointReasonsExample⟩

组合已检查经验方面、非空推论单元素理论、价值程序及联合理由反例。

L497  intro w hw; exact (modelsSingleton (fun x : Bool => x = true) w).1 hw

对推论方面，其单元素前提在任意模型中直接给出同一真世界主张。

L499/- This local observation checks the actual output on input zero. -/

说明 zeroRecord 的预定范围。对应声明涉及：只测试布尔函数在自然数零处的输出。 该注释用于解释，不是证明前提。

L500def zeroRecord : Record (Nat → Bool) := ⟨fun f => f 0, true⟩

定义 zeroRecord。只测试布尔函数在自然数零处的输出。

L501def localGenerator (seed : Nat) : Nat → Bool := fun n => n == seed

定义 localGenerator。生成只在seed输入处返回真的布尔函数。

L502/- All outputs being true is a stronger, explicitly quantified capability claim. -/

说明 allTrue 的预定范围。对应声明涉及：要求函数在每个自然数输入都返回真。 该注释用于解释，不是证明前提。

L503def allTrue : Claim (Nat → Bool) := fun f => ∀ n, f n = true

定义 allTrue。要求函数在每个自然数输入都返回真。

L504theorem zeroCompatible (f : Nat → Bool) : Compatible [zeroRecord] f ↔ f 0 = true := by

陈述经检查的结果 zeroCompatible。证明零点记录的兼容性恰好只要求f(0)=true。 后续策略块证明这一显式类型。

L505  constructor

证明匹配 zeroRecord 与真实函数在输入 0 返回 true 之间的两个方向。

L506  · intro h; exact h zeroRecord (by simp)

把记录相容性应用于唯一指定测试，恢复其真实观测等式。

L507  · intro hf r hr; simp only [List.mem_singleton] at hr; cases hr; exact hf

反方向中，单元素成员关系把任意列出记录确定为该测试，其等式即为给定观测前提。

L508/- A generating subject owns an earlier predicate and a seed used to revise that actual predicate. -/

说明 GeneratingProcess 的预定范围。对应声明涉及：保存生产者身份、实际旧谓词及修订算法种子。 该注释用于解释，不是证明前提。

L509structure GeneratingProcess where

声明数据接口 GeneratingProcess。保存生产者身份、实际旧谓词及修订算法种子。

L510  owner : Nat

保存实际生成过程的所有者标识。

L511  prior : Nat → Bool

保存该过程生成修订之前的布尔值函数。

L512  generateSeed : Nat

保存该过程真实局部生成器使用的种子输入。

L513/- The revision preserves prior successes and adds the seed-selected case through the actual generator. -/

说明 GeneratingProcess.outputRevision 的预定范围。对应声明涉及：保留旧谓词成功输入，并由实际局部生成器增加种子输入。 该注释用于解释，不是证明前提。

L514def GeneratingProcess.outputRevision (process : GeneratingProcess) : Nat → Bool :=

定义 GeneratingProcess.outputRevision。保留旧谓词成功输入，并由实际局部生成器增加种子输入。

L515  fun input => process.prior input || localGenerator process.generateSeed input

修订函数保留每个原先为真的输出，或在实际生成种子输入处增加真值。

L516/- A produced revision retains its producer and exact old/new objects. -/

说明 ProducedRevision 的预定范围。对应声明涉及：保存生产者及精确旧新谓词对象。 该注释用于解释，不是证明前提。

L517structure ProducedRevision where

声明数据接口 ProducedRevision。保存生产者及精确旧新谓词对象。

L518  producer : Nat

标识哪个所有者生成了这一具体修订对象。

L519  before : Nat → Bool

保存修订的真实前函数。

L520  after : Nat → Bool

保存修订的真实后函数。

L521/- The subject itself constructs the owned before/after revision object. -/

说明 GeneratingProcess.produce 的预定范围。对应声明涉及：由该过程构造带自身主体及实际旧函数、输出函数的修订。 该注释用于解释，不是证明前提。

L522def GeneratingProcess.produce (process : GeneratingProcess) : ProducedRevision :=

定义 GeneratingProcess.produce。由该过程构造带自身主体及实际旧函数、输出函数的修订。

L523  ⟨process.owner, process.prior, process.outputRevision⟩

直接以该过程的所有者、原函数及计算所得输出修订构造修订对象。

L524def sampleGeneratingProcess : GeneratingProcess := ⟨17, fun _ => false, 0⟩

定义 sampleGeneratingProcess。以主体十七、恒假旧谓词及零种子构造实际生成过程。

L525/- This same-owner revision actually changes input zero, while its produced predicate still fails at input one. -/

说明 OwnedRevisionExample 的预定范围。对应声明涉及：把自身来源与精确旧新函数关联到零输入上的实际变化，而全局主张仍无支持。 该注释用于解释，不是证明前提。

L526def OwnedRevisionExample : Prop :=

定义 OwnedRevisionExample。把自身来源与精确旧新函数关联到零输入上的实际变化，而全局主张仍无支持。

L527  sampleGeneratingProcess.produce.producer = sampleGeneratingProcess.owner ∧

把修订生成者标识绑定到真实生成过程所有者。

L528  sampleGeneratingProcess.produce.before = sampleGeneratingProcess.prior ∧

把其前函数绑定到该过程的真实原函数。

L529  sampleGeneratingProcess.produce.after = sampleGeneratingProcess.outputRevision ∧

把其后函数绑定到该过程的真实 outputRevision。

L530  sampleGeneratingProcess.produce.before 0 = false ∧ sampleGeneratingProcess.produce.after 0 = true ∧

要求输入 0 处实际从此前 false 变为此后 true。

L531  sampleGeneratingProcess.produce.after 1 = false ∧

保留修订后输入 1 处真实为 false 的输出。

L532  Compatible [zeroRecord] sampleGeneratingProcess.produce.after ∧

实际生成的后函数匹配输入 0 观测。

L533  ¬ Supports [zeroRecord] allTrue

该记录仍不支持所有输入为真的主张。

L534/- Actual producer/old/new links and the compatible failing revision witness the insufficiency of self-origin. -/

说明 ownedRevisionExample 的预定范围。对应声明涉及：计算主体和对象联系，并用自产函数在一处失败反驳全称支持。 该注释用于解释，不是证明前提。

L535theorem ownedRevisionExample : OwnedRevisionExample := by

陈述经检查的结果 ownedRevisionExample。计算主体和对象联系，并用自产函数在一处失败反驳全称支持。 后续策略块证明这一显式类型。

L536  refine ⟨rfl,rfl,rfl,rfl,rfl,rfl,(zeroCompatible _).2 rfl, ?_⟩

通过计算检查生成者身份、旧对象与输出修订关系及真实样本值；保留零输入记录相容性，留下全称支持的反证。

L537  intro h

假定 zeroRecord 支持 allTrue，以该所有者实际生成的修订反驳它。

L538  have bad := h sampleGeneratingProcess.produce.after ((zeroCompatible _).2 rfl) 1

把假定支持应用于该所有者实际生成的后函数及输入 1；该修订在此仍返回 false。

L539  cases bad

消去所得 false=true 等式；实际修订构成证据相容反例。

L540/- The generator's own sample succeeds, but its generated revision has a concrete unsupported global claim. -/

说明 selfOriginDoesNotSupport 的预定范围。对应声明涉及：保留局部观察反模型，另加具有同一未获支持全局主张的真实自身旧新修订。 该注释用于解释，不是证明前提。

L541theorem selfOriginDoesNotSupport :

陈述经检查的结果 selfOriginDoesNotSupport。保留局部观察反模型，另加具有同一未获支持全局主张的真实自身旧新修订。

L542    localGenerator 0 0 = true ∧ localGenerator 0 1 = false ∧

计算 localGenerator 0 在 0 处为 true、在 1 处为 false。

L543    Compatible [zeroRecord] (localGenerator 0) ∧

要求该生成函数匹配同一输入 0 记录。

L544    ¬ Supports [zeroRecord] allTrue ∧ OwnedRevisionExample := by

陈述全域支持失败，并纳入具体所有者、原对象与修订关系实例。

L545  refine ⟨rfl, rfl, (zeroCompatible _).2 rfl, ?_, ownedRevisionExample⟩

计算生成函数在 0 与 1 的值，给出零输入记录相容性，并纳入自有修订关系实例。

L546  intro h

假定局部零输入观测蕴含每个相容函数的全部输入均输出 true。

L547  have bad := h (localGenerator 0) ((zeroCompatible _).2 rfl) 1

把假定全称支持实例化到 localGenerator 0，再取输入 1；零输入相容性并未约束这一失败输入。

L548  cases bad

消去所得 false=true 等式；实际修订构成证据相容反例。

L549/- A proper local observation allows both a universally successful and a failing extension. -/

说明 localNotUniversal 的预定范围。对应声明涉及：常真函数与零点真函数都符合局部记录，但只有前者全称成立，故局部记录不支持全称结论。 该注释用于解释，不是证明前提。

L550theorem localNotUniversal :

陈述经检查的结果 localNotUniversal。常真函数与零点真函数都符合局部记录，但只有前者全称成立，故局部记录不支持全称结论。

L551    (∃ outside : Nat, outside ≠ 0) ∧

要求至少存在一个自然数输入处于观测单元素范围之外。

L552    Compatible [zeroRecord] (fun _ => true) ∧

恒真函数匹配零输入观测。

L553    Compatible [zeroRecord] (localGenerator 0) ∧

局部生成器也匹配同一观测。

L554    allTrue (fun _ => true) ∧ ¬ allTrue (localGenerator 0) ∧

第一个函数全域为真，第二个却不是。

L555    ¬ Supports [zeroRecord] allTrue := by

因此共同观测不支持全域为真。

L556  refine ⟨⟨1, by decide⟩, (zeroCompatible _).2 rfl, (zeroCompatible _).2 rfl,

提供观测范围以外的输入，并证明恒真函数与局部生成器都满足同一零输入观测。

L557    (fun _ => rfl), ?_, selfOriginDoesNotSupport.2.2.2.1⟩

恒真函数全域为真；保留已知支持反例，留下局部生成器全称主张的反证。

L558  intro h; have bad := h 1; cases bad

在输入 1 检验局部生成器的假定全域真值，而其实际结果为 false。

L559/- Two implementations agree on the actual observed input and differ on a specified relevant omitted input. -/

说明 hiddenDifference 的预定范围。对应声明涉及：两函数在零点范围相同，却在一处不同，说明排除范围不能否认相关差异。 该注释用于解释，不是证明前提。

L560theorem hiddenDifference :

陈述经检查的结果 hiddenDifference。两函数在零点范围相同，却在一处不同，说明排除范围不能否认相关差异。

L561    (∀ n : Nat, n = 0 → (fun _ : Nat => true) n = localGenerator 0 n) ∧

只对满足 n=0 的输入陈述两个函数相等。

L562    (fun _ : Nat => true) 1 ≠ localGenerator 0 1 := by

陈述它们在输入 1 处真实输出不等。

L563  refine ⟨?_, by decide⟩

分开输入 0 范围内一致与输入 1 处真实输出不同两个结论。

L564  intro n hn; cases hn; rfl

根据范围前提代入 n=0；两个函数都计算为 true。

L565/- One observation supplies only its actual input-specific consequence, without repetition. -/

说明 singleObservation 的预定范围。对应声明涉及：单条记录有兼容见证并支持局部结果，但不支持全输入结论。 该注释用于解释，不是证明前提。

L566theorem singleObservation : [zeroRecord].length = 1 ∧

陈述经检查的结果 singleObservation。单条记录有兼容见证并支持局部结果，但不支持全输入结论。

L567    (∃ f, Compatible [zeroRecord] f) ∧

要求存在与单次观测相容的真实函数，避免空证据语义。

L568    Supports [zeroRecord] (fun f => f 0 = true) ∧

该单条记录支持其真实输入 0 主张。

L569    ¬ Supports [zeroRecord] allTrue :=

它不支持更强的全输入主张。

L570  ⟨rfl, ⟨localGenerator 0, (zeroCompatible _).2 rfl⟩,

计算记录数量为一，并提供 localGenerator 0 作为真实相容见证。

L571    (fun f hf => (zeroCompatible f).1 hf), selfOriginDoesNotSupport.2.2.2.1⟩

从相容性直接提取获支持的输入 0 事实，并复用已证的 allTrue 支持失败。

L572/- This inferential assessment derives a successor value from its explicit numeric premise without observation. -/

说明 arithmeticFacet 的预定范围。对应声明涉及：以n=2为假设、n+1=3为结论构造推论面向。 该注释用于解释，不是证明前提。

L573def arithmeticFacet : Facet Nat := .inferential (singleton (fun n => n = 2)) (fun n => n + 1 = 3)

定义 arithmeticFacet。以n=2为假设、n+1=3为结论构造推论面向。

L574def usesObservation {W : Type} : Facet W → Bool

定义 usesObservation。只按面向标签判断是否经验型，不判断命题是否可计算。

L575  | .empirical _ _ _ _ => true

经验方面携带真实测试记录，因此将其分类为使用观测。

L576  | _ => false

在此已表示的方法分类器中，把推论与价值方面分类为不使用观测。

L577/- An actual valid inferential assessment refutes a mandatory measurement/repetition/framework chain. -/

说明 noUniversalChain 的预定范围。对应声明涉及：以二为模型证明算术推论面向成立且无需经验观察。 该注释用于解释，不是证明前提。

L578theorem noUniversalChain : FacetDischarged arithmeticFacet ∧ usesObservation arithmeticFacet = false := by

陈述经检查的结果 noUniversalChain。以二为模型证明算术推论面向成立且无需经验观察。 后续策略块证明这一显式类型。

L579  refine ⟨⟨⟨2, (modelsSingleton _ _).2 rfl⟩, ?_⟩, rfl⟩

提供 n=2 作为推论理论的非空见证，并指出其方面构造子不使用观测。

L580  intro n hn

任取满足算术方面真实前提理论的自然数世界 n。

L581  have premise := (modelsSingleton (fun x : Nat => x = 2) n).1 hn

从真实单元素前提提取 n=2，而不是假定所需后继结论。

L582  change n + 1 = 3

把算术结论 n+1=3 展开为剩余目标。

L583  rw [premise]

根据前提把 n 改写为 2；所需算术等式通过计算化简。

L584/- A trial has a reproducible setting, an actual outcome and a separately recorded outcome. -/

说明 Trial 的预定范围。对应声明涉及：分别保存设置、实际结果和记录结果三个自然数字段。 该注释用于解释，不是证明前提。

L585structure Trial where

声明数据接口 Trial。分别保存设置、实际结果和记录结果三个自然数字段。

L586  setting : Nat

保存试次设置，与结果分开。

L587  actualOutcome : Nat

保存试次实际结果，无论记录是否准确。

L588  recordedOutcome : Nat

保存独立记录的结果，以便比较准确性。

L589/- Verifying a record, reproducing settings and retaining a conclusion are separate predicates. -/

说明 Verified 的预定范围。对应声明涉及：记录结果等于给定实际结果即满足此验证谓词。 该注释用于解释，不是证明前提。

L590def Verified (t : Trial) : Prop := t.recordedOutcome = t.actualOutcome

定义 Verified。记录结果等于给定实际结果即满足此验证谓词。

L591def Reproduced (a b : Trial) : Prop := a.setting = b.setting

定义 Reproduced。只要求两次设置相等，不要求结果相同。

L592def Bounded (t : Trial) : Prop := t.actualOutcome ≤ 2

定义 Bounded。要求实际结果不超过固定阈值二。

L593/- Same-setting possible trials can differ while preserving the chosen bound; no probability semantics is claimed. -/

说明 variableOutcomesStableBound 的预定范围。对应声明涉及：同设置的结果一和二不同，却都满足给定范围界限。 该注释用于解释，不是证明前提。

L594theorem variableOutcomesStableBound :

陈述经检查的结果 variableOutcomesStableBound。同设置的结果一和二不同，却都满足给定范围界限。

L595    let a : Trial := ⟨0,1,1⟩

固定第一试次：设置 0，实际及记录结果均为 1。

L596    let b : Trial := ⟨0,2,2⟩

固定第二试次：设置相同，实际及记录结果均为 2。

L597    Reproduced a b ∧ a.actualOutcome ≠ b.actualOutcome ∧ Bounded a ∧ Bounded b := by

要求两个明确固定试次的设置相同、真实结果不同，且都满足 actualOutcome ≤ 2。

L598  simp [Reproduced, Bounded]

计算两个相同设置的试次：实际结果 1 与 2 不同，却都满足 actualOutcome ≤ 2。

L599/- Concrete records distinguish record accuracy, condition reproduction and conclusion stability. -/

说明 verificationReproductionStability 的预定范围。对应声明涉及：用具体数字分别区分记录准确、设置复现和结果有界。 该注释用于解释，不是证明前提。

L600theorem verificationReproductionStability :

陈述经检查的结果 verificationReproductionStability。用具体数字分别区分记录准确、设置复现和结果有界。

L601    (Verified ⟨0,1,1⟩ ∧ Verified ⟨1,1,1⟩ ∧ ¬ Reproduced ⟨0,1,1⟩ ⟨1,1,1⟩) ∧

要求两个记录准确但设置不同的试次。

L602    (Reproduced ⟨0,1,1⟩ ⟨0,3,2⟩ ∧ ¬ Verified ⟨0,3,2⟩ ∧ ¬ Bounded ⟨0,3,2⟩) ∧

要求设置复现，同时第二记录不准确且实际结果超出界限。

L603    (Bounded ⟨0,1,1⟩ ∧ Bounded ⟨0,2,0⟩ ∧ ¬ Verified ⟨0,2,0⟩) := by

要求界限保持，即使其中一个结果记录不准确。

L604  simp [Verified, Reproduced, Bounded]

分别计算各具体试次谓词，展示设置变化、记录不准确及界限失败或保持，而不混淆这些性质。

L605/- Explanation certificates are executable syntax for this same arithmetic process. -/

说明 Program 的预定范围。对应声明涉及：定义只含输入翻倍及常量的微型解释程序语法。 该注释用于解释，不是证明前提。

L606inductive Program where

声明可选构造 Program。定义只含输入翻倍及常量的微型解释程序语法。

L607  | doubleInput

提供把实际输入加倍的解释程序语法。

L608  | constant (value : Nat)

提供常量输出解释程序语法，携带其返回自然数。

L609def Program.eval : Program → Nat → Nat

定义 Program.eval。执行翻倍或返回储存常量。

L610  | .doubleInput, n => n + n

通过真实加法 n+n 计算 doubleInput 解释程序在 n 处的结果。

L611  | .constant value, _ => value

通过返回存储值计算常量程序，与输入无关。

L612/- A process exposes outputs and an explanation response, whose certificate can be checked against those outputs. -/

说明 Process 的预定范围。对应声明涉及：保存实际输出函数和可缺失的解释程序。 该注释用于解释，不是证明前提。

L613structure Process where

声明数据接口 Process。保存实际输出函数和可缺失的解释程序。

L614  output : Nat → Nat

保存同一过程在自然数输入上的真实输出函数。

L615  explanation : Option Program

保存过程可选的已提供解释程序，与输出函数分开。

L616/- The output-only application contract checks every relevant input. -/

说明 OutputContract 的预定范围。对应声明涉及：要求每个自然数输入的输出等于输入翻倍。 该注释用于解释，不是证明前提。

L617def OutputContract (p : Process) : Prop := ∀ n, p.output n = n + n

定义 OutputContract。要求每个自然数输入的输出等于输入翻倍。

L618/- The explanation application contract requires a provided certificate faithful to this very process. -/

说明 ExplanationContract 的预定范围。对应声明涉及：要求已附程序在所有输入上与同一过程输出相等，不断言因果理解。 该注释用于解释，不是证明前提。

L619def ExplanationContract (p : Process) : Prop :=

定义 ExplanationContract。要求已附程序在所有输入上与同一过程输出相等，不断言因果理解。

L620  ∃ program, p.explanation = some program ∧ ∀ n, program.eval n = p.output n

要求实际提供程序，且其在每个自然数输入的计算等于该过程输出。

L621/- This process produces doubled values but returns no explanatory certificate. -/

说明 outputOnlyProcess 的预定范围。对应声明涉及：给出正确翻倍输出，却不提供解释程序。 该注释用于解释，不是证明前提。

L622def outputOnlyProcess : Process := ⟨fun n => n + n, none⟩

定义 outputOnlyProcess。给出正确翻倍输出，却不提供解释程序。

L623def explainedProcess : Process := ⟨fun n => n + n, some .doubleInput⟩

定义 explainedProcess。给同样输出并附上翻倍程序。

L624/- Object scope fixes the very process whose contract is assessed; contract inputs themselves still range over all naturals. -/

说明 processScope 的预定范围。对应声明涉及：把候选范围限定为同一被评过程，不缩窄合同的输入量词域。 该注释用于解释，不是证明前提。

L625def processScope (assessed : Process) : Theory Process :=

定义 processScope。把候选范围限定为同一被评过程，不缩窄合同的输入量词域。

L626  singleton (fun candidate => candidate = assessed)

用真实等式 candidate=assessed 限制理论模型，而不是假定所需契约。

L627/- This inferential facet checks an explicit contract under exact process-identity assumptions. -/

说明 processContractFacet 的预定范围。对应声明涉及：在精确被评过程身份假设下构造合同推论面向。 该注释用于解释，不是证明前提。

L628def processContractFacet (assessed : Process) (contract : Claim Process) : Facet Process :=

定义 processContractFacet。在精确被评过程身份假设下构造合同推论面向。

L629  .inferential (processScope assessed) contract

用这一准确对象身份范围与给定契约结论构造推论方面。

L630/- The scope's compatible interpretations are exactly this assessed process, not an unrelated substitute. -/

说明 processScopeModels 的预定范围。对应声明涉及：证明满足身份范围恰好等价于候选为同一被评过程。 该注释用于解释，不是证明前提。

L631theorem processScopeModels (assessed candidate : Process) :

陈述经检查的结果 processScopeModels。证明满足身份范围恰好等价于候选为同一被评过程。

L632    Models (processScope assessed) candidate ↔ candidate = assessed :=

陈述满足该范围恰等于成为受评过程。

L633  modelsSingleton (fun process => process = assessed) candidate

用等于真实受评 Process 的谓词实例化 modelsSingleton，准确证明哪些候选满足 processScope。

L634/- A concrete contract proof supplies the facet's consequence for its scoped object. -/

说明 processContractDischarged 的预定范围。对应声明涉及：利用给定实际过程合同证明及范围身份等式，完成对应推论检查。 该注释用于解释，不是证明前提。

L635theorem processContractDischarged (assessed : Process) (contract : Claim Process) (proof : contract assessed) :

陈述经检查的结果 processContractDischarged。利用给定实际过程合同证明及范围身份等式，完成对应推论检查。

L636    FacetDischarged (processContractFacet assessed contract) := by

使用明确契约证明前提，得出同一对象契约方面的履行。

L637  refine ⟨⟨assessed,(processScopeModels _ _).2 rfl⟩, ?_⟩

以受评过程自身作为其身份范围的模型，留下契约的语义蕴含。

L638  intro candidate hc

任取候选及其处于真实受评过程身份范围的证明 hc。

L639  have same := (processScopeModels _ _).1 hc

从范围模型 hc 恢复候选恰为受评过程。

L640  subst candidate

代入该过程身份，使契约目标针对实际受评对象。

L641  exact proof

使用明确给出的该对象契约证明前提；此一般辅助结果不会无前提地产生契约正确性。

L642/- Scoped capability grounds include exact claim, object-specific assumptions, canonical articulation and actual assessment. -/

说明 ProcessGrounds 的预定范围。对应声明涉及：为精确过程及合同面向要求规范Grounds，适用范围只含该面向。 该注释用于解释，不是证明前提。

L643def ProcessGrounds (assessed : Process) (contract : Claim Process) : Prop :=

定义 ProcessGrounds。为精确过程及合同面向要求规范Grounds，适用范围只含该面向。

L644  Grounds contract canonicalArticulation (fun facet => facet = processContractFacet assessed contract)

要求给定契约具有 Grounds，使用规范表述，并将准确受评过程方面认定为适用。

L645    [processContractFacet assessed contract]

列出的证据组合恰好包含同一过程契约方面。

L646theorem processGrounds (assessed : Process) (contract : Claim Process) (proof : contract assessed) :

陈述经检查的结果 processGrounds。从同一被评过程的实际合同证明构造匹配Grounds。

L647    ProcessGrounds assessed contract := by

由受评过程处的明确契约证明，得出这些同一对象 ProcessGrounds。

L648  have discharged := processContractDischarged assessed contract proof

把契约履行辅助结果应用于同一受评过程的明确证明。

L649  refine ⟨by simp, ?_, ?_⟩

拆分方面非空、准确适用性覆盖，以及各方面的主张、表述与履行义务。

L650  · intro facet hf; subst facet; exact List.mem_singleton.mpr rfl

适用性假设把方面确定为规定的唯一方面，因此它属于该单元素列表。

L651  · intro facet hf; have hf' := List.mem_singleton.mp hf; subst facet

单元素成员关系把当前方面确定为规定方面；代入后检查其准确主张与依据。

L652    exact ⟨rfl,canonicalArticulated _ discharged,canonicalFacetArticulated _,discharged⟩

组合相同契约主张、非空规范表述、与对象范围的语义连接及已确立履行。

L653/- Universal output correctness here comes from the concrete program definition, not from an assumed capability label. -/

说明 outputCorrectByEvaluation 的预定范围。对应声明涉及：从实际输出函数直接证明全输入翻倍，不假定成功标记。 该注释用于解释，不是证明前提。

L654theorem outputCorrectByEvaluation : OutputContract outputOnlyProcess := fun _ => rfl

陈述经检查的结果 outputCorrectByEvaluation。从实际输出函数直接证明全输入翻倍，不假定成功标记。 给出的证明项使用所示构造见证或先前引理，而不增加公理。

L655/- This same process actually returns no explanation certificate. -/

说明 outputOnlyNoExplanation 的预定范围。对应声明涉及：因同一过程储存none而拒绝已附解释程序的存在。 该注释用于解释，不是证明前提。

L656theorem outputOnlyNoExplanation : ¬ ExplanationContract outputOnlyProcess := by

陈述经检查的结果 outputOnlyNoExplanation。因同一过程储存none而拒绝已附解释程序的存在。 后续策略块证明这一显式类型。

L657  rintro ⟨program,h,_⟩; cases h

任何解释契约都需提供程序，令其 some 值等于该过程实际的 none 回应；不同选项构造子使之不可能。

L658/- The full application contract requires outputs and an explanation of that same process. -/

说明 FullProcessContract 的预定范围。对应声明涉及：要求同一过程既输出正确，又附有输出一致的解释程序。 该注释用于解释，不是证明前提。

L659def FullProcessContract (assessed : Process) : Prop := OutputContract assessed ∧ ExplanationContract assessed

定义 FullProcessContract。要求同一过程既输出正确，又附有输出一致的解释程序。

L660/- Output-only grounds have the assessed process itself as a counterworld to the stronger contract. -/

说明 OutputContractEvidence 的预定范围。对应声明涉及：组合有根据输出及非空精确过程范围，以该模型反驳更强完整合同。 该注释用于解释，不是证明前提。

L661def OutputContractEvidence : Prop :=

定义 OutputContractEvidence。组合有根据输出及非空精确过程范围，以该模型反驳更强完整合同。

L662  ProcessGrounds outputOnlyProcess OutputContract ∧

要求真实只输出过程具有输出正确性依据。

L663  Models (processScope outputOnlyProcess) outputOnlyProcess ∧

保留该过程自身作为准确评估范围中的实例。

L664  ¬ Entails (processScope outputOnlyProcess) FullProcessContract

否定同一范围蕴含更强的输出与解释联合契约。

L665/- Existing output evidence does not supply the absent explanation for the same object and scope. -/

说明 outputContractEvidence 的预定范围。对应声明涉及：由计算建立输出Grounds，并用同一过程缺少解释反驳完整合同蕴涵。 该注释用于解释，不是证明前提。

L666theorem outputContractEvidence : OutputContractEvidence := by

陈述经检查的结果 outputContractEvidence。由计算建立输出Grounds，并用同一过程缺少解释反驳完整合同蕴涵。 后续策略块证明这一显式类型。

L667  refine ⟨processGrounds _ _ outputCorrectByEvaluation, (processScopeModels _ _).2 rfl, ?_⟩

提供真实输出契约的依据及过程自身的范围见证，再在同一范围内否定更强契约。

L668  intro stronger

假定该准确过程范围蕴含更强的输出与解释联合契约。

L669  exact outputOnlyNoExplanation (stronger outputOnlyProcess ((processScopeModels _ _).2 rfl)).2

在 outputOnlyProcess 自身处实例化假定的完整契约蕴含；其解释部分与已证的解释缺失矛盾。

L670/- Both actual application contracts have grounds and explicit object scopes; neither scope is empty. -/

说明 ScopedApplicationEvidence 的预定范围。对应声明涉及：要求两个不同应用合同分别具有Grounds及非空精确过程范围。 该注释用于解释，不是证明前提。

L671def ScopedApplicationEvidence : Prop :=

定义 ScopedApplicationEvidence。要求两个不同应用合同分别具有Grounds及非空精确过程范围。

L672  ProcessGrounds outputOnlyProcess OutputContract ∧

纳入 outputOnlyProcess 的输出正确性依据。

L673  ProcessGrounds explainedProcess FullProcessContract ∧

纳入 explainedProcess 的输出与解释联合依据。

L674  (∀ candidate, Models (processScope outputOnlyProcess) candidate ↔ candidate = outputOnlyProcess) ∧

对每个候选明确第一个范围准确固定为 outputOnlyProcess。

L675  (∀ candidate, Models (processScope explainedProcess) candidate ↔ candidate = explainedProcess) ∧

同样明确第二个范围准确固定为 explainedProcess。

L676  Satisfiable (processScope outputOnlyProcess) ∧ Satisfiable (processScope explainedProcess)

要求两个真实过程身份理论均可满足。

L677/- Concrete evaluation and a faithful double-input certificate establish the two differently scoped contracts. -/

说明 scopedApplicationEvidence 的预定范围。对应声明涉及：提供实际全输入输出证明，并为强合同提供翻倍解释程序。 该注释用于解释，不是证明前提。

L678theorem scopedApplicationEvidence : ScopedApplicationEvidence := by

陈述经检查的结果 scopedApplicationEvidence。提供实际全输入输出证明，并为强合同提供翻倍解释程序。 后续策略块证明这一显式类型。

L679  refine ⟨processGrounds _ _ outputCorrectByEvaluation, processGrounds _ _ ?_,

通过计算构造只输出依据，并留下有解释过程的更强契约证明。

L680    processScopeModels _,processScopeModels _,⟨_,(processScopeModels _ _).2 rfl⟩,

提供准确的过程身份范围等价关系，并用各过程自身作为其非空范围见证。

L681    ⟨_,(processScopeModels _ _).2 rfl⟩⟩

提供准确的过程身份范围等价关系，并用各过程自身作为其非空范围见证。

L682  exact ⟨fun _ => rfl,⟨.doubleInput,rfl,fun _ => rfl⟩⟩

对 explainedProcess，通过自反性证明每个加倍输出，并提供实际给出且外延忠实的解释程序 doubleInput。

L683/- Universal output correctness does not entail the explanation-requiring contract for the same process. -/

说明 outputNotExplanation 的预定范围。对应声明涉及：证明输出正确但无已附解释，并附同对象Grounds及反模型证据。 该注释用于解释，不是证明前提。

L684theorem outputNotExplanation : OutputContract outputOnlyProcess ∧

陈述经检查的结果 outputNotExplanation。证明输出正确但无已附解释，并附同对象Grounds及反模型证据。

L685    ¬ ExplanationContract outputOnlyProcess ∧ OutputContractEvidence :=

保留该过程解释契约缺失及其范围内输出证据。

L686  ⟨outputCorrectByEvaluation, outputOnlyNoExplanation, outputContractEvidence⟩

组合真实输出正确性、同一过程解释缺失及其匹配的范围内输出证据。

L687/- Applications may use distinct contracts, and a faithful certificate can satisfy the stronger one. -/

说明 applicationContractsDiffer 的预定范围。对应声明涉及：证明仅输出不足以满足强合同，解释过程满足两者；两个应用各有对应Grounds。 该注释用于解释，不是证明前提。

L688theorem applicationContractsDiffer :

陈述经检查的结果 applicationContractsDiffer。证明仅输出不足以满足强合同，解释过程满足两者；两个应用各有对应Grounds。

L689    (OutputContract outputOnlyProcess ∧ ¬ (OutputContract outputOnlyProcess ∧ ExplanationContract outputOnlyProcess)) ∧

只输出过程满足输出正确性，却未满足输出与解释联合契约。

L690    (OutputContract explainedProcess ∧ ExplanationContract explainedProcess) ∧

有解释过程满足两个真实契约。

L691    ScopedApplicationEvidence :=

纳入两个应用契约的明确范围内依据与非空见证。

L692  ⟨⟨outputCorrectByEvaluation, fun h => outputOnlyNoExplanation h.2⟩,

对 outputOnlyProcess 提供真实输出正确性，并通过提取不可能解释组件反驳任何联合契约。

L693    ⟨(fun _ => rfl), ⟨.doubleInput, rfl, fun _ => rfl⟩⟩, scopedApplicationEvidence⟩

对 explainedProcess 计算全部加倍输出，提供忠实 doubleInput 语法，并纳入两个契约匹配的范围内依据。

L694/- The assessor supplies a mathematical certificate; the process's own explanation response is unnecessary. -/

说明 ExternalCertificate 的预定范围。对应声明涉及：把输出证明绑定到精确过程及不同评估者、被评者编号；这是数学角色模型，不认证现实出处。 该注释用于解释，不是证明前提。

L695structure ExternalCertificate (p : Process) where

声明数据接口 ExternalCertificate。把输出证明绑定到精确过程及不同评估者、被评者编号；这是数学角色模型，不认证现实出处。

L696  assessorId : Nat

保存外部评估者标识。

L697  assessedId : Nat

保存受评参与者标识；证书类型已固定受评 Process。

L698  distinctParticipants : assessorId ≠ assessedId

把参与者标识不同规定为明确证书字段。

L699  outputCorrect : ∀ n, p.output n = n + n

要求同一过程每个输入加倍输出的证明；一般证书假定该字段，具体证书则构造它。

L700/- The external assessor 42 evaluates the specified process 7; the full output proof is constructed by evaluation. -/

说明 externalOutputCertificate 的预定范围。对应声明涉及：由实际输出计算构造评估者四十二对被评对象七的证书。 该注释用于解释，不是证明前提。

L701def externalOutputCertificate : ExternalCertificate outputOnlyProcess :=

定义 externalOutputCertificate。由实际输出计算构造评估者四十二对被评对象七的证书。

L702  ⟨42,7,by decide,fun _ => rfl⟩

构造参与者 42 与 7，计算其不等，并依真实程序自反性证明每个加倍输出。

L703/- An external certificate establishes the output contract without producing an internal explanation. -/

说明 externalAssessment 的预定范围。对应声明涉及：由不同参与者证书提供匹配输出Grounds，而被评过程仍不返回解释。 该注释用于解释，不是证明前提。

L704theorem externalAssessment :

陈述经检查的结果 externalAssessment。由不同参与者证书提供匹配输出Grounds，而被评过程仍不返回解释。

L705    (∃ certificate : ExternalCertificate outputOnlyProcess,

要求存在以 outputOnlyProcess 为索引的真实外部证书。

L706      certificate.assessorId = 42 ∧ certificate.assessedId = 7 ∧

确定其评估者为 42、受评参与者为 7。

L707      certificate.assessorId ≠ certificate.assessedId ∧ OutputContract outputOnlyProcess) ∧

要求两者不同，且同一过程真实输出正确。

L708    ProcessGrounds outputOnlyProcess OutputContract ∧

还保留同一输出契约匹配的 ProcessGrounds。

L709    ¬ ExplanationContract outputOnlyProcess :=

仍否定该实际过程具有内部解释契约。

L710  ⟨⟨externalOutputCertificate,rfl,rfl,externalOutputCertificate.distinctParticipants,

使用真实 externalOutputCertificate，参与者固定为 42 与 7，并带有两者不同的证明。

L711    externalOutputCertificate.outputCorrect⟩,

从该具体证书提取全称输出正确性，其证明由真实程序构造。

L712    processGrounds outputOnlyProcess OutputContract externalOutputCertificate.outputCorrect,

使用同一具体输出证明，为该 outputOnlyProcess 构造匹配的 ProcessGrounds。

L713    outputOnlyNoExplanation⟩

保留 outputOnlyNoExplanation，因此外部证书不声称存在内部解释。

L714/- This argument records concepts and actual premises for a semantic inference, separately from executable tests. -/

说明 arithmeticArticulation 的预定范围。对应声明涉及：取得算术推论面向的规范表达。 该注释用于解释，不是证明前提。

L715def arithmeticArticulation : Articulation Nat := canonicalArticulation arithmeticFacet

定义 arithmeticArticulation。取得算术推论面向的规范表达。

L716/- A reasoned inferential assessment needs no observation method, while applicable empirical assessment retains observations. -/

说明 nonExecutableAssessment 的预定范围。对应声明涉及：实际算术根据检查不要求经验测试，同时保留经验面向的观察义务。 该注释用于解释，不是证明前提。

L717theorem nonExecutableAssessment :

陈述经检查的结果 nonExecutableAssessment。实际算术根据检查不要求经验测试，同时保留经验面向的观察义务。

L718    Grounds (fun n : Nat => n + 1 = 3) canonicalArticulation (fun f => f = arithmeticFacet) [arithmeticFacet] ∧

要求仅用 arithmeticFacet，为 n+1=3 提供匹配的规范 Grounds。

L719    usesObservation arithmeticFacet = false ∧

规定该推论方面不使用观测。

L720    FacetDischarged switchEmpirical ∧ usesObservation switchEmpirical = true := by

同时纳入确实使用观测且真实已履行的经验方面。

L721  refine ⟨⟨by simp, (by intro f hf; cases hf; simp), ?_⟩, rfl, switchEmpiricalDischarged, rfl⟩

构造算术主张的非空且覆盖适用性的 Grounds，保留其无观测分类，并纳入有效的观测开关方面。

L722  intro f hf; simp only [List.mem_singleton] at hf; cases hf

单元素成员关系把受评方面固定为 arithmeticFacet，因此检查其具体假设与结论。

L723  exact ⟨rfl, canonicalArticulated _ noUniversalChain.1, canonicalFacetArticulated _, noUniversalChain.1⟩

使用同一算术方面已证的履行，配以非空规范表述及其准确语义连接。

L725end CoreReader.Evidence

关闭命名空间 CoreReader.Evidence；这不增加证明或前提。