leanified/CoreReader/Agency.lean
哲学 0.2.1 · 已考虑的 Core 0.1.2。阅读视图来自本仓库公开的目标清单、读者稿和 Lean 文件；页面布局不改变其中的判定。
展开 Lean 与逐行解读 · 215 行
L1import CoreReader.Reflexivity导入CoreReader.Reflexivity及其依赖。
L3namespace CoreReader.Agency打开命名空间CoreReader.Agency；文件边界不改变声明身份。
L5inductive FormKind | organization | method | principle | appearance | artifact定义组织、方法、原则、外观和产物五类形式标签。
L6 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L8structure Form where形式由种类标签和自然数版本构成，不包含内容或转换规则。
L9 kind : FormKind保存该形式属于组织、方法、原则、外观还是产物。
L10 version : Nat保存自然数形式版本，不证明变化已经发生。
L11 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L13inductive Aim | expandUnderstandingAndConstruction | preserveSafeOperation定义扩展理解与构造、保持安全运行两个目标标签；数据类型自身不为任一目标赋值。
L14 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L16/- A policy records an adopted valuation, current forms, and permission. It does not assert that valuation is correct or enacted. -/说明后续定义或结果：分别保存目标价值、当前形式、可修订形式和版本许可四个谓词。
L17structure Policy where分别保存目标价值、当前形式、可修订形式和版本许可四个谓词。
L18 worthPursuing : Aim → Prop规定此政策把两个已表示目标中的哪些视为值得追求。
L19 current : Form → Prop规定此政策当前持有的形式种类与版本对。
L20 revisable : Form → Prop规定此政策保留哪些形式种类与版本对的可修订性。
L21 permitsVersion : Nat → Nat → Prop独立于实际执行规定版本间许可。
L23/- The normative specification keeps valuation and revisability separate from realized transitions. -/说明后续定义或结果：要求视扩展为值得追求，且全部当前形式可修订；不承诺执行或进步。
L24def Generative (p : Policy) : Prop :=要求视扩展为值得追求，且全部当前形式可修订；不承诺执行或进步。
L25 p.worthPursuing .expandUnderstandingAndConstruction ∧要求该政策把理解与构造的扩展视为值得追求。
L26 ∀ f, p.current f → p.revisable f要求该政策当前持有的每个形式仍可修订。
L28def openPolicy : Policy where重视两个目标，以版本零为当前形式，并允许所有修订和版本对。
L29 worthPursuing a := a = .expandUnderstandingAndConstruction ∨ a = .preserveSafeOperationopenPolicy同时重视扩展与保持安全运行。
L30 current f := f.version = 0把版本恰为0的形式视为当前形式，不限种类。
L31 revisable _ := True允许修订所有形式，包括当前未持有的形式。
L32 permitsVersion _ _ := True允许任意两个版本号间的变更，但不执行变更。
L34def neutralPolicy : Policy := { openPolicy with worthPursuing := fun _ => False }保留开放政策许可，但把所有目标价值设为假。
L36/- Permitting a real version change does not supply an adopted value position. -/说明后续定义或结果：实际允许不同版本零到一，同时缺少扩展价值取向，证明许可不充分。
L37theorem permissionNotValuation :实际允许不同版本零到一，同时缺少扩展价值取向，证明许可不充分。
L38 neutralPolicy.permitsVersion 0 1 ∧ (0 : Nat) ≠ 1 ∧ ¬ Generative neutralPolicy := by陈述neutralPolicy允许0→1且两版本不同，但缺少价值取向使Generative失败。
L39 simp [neutralPolicy, openPolicy, Generative]展开两个政策：许可为真，0≠1可计算为真，所需价值取向为假。
L41/- This is an explicit consequence of the adopted specification, not evidence of actual revision. -/说明后续定义或结果：将已假定的生成规范实例化到指定当前种类与版本，不执行修订。
L42theorem revisabilityCovers (p : Policy) (h : Generative p) (k : FormKind) (v : Nat)将已假定的生成规范实例化到指定当前种类与版本，不执行修订。
L43 (hc : p.current ⟨k, v⟩) : p.revisable ⟨k, v⟩ := h.2 _ hc将h中的可修订条款应用于hc确认是当前形式的同一种类与版本。
L45inductive Operation | copy | successor只定义自然数恒等和后继两种操作。
L46 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L48def Operation.run : Operation → Nat → Nat按构造器计算恒等或加一输出。
L49 | .copy, n => n执行copy直接返回原输入。
L50 | .successor, n => n + 1执行successor返回输入加1。
L52inductive InventoryKind | document | term | tool | artifact定义文档、术语、工具、产物四个库存标签。
L53 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L55structure Item where库存项保存种类标签及两种操作之一。
L56 kind : InventoryKind把库存条目分类为文档、术语、工具或产物。
L57 content : Operation记录条目表示的操作，与其类别分开。
L58 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L60/- Available represented operations are the contents present, not their number of occurrences. -/说明后续定义或结果：存在库存成员携带指定操作即为可用；重复次数不影响此条件。
L61def Available (xs : List Item) (op : Operation) : Prop :=存在库存成员携带指定操作即为可用；重复次数不影响此条件。
L62 ∃ item ∈ xs, item.content = op只有存在包含该操作的列表条目，该操作才可用。
L64/- Duplicating any inventory category preserves exactly the represented operation content. -/说明后续定义或结果：通过双向复用同一成员见证，证明复制任一种类库存不会新增可用操作。
L65theorem inventoryNotCapability (kind : InventoryKind) (ops : List Operation) (op : Operation) :通过双向复用同一成员见证，证明复制任一种类库存不会新增可用操作。
L66 Available ((ops.map fun x => Item.mk kind x) ++ (ops.map fun x => Item.mk kind x)) op ↔检查把ops按固定类别包装并复制列表后的操作可用性。
L67 Available (ops.map fun x => Item.mk kind x) op := by将其与同一列表未复制时的可用性比较。
L68 simp only [Available, List.mem_append]展开可用性，把复制列表成员关系化为属于任一副本。
L69 constructor分别证明复制既不增加也不减少已表示的操作。
L70 · rintro ⟨x, hx | hx, hop⟩ <;> exact ⟨x, hx, hop⟩任一副本中的条目都可作为原列表中同一操作的见证。
L71 · rintro ⟨x, hx, hop⟩反向证明取原条目x、成员证明hx及内容匹配证明hop。
L72 exact ⟨x, Or.inl hx, hop⟩把同一条目放在第一副本中，保持操作匹配。
L74structure State where用五个列表分别表示理解、构造、库存、抽象层级和词汇。
L75 understood : List Operation列出该状态中表示为已理解的操作。
L76 constructed : List Operation列出该状态中表示为已构造的操作。
L77 inventory : List Item保存库存条目；条目重复数量与能力成员关系不同。
L78 abstractionLayers : List Operation保存抽象层级条目，不把数量等同理解能力。
L79 vocabulary : List Operation保存词汇条目，不把数量等同构造能力。
L80 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L82/- A gain must identify an operation newly understood or constructed; this is a disclosed finite capability representation. -/说明后续定义或结果：理解或构造列表新增至少一个先前没有的操作；不要求其他能力都保留。
L83def Expanded (before after : State) : Prop :=理解或构造列表新增至少一个先前没有的操作；不要求其他能力都保留。
L84 (∃ op, op ∈ after.understood ∧ op ∉ before.understood) ∨扩展可由变化后已理解、变化前未理解的操作见证。
L85 (∃ op, op ∈ after.constructed ∧ op ∉ before.constructed)另一种扩展见证是新增的已构造操作。
L87def baseState : State :=构造只含copy操作、一个copy产物的初始状态。
L88 ⟨[.copy], [.copy], [⟨.artifact, .copy⟩], [.copy], [.copy]⟩基线理解并构造copy，且各有一个copy产物、层级和词汇条目。
L90def inflatedState : State :=只复制库存、层级和词汇，理解与构造列表保持原样。
L91 { baseState with以baseState为起点，保留下面未覆盖的字段。
L92 inventory := baseState.inventory ++ baseState.inventory复制单条库存，但保持已理解和已构造操作不变。
L93 abstractionLayers := [.copy, .copy]将一个抽象层级条目改为两个copy条目。
L94 vocabulary := [.copy, .copy] }同样把词汇列表加倍，不引入新操作。
L96def stableTrace (_time : Nat) : State := baseState每个时刻都返回同一初始状态。
L98/- A revisable policy can govern an unchanged trace; no improvement is hidden in revisability. -/说明后续定义或结果：生成规范和全面可修订性与常值、无扩展轨迹相容。
L99theorem revisionWithoutProgress :生成规范和全面可修订性与常值、无扩展轨迹相容。
L100 Generative openPolicy ∧陈述openPolicy满足所采纳的价值取向与可修订规范。
L101 (∀ k : FormKind, openPolicy.revisable ⟨k, 0⟩) ∧另明确每类形式的版本0均可修订。
L102 (∀ t, ¬ Expanded (stableTrace t) (stableTrace (t + 1))) := by常值轨迹中任意相邻状态都没有新增理解或构造操作。
L103 simp [Generative, openPolicy, stableTrace, Expanded]把政策条款化为真，把每项扩展化为未变列表中不可能的新增成员。
L105structure ExternalResources where保存经验、知识和协作者三个可缺失自然数槽。
L106 experience : Option Nat可选外部经验值；none会使辅助执行在首次读取时失败。
L107 knowledge : Option Nat继经验输入后必须取得的可选知识值。
L108 collaborator : Option Nat产生结果前必须取得的可选协作者值。
L109 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L111/- This interpreter actually needs all three external inputs to produce the modeled result. -/说明后续定义或结果：依次读取三个Option槽；全部存在时返回总和，任一缺失时返回none。
L112def assistedExecution (r : ExternalResources) : Option Nat := do依次读取三个Option槽；全部存在时返回总和，任一缺失时返回none。
L113 let e ← r.experience将经验读入e，若资源缺失则立即返回none。
L114 let k ← r.knowledge将知识读入k，缺失则终止同一个Option计算。
L115 let c ← r.collaborator将协作者值读入c，同样传递缺失结果。
L116 pure (Operation.copy.run (e + k + c))通过copy操作返回e+k+c之和，并包装为some。
L118def availableResources : ExternalResources := ⟨some 1, some 2, some 3⟩提供一、二、三三个实际资源值。
L120/- Stability has a concrete stated reason in this workload: preserve its operation while staying within the one-item budget. -/说明后续定义或结果：要求构造列表相同、原库存至多一项而拟议库存超限。
L121def StableReason (before proposed : State) : Prop :=要求构造列表相同、原库存至多一项而拟议库存超限。
L122 before.constructed = proposed.constructed ∧保留旧状态的理由之一是两状态具有完全相同的已构造操作。
L123 before.inventory.length ≤ 1 ∧ ¬ proposed.inventory.length ≤ 1旧库存必须满足单条限制，而拟议库存超过该限制。
L125/- The policy, current capabilities, execution interface and workload constraints belong to one generating system. -/说明后续定义或结果：把同一主体的政策、当前状态、资源执行函数、预算和所需操作绑定成系统。
L126structure GeneratingSystem where把同一主体的政策、当前状态、资源执行函数、预算和所需操作绑定成系统。
L127 owner : Nat标识该生成系统的所有者。
L128 policy : Policy把价值取向与可修订政策附于同一系统。
L129 current : State保存系统当前的能力与库存表示状态。
L130 execute : ExternalResources → Option Nat保存该系统实际消耗资源的执行函数。
L131 applicationBudget : Nat规定评估稳定状态和拟议状态的库存数量预算。
L132 requiredOperations : List Operation规定工作负载要求保持已构造的操作。
L133/- The modeled system uses the assisted interpreter under a one-item budget and a copy-operation requirement. -/说明后续定义或结果：主体零采用开放政策、初始状态、三资源执行、预算一和copy要求。
L134def generatingSystem : GeneratingSystem where主体零采用开放政策、初始状态、三资源执行、预算一和copy要求。
L135 owner := 0给具体生成系统分配所有者编号0。
L136 policy := openPolicy在同一具体系统中采用openPolicy。
L137 current := baseState将其当前能力和库存设为baseState。
L138 execute := assistedExecution以需要三种资源的辅助解释器作为该系统执行接口。
L139 applicationBudget := 1把该工作负载的库存预算定为恰好1条。
L140 requiredOperations := [.copy]要求具体工作负载保留copy操作。
L141/- A stable action retains this system's own current state. -/说明后续定义或结果：以该系统当前状态作为保持稳定的动作结果。
L142def GeneratingSystem.stableAction (system : GeneratingSystem) : State := system.current以该系统当前状态作为保持稳定的动作结果。
L143def GeneratingSystem.requirementsMet (system : GeneratingSystem) (state : State) : Prop :=检查同一系统要求的每个操作都在被评状态构造列表中。
L144 ∀ operation, operation ∈ system.requiredOperations → operation ∈ state.constructed对该系统和待评状态，所有必需操作都必须属于状态的已构造列表。
L145def GeneratingSystem.withinBudget (system : GeneratingSystem) (state : State) : Prop :=按该系统明示预算检查被评状态库存长度。
L146 state.inventory.length ≤ system.applicationBudget用同一系统声明的应用预算检查该状态的库存数量。
L147/- An expansion report identifies the actual before/after states and the operation/performance it asserts was added. -/说明后续定义或结果：保存报告主体、精确前后状态、声称新增操作、输入和期望输出。
L148structure Announcement where保存报告主体、精确前后状态、声称新增操作、输入和期望输出。
L149 owner : Nat记录该扩展公告的所有者。
L150 before : State保存公告指定的确切基线状态。
L151 after : State保存公告指定的确切结果状态。
L152 reportedNewOperation : Operation指定声称新增构造的操作。
L153 input : Nat固定公告声称该操作表现所用的输入。
L154 expectedOutput : Nat保存该操作在指定输入上的声称输出。
L155 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L156/- Reports are generated by this system and identify its actual current state as their baseline. -/说明后续定义或结果：用本系统主体和当前状态构造对应拟议状态及操作合同的报告。
L157def GeneratingSystem.report (system : GeneratingSystem) (after : State)用本系统主体和当前状态构造对应拟议状态及操作合同的报告。
L158 (operation : Operation) (input expectedOutput : Nat) : Announcement :=接收该报告声称新增的操作及具体输入输出对。
L159 ⟨system.owner, system.current, after, operation, input, expectedOutput⟩以系统所有者和当前基线构造报告，并填入给定后状态与主张数据。
L160/- Report content is interpreted against those very states and the named operation's actual behavior. -/说明后续定义或结果：要求声称操作在后状态中新出现，并在指定输入产生期望输出。
L161def Announcement.claim (report : Announcement) : Prop :=要求声称操作在后状态中新出现，并在指定输入产生期望输出。
L162 report.reportedNewOperation ∈ report.after.constructed ∧报告所称新增操作必须实际属于公告的后状态。
L163 report.reportedNewOperation ∉ report.before.constructed ∧同一操作必须不属于公告基线的已构造列表。
L164 report.reportedNewOperation.run report.input = report.expectedOutput该操作在报告输入上的实际运行必须等于声称输出。
L165/- A true report of this form entails a represented construction expansion. -/说明后续定义或结果：从已成立报告中抽取新构造操作，作为扩展的存在见证。
L166theorem announcementClaimImpliesExpansion (report : Announcement) (h : report.claim) :从已成立报告中抽取新构造操作，作为扩展的存在见证。
L167 Expanded report.before report.after := Or.inr ⟨report.reportedNewOperation, h.1, h.2.1⟩用主张中的后状态成员关系与前状态缺失关系构造Expanded的构造分支。
L168/- This concrete self-report asserts a successor operation for the actual inventory-only inflation. -/说明后续定义或结果：系统对仅库存膨胀的状态报告零输入上的新增successor。
L169def inflatedAnnouncement : Announcement := generatingSystem.report inflatedState .successor 0 1系统对仅库存膨胀的状态报告零输入上的新增successor。
L170/- The report asserts a real successor result but its named operation is absent from its own after-state. -/说明后续定义或结果：核实报告对象后计算其新增操作主张及实际扩展均不成立。
L171theorem inflatedAnnouncementRefuted :核实报告对象后计算其新增操作主张及实际扩展均不成立。
L172 inflatedAnnouncement.before = baseState ∧ inflatedAnnouncement.after = inflatedState ∧确认具体公告所指正是baseState与inflatedState。
L173 inflatedAnnouncement.reportedNewOperation = .successor ∧确认声称新增操作是successor。
L174 inflatedAnnouncement.input = 0 ∧ inflatedAnnouncement.expectedOutput = 1 ∧确认公告中的测试输入是0、预期输出是1。
L175 ¬ inflatedAnnouncement.claim ∧ ¬ Expanded inflatedAnnouncement.before inflatedAnnouncement.after := by陈述公告实质主张失败，且公告自身的状态对没有扩展。
L176 simp [inflatedAnnouncement, GeneratingSystem.report, generatingSystem, Announcement.claim, Expanded, baseState, inflatedState]计算报告字段和未变能力列表；即使successor的0→1表现正确，后状态仍没有该操作。
L178/- These transitions share one initial state; only extension adds an actual new operation. -/说明后续定义或结果：成就模型仅含库存膨胀与实际操作扩展两个候选变化。
L179inductive TransitionCase | inflate | extend成就模型仅含库存膨胀与实际操作扩展两个候选变化。
L180 deriving DecidableEq, Repr为前述数据类型生成可判定相等及显示实例。
L182def extendedState : State :=在初始状态的理解和构造列表中添加successor。
L183 { baseState with understood := [.copy, .successor], constructed := [.copy, .successor] }在理解与构造列表中同时加入successor，保留基线其他字段。
L184def transitionBefore (_transition : TransitionCase) : State := baseState两种模型变化使用同一个初始状态基线。
L185def transitionAfter : TransitionCase → State按变化类别选择库存膨胀或能力扩展后状态。
L186 | .inflate => inflatedStateinflate转移以仅膨胀库存的状态结束。
L187 | .extend => extendedStateextend转移以新增理解和构造successor的状态结束。
L188/- Both alternatives are assessed under the same concrete input condition. -/说明后续定义或结果：两种变化都明确使用零作为测试输入。
L189def transitionInput (_transition : TransitionCase) : Nat := 0两种变化都明确使用零作为测试输入。
L190def transitionAnnouncement (transition : TransitionCase) : Announcement :=对同一系统及指定后状态报告successor在零处输出一。
L191 generatingSystem.report (transitionAfter transition) .successor (transitionInput transition) 1两种转移都在共同输入0上公告successor，但各自指定实际后状态。
L193/- Eleven boundary branches share a content-bearing trace and executable dependency model. They do not assert a universal law of human capability. -/说明后续定义或结果：在绑定系统上核实数量不增能力、外援依赖、有根据稳定动作和同对象虚假成就报告等全部分支。
L194theorem generationLimits :在绑定系统上核实数量不增能力、外援依赖、有根据稳定动作和同对象虚假成就报告等全部分支。
L195 Generative generatingSystem.policy ∧具体系统仍满足所采纳的生成政策。
L196 generatingSystem.policy.permitsVersion 0 0 ∧其政策允许保持版本0，因此生成取向不要求每次行动都改变版本。
L197 ¬ Expanded generatingSystem.current inflatedState ∧膨胀该系统库存不会扩展其已表示能力。
L198 generatingSystem.current.inventory.length < inflatedState.inventory.length ∧膨胀状态的库存条目严格多于该系统当前状态。
L199 generatingSystem.current.abstractionLayers.length < inflatedState.abstractionLayers.length ∧抽象层级数也严格增加，却没有能力扩展。
L200 generatingSystem.current.vocabulary.length < inflatedState.vocabulary.length ∧在能力内容保持不变时，词汇条目数严格增加。
L201 generatingSystem.execute availableResources = some 6 ∧资源为1、2、3时，该系统执行实际返回some 6。
L202 generatingSystem.execute { availableResources with experience := none } = none ∧从同一资源包移除经验，使该系统执行失败。
L203 generatingSystem.execute { availableResources with knowledge := none } = none ∧单独移除知识，同样使其执行返回none。
L204 generatingSystem.execute { availableResources with collaborator := none } = none ∧单独移除协作者输入，也使执行失败。
L205 generatingSystem.execute ⟨none, none, none⟩ = none ∧三种外部输入均缺失时，同一执行接口返回none。
L206 ¬ Expanded generatingSystem.current generatingSystem.stableAction ∧系统稳定动作不产生已表示能力扩展。
L207 generatingSystem.stableAction = generatingSystem.current ∧该稳定动作恰为保持系统当前状态。
L208 generatingSystem.requirementsMet generatingSystem.stableAction ∧保持当前状态可保留工作负载必需的copy操作。
L209 generatingSystem.withinBudget generatingSystem.stableAction ∧保留的单条状态满足该系统1条的应用预算。
L210 ¬ generatingSystem.withinBudget inflatedState ∧复制后库存有2条，超过同一系统的1条预算。
L211 StableReason generatingSystem.current inflatedState ∧稳定具有所述理由：构造内容未变，但只有当前状态满足预算。
L212 (inflatedAnnouncement = generatingSystem.report inflatedState .successor 0 1 ∧确认该报告由此系统针对inflatedState、successor、输入0和输出1构造。
L213 inflatedAnnouncement.owner = generatingSystem.owner ∧报告所有者等于该生成系统的所有者。
L214 inflatedAnnouncement.before = generatingSystem.current ∧ inflatedAnnouncement.after = inflatedState ∧报告以该系统当前状态为基线，以inflatedState为结果。
L215 inflatedAnnouncement.reportedNewOperation = .successor ∧此实际报告称为新增的操作是successor。
L216 inflatedAnnouncement.input = 0 ∧ inflatedAnnouncement.expectedOutput = 1 ∧报告声称的表现仍是具体的0→1。
L217 ¬ inflatedAnnouncement.claim ∧ ¬ Expanded inflatedAnnouncement.before inflatedAnnouncement.after) := by尽管存在该报告，其主张仍为假，其自身前后状态也没有能力扩展。
L218 simp [generatingSystem, GeneratingSystem.stableAction, GeneratingSystem.requirementsMet,展开具体系统、保持动作和必需操作检查，开始计算generationLimits各条款。
L219 GeneratingSystem.withinBudget, GeneratingSystem.report, Generative, openPolicy, Expanded,再展开单条预算、报告构造器和政策及扩展谓词，使主张化为具体数据。
L220 baseState, inflatedState, assistedExecution, availableResources, Operation.run,用实际基线及膨胀列表和三资源解释器，判定数量、成员关系和执行结果。
L221 StableReason, inflatedAnnouncement, Announcement.claim]最后展开稳定理由与自有公告主张，通过计算完成全部合取分支。
L223/- The empty work log omits an actually applicable system assessment despite an open generative policy. -/说明后续定义或结果：开放政策满足生成规范，但空记录无法履行非空自身规则的评估要求。
L224theorem generationNotReflexivity :开放政策满足生成规范，但空记录无法履行非空自身规则的评估要求。
L225 Generative openPolicy ∧ ¬ Reflexive 0 (ownRules 0) [] := by将openPolicy的生成取向与空工作日志下的自有反身履责失败组合。
L226 constructor分别证明生成取向，并反驳空日志的Reflexive主张。
L227 · simp [Generative, openPolicy]计算openPolicy的扩展价值取向与无条件可修订性。
L228 · intro h反证假设空日志满足自有反身契约。
L229 have bad := noSelfExemption 0 (ownRules 0) [] h (assessingRule 0) (by simp [ownRules])对已登记assessingRule应用无自我豁免定理，从假设的空日志履责迫出已执行评估。
L230 (.system 0) rfl (by simp [assessingRule, ownSubjects])选取所有者匹配的系统自身，并证明该评估对它适用。
L231 simp [Performed] at bad展开Performed后得到空工作列表中不可能存在的成员。
L233/- The same proposed arithmetic principle is used in the self-test and in the universal correctness claim. -/说明后续定义或结果：计算自然数等式n+1=2*n是否成立。
L234def ownArithmeticPrinciple (n : Nat) : Bool := decide (n + 1 = 2 * n)计算自然数等式n+1=2*n是否成立。
L236def selfTest (samples : List Nat) : Bool := samples.all ownArithmeticPrinciple逐个检验给定样本上的算术谓词，不检查样本外输入。
L238/- A genuine evaluation on the selected sample succeeds, while the same principle fails at zero. -/说明后续定义或结果：样本一通过而零失败，反驳从有限自测得到全称正确性。
L239theorem selfTestDoesNotProve :样本一通过而零失败，反驳从有限自测得到全称正确性。
L240 selfTest [1] = true ∧ ownArithmeticPrinciple 0 = false ∧同一算术原则在样本1上通过，却在0上为假。
L241 ¬ (∀ n, ownArithmeticPrinciple n = true) := by因此该原则并非对所有自然数输入都返回true。
L242 constructor将通过样本的计算与两项失败主张分开。
L243 · decide计算单样本：1+1等于2×1，故selfTest [1]为true。
L244 constructor把0处的具体失败与普遍成功的反驳分开。
L245 · decide计算0+1≠2×0，使ownArithmeticPrinciple 0为false。
L246 · intro h假设同一原则对每个输入都成功。
L247 have bad := h 0把该普遍假设实例化到输入0。
L248 contradiction与0处计算所得false矛盾，反驳普遍正确性。
L250end CoreReader.Agency关闭当前命名空间。