leanified/CoreReader/Reflexivity.lean

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

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

展开 Lean 与逐行解读 · 356 行

Lean逐行解读

L1import Std

导入Std及其依赖。

L3namespace CoreReader.Agency

打开命名空间CoreReader.Agency；文件边界不改变声明身份。

L5inductive Phase | formation | application | revision

定义形成、应用和修订三个阶段标签。

L6  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L8structure PrincipleKey where

用所属主体和局部编号标识登记原则。

L9  owner : Nat

保存所属主体编号。

L10  localId : Nat

保存主体内部原则编号。

L11  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L13inductive Subject

区分系统、原则及带阶段的原则过程对象。

L14  | system (owner : Nat)

用所有者编号表示系统自身。

L15  | principle (owner id : Nat)

用所有者及局部原则编号表示某项原则。

L16  | process (owner id : Nat) (phase : Phase)

把该原则的形成、应用或修订过程表示为独立对象。

L17  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L19def Subject.owner : Subject → Nat

从各类主体对象中提取所属主体编号。

L20  | .system n => n

直接从系统对象提取所有者。

L21  | .principle n _ => n

提取原则所有者，忽略局部编号。

L22  | .process n _ _ => n

提取过程对象所有者，不受原则编号和阶段影响。

L24inductive Activity | generation | assessment

区分生成工作与评估工作。

L25  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L27inductive QuestionKind | conformity | formationBasis | applicability | revisionGrounds

分别表示合规、形成根据、适用性和修订根据问题。

L28  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L30inductive SampleProgram | alwaysTrue | onlyAtZero

提供恒真程序及仅在零处为真的程序。

L31  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L33def SampleProgram.run : SampleProgram → Nat → Bool

在自然数输入上计算两种样例程序。

L34  | .alwaysTrue, _ => true

alwaysTrue样例程序接受每个自然数输入。

L35  | .onlyAtZero, n => n == 0

onlyAtZero程序仅在输入0时返回true。

L37/- A generated candidate specifies both the inputs it tests and the scope it proposes to license. -/

说明后续定义或结果：分别保存测试输入和声称范围，以表示超出测试的主张。

L38structure MethodDraft where

分别保存测试输入和声称范围，以表示超出测试的主张。

L39  testedInputs : List Nat

记录该方法草案实际测试程序的输入。

L40  claimedScope : List Nat

另记录该草案拟授权的输入范围。

L41  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L43def MethodDraft.accepts (draft : MethodDraft) (program : SampleProgram) : Bool :=

程序通过列表中全部测试即被接受，未测试输入不被检查。

L44  draft.testedInputs.all program.run

所有已测试输入返回true时接受程序；此处不检查claimedScope。

L46/- This finite application asks whether a proposed rule's observed inputs support its claimed input scope. -/

说明后续定义或结果：将目标对象与问题种类、请求范围和目标当前方法内容相连。

L47structure Inquiry where

将目标对象与问题种类、请求范围和目标当前方法内容相连。

L48  target : Subject

标识正在考察其方法的确切对象。

L49  kind : QuestionKind

区分符合性、形成理由、适用性和修订理由四类问题。

L50  requestedScope : List Nat

记录此问题要求方法覆盖的输入范围。

L51  currentMethod : MethodDraft

附上实际待考察方法草案，包括测试输入和声称范围。

L52  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L54inductive ReasonContent

表示目的、声明范围、观察以及具体程序和输入反例。

L55  | purpose (inputs : List Nat)

目的理由指定方法意欲处理的输入。

L56  | declaredScope (inputs : List Nat)

范围理由陈述方法声明的输入限度。

L57  | observation (input : Nat) (output : Bool)

观察理由记录具体输入和布尔输出。

L58  | counterexample (program : SampleProgram) (input : Nat)

反例理由指定待检查的实际样例程序与输入。

L59  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L61def ReasonContent.identifier : ReasonContent → Nat

给理由构造器分配编号；编号本身不提供根据。

L62  | .purpose _ => 0

目的理由使用局部引用0；它是类别编号，不是全局唯一标识。

L63  | .declaredScope _ => 1

声明范围理由使用局部引用1。

L64  | .observation _ _ => 2

观察理由使用局部引用2。

L65  | .counterexample _ _ => 3

反例理由使用局部引用3。

L67/- Reasons have independently supplied contents, a stable local reference and the actual target they concern. -/

说明后续定义或结果：把理由内容和引用编号绑定到其所针对对象。

L68structure ReasonObject where

把理由内容和引用编号绑定到其所针对对象。

L69  reference : Nat

保存该建模问题中此理由的局部引用。

L70  target : Subject

标识该理由实际针对的对象。

L71  content : ReasonContent

保存理由的目的、范围、观察或反例内容。

L72  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L74inductive AssessmentResult | supportedWithinScope | insufficient | notApplicable | undetermined

允许范围内支持、不充分、不适用和未确定四种结果。

L75  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L77inductive WorkOutcome

区分评估结果和生成的方法草案。

L78  | assessment (result : AssessmentResult)

把判定包装为评估结果；负面判定仍是评估。

L79  | generated (draft : MethodDraft)

包装新生成的方法草案，不断言该草案正确。

L80  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L82/- A method's question, source reasons and limits are determined before looking at its activity records.

说明后续定义或结果：登记规则身份、活动、方法内容、适用性、问题、理由、限度和结果语义。

L83The meaning relation describes application of that method, not its universal adequacy. -/

说明后续定义或结果：登记规则身份、活动、方法内容、适用性、问题、理由、限度和结果语义。

L84structure Principle where

登记规则身份、活动、方法内容、适用性、问题、理由、限度和结果语义。

L85  key : PrincipleKey

为原则赋予所有者与局部编号，用于解析其记录。

L86  activity : Activity

规定该原则约束生成活动还是评估活动。

L87  declaredMethod : MethodDraft

陈述该登记原则自身的方法草案。

L88  applicable : Subject → Prop

规定该原则适用的对象。

L89  inquiry : Subject → Inquiry

为每个对象指定实际待考察问题。

L90  reasons : Subject → List ReasonObject

为每个对象的问题指定所提供理由。

L91  limits : Subject → List Nat

为每个对象的适用指定保留的输入限度。

L92  meaning : Inquiry → List ReasonObject → List Nat → WorkOutcome → Prop

定义结果何时遵循该原则的问题、理由与限度；仅此字段不保证方法充分。

L94structure WorkRecord where

记录实际应用的规则身份、目标、活动、问题、理由、限度和结果。

L95  usedPrinciple : PrincipleKey

记录声称采用的确切登记原则标识。

L96  target : Subject

记录该工作针对的对象。

L97  activity : Activity

记录此工作是生成还是评估。

L98  inquiry : Inquiry

保存该工作的具体问题记录。

L99  reasons : List ReasonObject

保存该工作记录采用的具体理由。

L100  limits : List Nat

保存该工作记录保留的输入限度。

L101  outcome : WorkOutcome

保存记录的评估判定或生成的方法草案。

L102  deriving DecidableEq, Repr

为前述数据类型生成可判定相等及显示实例。

L104def RegistryCoherent (rules : List Principle) : Prop :=

要求相同登记键对应同一原则，排除身份歧义。

L105  ∀ p ∈ rules, ∀ q ∈ rules, p.key = q.key → p = q

两项已登记原则若标识相同，就必须是同一原则，防止查找歧义。

L107def TargetResolved (rules : List Principle) : Subject → Prop

要求评估目标能解析到登记主体或精确原则键。

L108  | .system owner => ∃ p ∈ rules, p.key.owner = owner

登记表中存在同所有者原则时，该系统对象可解析。

L109  | .principle owner id | .process owner id _ => ∃ p ∈ rules, p.key = ⟨owner,id⟩

原则和过程对象要求登记表中有确切所有者及局部编号对应项。

L111/- The inquiry names the registered target's declared method contract, not an unrelated candidate.

说明后续定义或结果：把问题中当前方法内容与登记目标原则的方法精确相连。

L112For a system inquiry this finite model uses the registered generation contract as its assessed artifact. -/

说明后续定义或结果：把问题中当前方法内容与登记目标原则的方法精确相连。

L113def TargetContentResolved (rules : List Principle) (question : Inquiry) : Prop :=

把问题中当前方法内容与登记目标原则的方法精确相连。

L114  match question.target with

按问题实际目标的种类选择查找规则。

L115  | .system owner => ∃ p ∈ rules, p.key = ⟨owner,0⟩ ∧ question.currentMethod = p.declaredMethod

系统问题考察其所有者已登记原则0的声明方法。

L116  | .principle owner id | .process owner id _ =>

对原则或其过程，按该目标实际所有者和编号查找。

L117      ∃ p ∈ rules, p.key = ⟨owner,id⟩ ∧ question.currentMethod = p.declaredMethod

要求确切标识查找成功，且问题所用方法等于登记原则的方法。

L119def Performed (records : List WorkRecord) (s : Subject) (a : Activity) : Prop :=

要求存在匹配目标和活动的实际记录；有效性另行检查。

L120  ∃ record ∈ records, record.target = s ∧ record.activity = a

Performed要求存在目标和活动完全匹配的记录；它本身不检查理由内容。

L122/- The old scope condition remains available without conflating scope with content completion. -/

说明后续定义或结果：保留受所属主体和适用性条件限制的记录覆盖接口。

L123def ReflexiveScope (owner : Nat) (rules : List Principle) (records : List WorkRecord) : Prop :=

保留受所属主体和适用性条件限制的记录覆盖接口。

L124  ∀ rule ∈ rules, ∀ s, s.owner = owner → rule.applicable s → Performed records s rule.activity

对指定所有者的对象，每项适用的登记规则都须有对应活动记录。

L126/- A record uses a registered principle on the same resolvable target, question, reasons and limits,

说明后续定义或结果：检查登记与适用性、对象身份、目标方法内容、非空对应理由、限度及规则语义一致性。

L127and its result must actually follow that principle's method. A negative result can satisfy this relation. -/

说明后续定义或结果：检查登记与适用性、对象身份、目标方法内容、非空对应理由、限度及规则语义一致性。

L128structure ValidApplication (rules : List Principle) (rule : Principle) (s : Subject)

检查登记与适用性、对象身份、目标方法内容、非空对应理由、限度及规则语义一致性。

L129    (record : WorkRecord) : Prop where

以下证明字段确认这条特定工作记录是rule对s的有效适用。

L130  registered : rule ∈ rules

要求记录采用的规则属于此登记表。

L131  applicable : rule.applicable s

要求同一规则对待评对象适用。

L132  usedIdentity : record.usedPrinciple = rule.key

核对记录所用原则标识与该规则确切标识相等。

L133  targetIdentity : record.target = s

检查工作记录针对的正是对象s。

L134  targetResolved : TargetResolved rules s

要求记录对象能在同一规则登记表中解析。

L135  activityIdentity : record.activity = rule.activity

检查记录活动正是该规则约束的活动。

L136  inquiryIdentity : record.inquiry = rule.inquiry s

检查记录问题等于该规则为s指定的问题。

L137  inquiryTarget : record.inquiry.target = s

另检查问题自身针对s，而非无关对象。

L138  targetContent : TargetContentResolved rules record.inquiry

检查问题中的方法属于已解析的登记目标。

L139  reasonsIdentity : record.reasons = rule.reasons s

检查记录理由等于该规则为s指定的理由。

L140  reasonsNonempty : record.reasons ≠ []

要求该记录至少包含一项实际理由。

L141  reasonTargets : ∀ reason ∈ record.reasons, reason.target = s

要求每个记录理由都针对同一对象s。

L142  limitsIdentity : record.limits = rule.limits s

检查记录限度等于该规则对s的限度。

L143  followsMeaning : rule.meaning record.inquiry record.reasons record.limits record.outcome

要求记录结果满足该规则对问题、理由和限度的实际含义关系。

L145/- The registered normative interface requires contentful application, not just activity labels. -/

说明后续定义或结果：要求登记一致，且每条适用规则对同主体对象都有有效应用记录；仍是模型遵守条件。

L146def Reflexive (owner : Nat) (rules : List Principle) (records : List WorkRecord) : Prop :=

要求登记一致，且每条适用规则对同主体对象都有有效应用记录；仍是模型遵守条件。

L147  RegistryCoherent rules ∧

Reflexive首先要求原则登记无歧义。

L148  ∀ rule ∈ rules, ∀ s, s.owner = owner → rule.applicable s →

然后量化每项登记规则及其适用的自有对象。

L149    ∃ record ∈ records, ValidApplication rules rule s record

对每次上述适用，都须存在通过全部ValidApplication内容检查的记录。

L151theorem Reflexive.toScope {owner : Nat} {rules : List Principle} {records : List WorkRecord}

由完整反身性抽取目标和活动记录覆盖，不再保留内容有效性细节。

L152    (h : Reflexive owner rules records) : ReflexiveScope owner rules records := by

假设完整内容性Reflexive履责，推出较弱的仅范围覆盖。

L153  intro rule hr s hs ha

为范围义务取已登记规则、自有对象及其适用前提。

L154  obtain ⟨record, hm, hv⟩ := h.2 rule hr s hs ha

用完整Reflexive履责取得实际列表记录及ValidApplication证明。

L155  exact ⟨record, hm, hv.targetIdentity, hv.activityIdentity⟩

保留该记录的成员关系、目标一致与活动一致，证明Performed。

L157theorem noSelfExemption (owner : Nat) (rules : List Principle) (records : List WorkRecord)

把完整反身规范应用于已登记且适用的同主体对象，得到工作记录。

L158    (h : Reflexive owner rules records) (rule : Principle) (hr : rule ∈ rules)

要求完整Reflexive履责及该规则实际属于登记表。

L159    (s : Subject) (hs : s.owner = owner) (ha : rule.applicable s) :

还要求目标所有者匹配且该规则对其适用。

L160    Performed records s rule.activity := h.toScope rule hr s hs ha

把导出的范围义务应用于这些前提，得到该目标的活动已经记录。

L162def localMethod : MethodDraft := ⟨[0],[0]⟩

只测试零并声明零点范围。

L164def inquiryFor (s : Subject) : Inquiry :=

形成询问根据，应用询问适用性，修订询问零与一范围的根据，其他对象询问合规。

L165  match s with

根据对象的过程阶段选择问题，仍以同一对象为目标。

L166  | .process _ _ .formation => ⟨s, .formationBasis, [0], localMethod⟩

对形成阶段，考察覆盖输入0的方法形成根据。

L167  | .process _ _ .application => ⟨s, .applicability, [0], localMethod⟩

对应用阶段，考察局部方法在输入0上的适用性。

L168  | .process _ _ .revision => ⟨s, .revisionGrounds, [0,1], localMethod⟩

对修订阶段，考察将同一局部方法范围扩至输入0和1的根据。

L169  | _ => ⟨s, .conformity, [0], localMethod⟩

对系统或原则自身，在局部范围{0}内考察符合性。

L171/- These original inquiry inputs do not depend on which work records happen to be present. -/

说明后续定义或结果：按问题提供目的、范围、观察；修订问题另含未测试输入失败的程序反例。

L172def sourceReasonContents : QuestionKind → List ReasonContent

按问题提供目的、范围、观察；修订问题另含未测试输入失败的程序反例。

L173  | .formationBasis => [.purpose [0], .declaredScope [0], .observation 0 true]

形成理由陈述目的{0}、声明范围{0}及0处为真的观察。

L174  | .applicability | .conformity => [.declaredScope [0], .observation 0 true]

适用性与符合性使用已声明局部范围及同一0处观察。

L175  | .revisionGrounds => [.purpose [0,1], .declaredScope [0], .observation 0 true,

修订理由要求{0,1}，同时承认原声明范围为{0}且仅有0处观察。

L176      .counterexample .onlyAtZero 1]

加入onlyAtZero程序在输入1处的具体修订反例。

L178def reasonsFor (s : Subject) : List ReasonObject :=

把选定理由内容逐项绑定到同一问题目标。

L179  (sourceReasonContents (inquiryFor s).kind).map fun content => ⟨content.identifier,s,content⟩

将每项源理由与类别引用和同一对象s包装，保留实际内容。

L181/- The application-specific evaluator examines actual scope and sample/counterexample contents.

说明后续定义或结果：按实际理由和方法范围计算结果；已通过当前测试却在请求输入失败的程序使修订主张不充分。

L182It is a finite inferential method, not a universal standard for empirical or value claims. -/

说明后续定义或结果：按实际理由和方法范围计算结果；已通过当前测试却在请求输入失败的程序使修订主张不充分。

L183def assessInquiry (question : Inquiry) (reasons : List ReasonObject) (limits : List Nat) : AssessmentResult :=

按实际理由和方法范围计算结果；已通过当前测试却在请求输入失败的程序使修订主张不充分。

L184  let contents := reasons.map ReasonObject.content

提取理由内容，以检查目的、范围、观察与反例实质。

L185  if limits ≠ question.currentMethod.claimedScope then .undetermined else

提供的限度若不同于待考察方法声明范围，则返回未确定。

L186  match question.kind with

检查限度后，评估提出的具体问题种类。

L187  | .formationBasis =>

进入形成根据的评估分支。

L188      if ReasonContent.purpose question.requestedScope ∈ contents ∧

要求存在覆盖问题所请求输入的目的理由。

L189          ReasonContent.declaredScope limits ∈ contents ∧ question.requestedScope = limits

还要求明确限度声明，且请求范围等于声明范围。

L190      then .supportedWithinScope else .undetermined

仅上述内容检查通过时形成评估才为域内有支持，否则未确定。

L191  | .applicability | .conformity =>

对适用性和符合性问题采用相同局部检查。

L192      if question.requestedScope.all (fun n => limits.contains n) then

首先检查每个请求输入都在所提供限度内。

L193        if ReasonContent.declaredScope limits ∈ contents ∧

在限度内，要求理由明确声明同一范围。

L194            ReasonContent.observation 0 true ∈ contents ∧ question.requestedScope = [0]

还要求0处为真的观察，以及请求范围恰为[0]。

L195        then .supportedWithinScope else .undetermined

通过这些局部检查得到域内有支持；证据不完整则未确定。

L196      else .notApplicable

请求输入超出所提供限度时，判为不适用。

L197  | .revisionGrounds =>

进入修订根据分支，寻找实际范围反例。

L198      if ReasonContent.purpose question.requestedScope ∈ contents ∧

要求理由把修订后请求范围陈述为预期目的。

L199          ReasonContent.declaredScope limits ∈ contents ∧

要求旧限度明确出现于声明范围理由中。

L200          ReasonContent.observation 0 true ∈ contents ∧

要求原先输入0上的成功观察。

L201          contents.any (fun reason => match reason with

在提供的理由内容中寻找满足以下具体检查的反例。

L202            | .counterexample program input => question.requestedScope.contains input &&

反例输入必须属于新请求范围。

L203                question.currentMethod.accepts program &&

但该反例程序必须通过当前方法的已测试输入。

L204                !(program.run input)

同一程序必须在反例输入处失败。

L205            | _ => false)

其他种类理由不能自行满足该反例搜索。

L206      then .insufficient else .undetermined

发现测试与范围之间的反例缺口时判为不足；缺少这些内容则未确定。

L208def finiteMethodResult (activity : Activity) (question : Inquiry)

生成保留测试输入并采用请求范围；评估执行依赖理由内容的问题检查。

L209    (reasons : List ReasonObject) (limits : List Nat) : WorkOutcome :=

把同一理由和限度传入按活动区分的结果函数。

L210  match activity with

在生成草案与评估问题之间选择。

L211  | .generation => .generated ⟨question.currentMethod.testedInputs,question.requestedScope⟩

生成保留方法已测试输入，却提出问题请求范围；不认证正确性。

L212  | .assessment => .assessment (assessInquiry question reasons limits)

评估使用此问题实际理由与限度计算assessInquiry。

L214def finiteMethodMeaning (activity : Activity) (question : Inquiry)

以结果等于明示有限算法的计算值定义语义，不预设检查成功。

L215    (reasons : List ReasonObject) (limits : List Nat) (outcome : WorkOutcome) : Prop :=

接收待检查是否遵循该活动方法的具体记录结果。

L216  outcome = finiteMethodResult activity question reasons limits

结果恰等于计算出的finiteMethodResult时才遵循该方法。

L218def ownSubjects (owner : Nat) : List Subject :=

枚举所属系统、两条登记原则及各原则的三个过程阶段。

L219  [.system owner, .principle owner 0, .principle owner 1,

把系统自身及其两个原则身份纳入自有对象。

L220   .process owner 0 .formation, .process owner 0 .application, .process owner 0 .revision,

把原则0的形成、应用和修订分别列为对象。

L221   .process owner 1 .formation, .process owner 1 .application, .process owner 1 .revision]

也纳入原则1的全部三个阶段，总计九个自有对象。

L223/- Applying an existing rule is not a generation event in this application. -/

说明后续定义或结果：此应用的生成规则排除应用阶段过程，保留其他对象。

L224def generationEligible : Subject → Bool

此应用的生成规则排除应用阶段过程，保留其他对象。

L225  | .process _ _ .application => false

在该应用模型中，把应用既有原则视为不适用生成活动。

L226  | _ => true

其余已表示对象种类均适用生成活动。

L228def generatingRule (owner : Nat) : Principle where

登记零号生成原则，带局部方法、问题、理由及受限适用条件。

L229  key := ⟨owner,0⟩

以此所有者的局部标识0登记生成原则。

L230  activity := .generation

令该规则约束生成工作。

L231  declaredMethod := localMethod

为生成规则指定测试与范围均为[0]的局部草案。

L232  applicable s := s ∈ ownSubjects owner ∧ generationEligible s = true

生成适用性同时要求属于该所有者九个对象及符合生成资格。

L233  inquiry := inquiryFor

用inquiryFor提供与对象阶段对应的实际问题。

L234  reasons := reasonsFor

用reasonsFor提供原始且与目标相连的理由内容。

L235  limits _ := [0]

对每个对象，生成规则均保留[0]这一限度。

L236  meaning := finiteMethodMeaning .generation

要求生成结果符合finiteMethodResult的生成分支。

L238def assessingRule (owner : Nat) : Principle where

登记一号评估原则，按明确有限语义评估全部枚举自身对象。

L239  key := ⟨owner,1⟩

以不同的局部标识1登记评估原则。

L240  activity := .assessment

令该规则约束评估工作。

L241  declaredMethod := localMethod

评估原则声明相同的局部[0]/[0]方法契约。

L242  applicable s := s ∈ ownSubjects owner

评估对该所有者全部九个对象适用。

L243  inquiry := inquiryFor

给评估规则指定同一按阶段区分的问题函数。

L244  reasons := reasonsFor

为其评估指定同一原始目标相关理由。

L245  limits _ := [0]

保留[0]作为评估规则声明的限度。

L246  meaning := finiteMethodMeaning .assessment

要求评估结果等于评估函数的实际结果。

L248def ownRules (owner : Nat) : List Principle := [generatingRule owner, assessingRule owner]

返回两个身份不同的生成和评估原则。

L250/- Recorded verdicts are stated separately from the evaluator, so agreement has to be proved. -/

说明后续定义或结果：构造拟记录草案和范围支持或不充分结果，随后与实际算法计算核对。

L251def statedOutcome (activity : Activity) (s : Subject) : WorkOutcome :=

构造拟记录草案和范围支持或不充分结果，随后与实际算法计算核对。

L252  match activity with

按活动选择独立陈述的记录结果。

L253  | .generation => .generated ⟨(inquiryFor s).currentMethod.testedInputs,(inquiryFor s).requestedScope⟩

记录中的生成草案保留测试输入并采用问题请求范围。

L254  | .assessment => .assessment (match (inquiryFor s).kind with

评估记录按问题种类选取所陈述判定，此处不调用assessInquiry。

L255      | .revisionGrounds => .insufficient

修订问题记录为不足。

L256      | _ => .supportedWithinScope)

其余已表示问题记录为域内有支持。

L258def recordFor (rule : Principle) (s : Subject) : WorkRecord :=

用提供的规则与对象构造记录；登记成员关系与内容有效性仍需后续ValidApplication证明。

L259  ⟨rule.key,s,rule.activity,rule.inquiry s,rule.reasons s,rule.limits s,statedOutcome rule.activity s⟩

用此规则的标识、问题、理由和限度构造记录，但结果采用独立陈述值。

L261theorem reasonsFor_nonempty (s : Subject) : reasonsFor s ≠ [] := by

穷尽对象与阶段，证明每个具体问题理由非空。

L262  cases s with

对每种对象检查理由列表非空。

L263  | system owner => simp [reasonsFor, inquiryFor, sourceReasonContents]

系统问题使用符合性理由，包含范围与观察条目。

L264  | principle owner id => simp [reasonsFor, inquiryFor, sourceReasonContents]

原则问题同样具有非空的范围与观察列表。

L265  | process owner id phase => cases phase <;> simp [reasonsFor, inquiryFor, sourceReasonContents]

各过程阶段分别化为实际非空的形成、应用或修订理由列表。

L267theorem reasonsFor_target (s : Subject) : ∀ reason ∈ reasonsFor s, reason.target = s := by

从理由列表的映射构造证明各理由都指向同一对象。

L268  intro reason h

取已知属于此对象构造理由列表的任意理由。

L269  obtain ⟨content, _, rfl⟩ := List.mem_map.mp h

反解map构造取得源内容，将理由替换为附有目标标识的包装。

L270  rfl

该包装的目标按构造就是s，故目标等式自反成立。

L272theorem inquiryFor_target (s : Subject) : (inquiryFor s).target = s := by

逐构造器验证生成问题保留目标身份。

L273  cases s with

分别检查系统、原则和过程对象的问题目标。

L274  | system owner => rfl

系统问题构造时就以同一系统为目标。

L275  | principle owner id => rfl

原则问题同样保留同一原则目标。

L276  | process owner id phase => cases phase <;> rfl

每个过程阶段均以原过程对象为问题目标。

L278/- This proof includes the actual negative revision evaluation for both principle identities. -/

说明后续定义或结果：计算各对象和阶段的评估及生成，证明记录预期结果与算法一致，包含不充分结果。

L279theorem ownContentEvaluates (activity : Activity) (s : Subject) :

计算各对象和阶段的评估及生成，证明记录预期结果与算法一致，包含不充分结果。

L280    statedOutcome activity s = finiteMethodResult activity (inquiryFor s) (reasonsFor s) [0] := by

要求独立陈述结果等于对该对象问题、理由及[0]限度的实际计算。

L281  cases activity with

分别检查生成草案与评估判定的结果等式。

L282  | generation => rfl

两个生成定义构造完全相同的测试输入与请求范围草案。

L283  | assessment =>

对评估，现须将所陈述判定与实际评估函数核对。

L284      cases s with

按对象种类区分有限评估检查。

L285      | system owner => rfl

系统的符合性内容计算得到所陈述的域内有支持判定。

L286      | principle owner id => rfl

原则的符合性内容计算得到同一域内有支持判定。

L287      | process owner id phase => cases phase <;> rfl

形成与应用计算为有支持；修订因程序在0通过而在1失败计算为不足。

L289theorem ownRegistryCoherent (owner : Nat) : RegistryCoherent (ownRules owner) := by

利用局部编号零和一不同，证明登记键无歧义。

L290  intro p hp q hq hkey

取两项登记原则，并假设其标识相等。

L291  simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hp hq

把两项登记成员关系限定为实际生成规则或评估规则。

L292  rcases hp with rfl | rfl <;> rcases hq with rfl | rfl

检查由此产生的四种具体规则配对。

L293  · rfl

两者都是生成规则时，原则相等直接成立。

L294  · have bad := congrArg PrincipleKey.localId hkey; contradiction

生成标识0不能等于评估标识1；提取localId得到矛盾。

L295  · have bad := congrArg PrincipleKey.localId hkey; contradiction

反向混合配对要求localId 1=0，也不可能。

L296  · rfl

两者都是评估规则时，原则相等直接成立。

L298theorem ownTargetResolved (owner : Nat) (s : Subject) (hs : s ∈ ownSubjects owner) :

核实九个枚举对象都能解析到实际登记主体或原则。

L299    TargetResolved (ownRules owner) s := by

从ownSubjects选出的对象必须可在该所有者实际登记表中解析。

L300  simp only [ownSubjects, List.mem_cons, List.not_mem_nil, or_false] at hs

把成员前提hs展开为九个具体自有对象。

L301  rcases hs with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;>

逐个处理九个对象，保持其原所有者和原则编号。

L302    simp [TargetResolved, ownRules, generatingRule, assessingRule]

为每个目标标识找到匹配的生成或评估登记项。

L304theorem ownTargetContent (owner : Nat) (s : Subject) (hs : s ∈ ownSubjects owner) :

核实每个问题的方法与登记目标的局部方法一致。

L305    TargetContentResolved (ownRules owner) (inquiryFor s) := by

要求所选对象的问题考察其自身登记声明的方法。

L306  simp only [ownSubjects, List.mem_cons, List.not_mem_nil, or_false] at hs

再次依据实际成员前提枚举九个具体对象。

L307  rcases hs with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;>

分别检查系统、原则和各阶段对象的目标方法对应。

L308    simp [TargetContentResolved, inquiryFor, ownRules, generatingRule, assessingRule]

两项登记规则都声明localMethod，恰与inquiryFor为每个枚举目标指定的方法相同。

L310theorem ownRecordValid (owner : Nat) (rule : Principle) (hr : rule ∈ ownRules owner)

综合身份、理由目标、范围、登记及实际计算，验证每个适用记录。

L311    (s : Subject) (ha : rule.applicable s) :

假设所选登记规则对对象s适用。

L312    ValidApplication (ownRules owner) rule s (recordFor rule s) := by

证明具体recordFor rule s满足每个ValidApplication字段。

L313  have hs : s ∈ ownSubjects owner := by

首先从适用性推出s属于该所有者对象列表。

L314    simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hr

用登记成员关系将rule限定为两个自有规则之一。

L315    rcases hr with rfl | rfl

分别处理生成与评估的适用条件。

L316    · exact ha.1

生成适用性的第一个合取项就是自有对象成员关系。

L317    · exact ha

评估适用性恰为该自有对象成员关系。

L318  have hq : rule.inquiry = inquiryFor := by

确立此实际规则以inquiryFor作为问题函数。

L319    simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hr

将登记规则成员关系化为生成或评估，以检查问题字段。

L320    rcases hr with rfl | rfl <;> rfl

两个可能规则的问题字段都定义为inquiryFor。

L321  have hg : rule.reasons = reasonsFor := by

确立所选规则用reasonsFor提供理由。

L322    simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hr

检查理由前，再次将规则限定为两个实际登记项。

L323    rcases hr with rfl | rfl <;> rfl

两个登记项都恰提供reasonsFor。

L324  have hl : rule.limits s = [0] := by

确立该规则对s的限度恰为[0]。

L325    simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hr

检查所选规则限度前，先解析登记成员关系。

L326    rcases hr with rfl | rfl <;> rfl

两个自有规则都保留[0]作为限度。

L327  have hm : rule.meaning = finiteMethodMeaning rule.activity := by

确立所选规则的含义是其自身活动对应的结果函数。

L328    simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hr

解析登记成员关系，以检查生成或评估的含义。

L329    rcases hr with rfl | rfl <;> rfl

两种情形中，规则含义都是按其活动实例化的finiteMethodMeaning。

L330  refine ⟨hr, ha, rfl, rfl, ownTargetResolved owner s hs, rfl, rfl, ?_, ?_, rfl, ?_, ?_, rfl, ?_⟩

用登记与适用前提、记录一致性和已解析目标构造ValidApplication，余下检查问题、理由及计算含义。

L331  · change (rule.inquiry s).target = s

余下的问题目标义务针对该规则对s的实际问题。

L332    rw [hq]; exact inquiryFor_target s

将规则问题换为inquiryFor，用其目标保持定理证明目标为s。

L333  · change TargetContentResolved (ownRules owner) (rule.inquiry s)

余下方法一致性义务检查该规则问题的登记目标。

L334    rw [hq]; exact ownTargetContent owner s hs

改写为inquiryFor，使用具体自有目标的方法解析定理。

L335  · change rule.reasons s ≠ []

把记录理由非空化为该规则提供理由非空。

L336    rw [hg]; exact reasonsFor_nonempty s

把这些理由改写为reasonsFor，应用其非空列表定理。

L337  · change ∀ reason ∈ rule.reasons s, reason.target = s

把理由目标一致性化为每项提供理由都针对s。

L338    rw [hg]; exact reasonsFor_target s

改写为reasonsFor，使用其目标保持构造定理。

L339  · change rule.meaning (rule.inquiry s) (rule.reasons s) (rule.limits s) (statedOutcome rule.activity s)

最后义务比较独立陈述结果与该规则实际问题、理由、限度及含义。

L340    rw [hm, hq, hg, hl]

代入含义、问题、理由和[0]限度这四项已证一致性。

L341    exact ownContentEvaluates rule.activity s

用ownContentEvaluates证明记录结果等于实际方法结果。

L343def completeOwnWork (owner : Nat) : List WorkRecord :=

为九个对象构造记录，仅在生成适用时加入生成记录。

L344  (ownSubjects owner).flatMap fun s =>

通过连接分配给每个自有对象的记录，构造完整日志。

L345    if generationEligible s then [recordFor (generatingRule owner) s, recordFor (assessingRule owner) s]

符合生成资格的对象同时获得生成记录和评估记录。

L346    else [recordFor (assessingRule owner) s]

应用阶段对象仅获评估记录，与生成的明确适用限制一致。

L348theorem assessingRecord_member (owner : Nat) (s : Subject) (hs : s ∈ ownSubjects owner) :

证明每个对象的评估记录进入完整工作列表。

L349    recordFor (assessingRule owner) s ∈ completeOwnWork owner := by

陈述该自有对象的评估记录属于构造出的完整日志。

L350  apply List.mem_flatMap.mpr

使用flatMap成员规则：选取其分配列表包含目标记录的对象。

L351  refine ⟨s,hs,?_⟩

选择同一s及其给定的自有对象成员证明hs。

L352  cases generationEligible s <;> simp

无论生成是否适用，分配列表都包含s的评估记录。

L354theorem generatingRecord_member (owner : Nat) (s : Subject) (hs : s ∈ ownSubjects owner)

在明确生成适用条件下证明生成记录存在。

L355    (hg : generationEligible s = true) : recordFor (generatingRule owner) s ∈ completeOwnWork owner := by

声称完整日志包含生成记录前，除自有成员关系外还要求生成资格。

L356  exact List.mem_flatMap.mpr ⟨s,hs,by simp [hg]⟩

选择s的flatMap分支；hg使该分支包含所需生成记录。

L358theorem completeOwnWork_reflexive (owner : Nat) :

综合登记一致、记录存在及内容有效性，建立具体非空反身模型。

L359    Reflexive owner (ownRules owner) (completeOwnWork owner) := by

陈述实际双规则登记表与构造工作日志满足完整内容性反身要求。

L360  refine ⟨ownRegistryCoherent owner, ?_⟩

提供已证登记一致性，余下逐一证明适用对象的内容性覆盖。

L361  intro rule hr s _ ha

取实际登记规则和适用对象；适用性自身将提供所需自有成员关系。

L362  refine ⟨recordFor rule s, ?_, ownRecordValid owner rule hr s ha⟩

选择recordFor rule s及已证内容有效性，仅留下它属于完整日志的义务。

L363  simp only [ownRules, List.mem_cons, List.not_mem_nil, or_false] at hr

把规则成员关系解析为生成或评估登记项。

L364  rcases hr with rfl | rfl

按这两个实际规则情形分别证明记录成员关系。

L365  · exact generatingRecord_member owner s ha.1 ha.2

对生成，ha提供自有成员关系和资格，使其记录属于完整日志。

L366  · exact assessingRecord_member owner s ha

对评估，ha直接提供其记录所需的自有成员关系。

L368theorem ownAssessmentPerformed (owner : Nat) (s : Subject) (hs : s ∈ ownSubjects owner) :

为列表中的自身对象抽取已构造评估记录。

L369    Performed (completeOwnWork owner) s .assessment :=

陈述同一完整工作日志中存在针对s的评估活动。

L370  ⟨recordFor (assessingRule owner) s, assessingRecord_member owner s hs, rfl, rfl⟩

以s的评估记录、已证日志成员关系及确切目标活动一致性作为Performed见证。

L372def applicationRule : Principle :=

把评估规则限定到一个应用阶段对象，并给出可解析键。

L373  { assessingRule 0 with key := ⟨0,0⟩, applicable := fun s => s = .process 0 0 .application }

把评估规则限制为原则0的应用过程，标识为(0,0)。

L375def applicationWork : List WorkRecord := [recordFor applicationRule (.process 0 0 .application)]

储存该单一应用对象的完整评估记录。

L377theorem applicationWork_reflexive : Reflexive 0 [applicationRule] applicationWork := by

核实单规则及其记录在受限适用范围内满足完整内容有效反身性。

L378  constructor

将单项登记表一致性与唯一适用对象覆盖分开。

L379  · intro p hp q hq _

取单项登记表中任意两规则；成员关系已确定两者，因此无需使用标识相等前提。

L380    simp only [List.mem_singleton] at hp hq

单项成员关系使两规则都等于applicationRule。

L381    rw [hp,hq]

代入这两个一致性证明两规则相等。

L382  · intro rule hr s _ ha

为单项应用登记表中的规则取一个适用对象。

L383    simp only [List.mem_singleton] at hr

用单项成员关系确认该规则是applicationRule。

L384    subst rule

在覆盖义务中把rule替换为确切的applicationRule。

L385    change s = .process 0 0 .application at ha

展开适用性，得到s恰为所有者0的原则0应用过程。

L386    subst s

把s替换为该确切过程，固定工作目标。

L387    refine ⟨recordFor applicationRule (.process 0 0 .application), by simp [applicationWork], ?_⟩

选择applicationWork唯一记录并证明成员关系，余下检查内容有效性。

L388    refine ⟨by simp, rfl, rfl, rfl, ?_, rfl, rfl, rfl, ?_, rfl, ?_, ?_, rfl, ?_⟩

填入直接成立的登记、适用与记录一致性字段，留下目标解析、理由及计算结果检查。

L389    · exact ⟨applicationRule, by simp, rfl⟩

目标标识解析为单项登记表中的applicationRule自身。

L390    · exact ⟨applicationRule, by simp, rfl, rfl⟩

同一登记规则提供问题实际考察的localMethod。

L391    · exact reasonsFor_nonempty _

由reasonsFor_nonempty得应用问题理由非空。

L392    · exact reasonsFor_target _

每项应用理由都针对该确切应用过程对象。

L393    · change statedOutcome .assessment (.process 0 0 .application) = finiteMethodResult .assessment (inquiryFor (.process 0 0 .application)) (reasonsFor (.process 0 0 .application)) [0]

余下含义义务是所陈述应用评估与实际有限计算结果相等。

L394      exact ownContentEvaluates .assessment _

用ownContentEvaluates确认应用阶段评估的该等式。

L396theorem applicabilityRetained (owner : Nat) (rules : List Principle) (records : List WorkRecord) :

从完整反身性得到范围覆盖，证明条件与析取等价，并给无系统评估记录的有效受限实例。

L397    (Reflexive owner rules records → ReflexiveScope owner rules records) ∧

第一条保留完整内容性反身要求推出范围覆盖的结论。

L398    (ReflexiveScope owner rules records ↔

第二条把条件性范围覆盖改述为二择一义务。

L399      ∀ rule ∈ rules, ∀ s, s.owner = owner → (¬ rule.applicable s ∨ Performed records s rule.activity)) ∧

对每个自有对象和登记规则，要么规则不适用，要么其活动已有记录。

L400    (Reflexive 0 [applicationRule] applicationWork ∧

具体单项应用日志在受限规则下满足完整反身要求。

L401      ¬ Performed applicationWork (.system 0) .assessment) := by

但同一日志不含系统自身评估，因为该规则对系统自身不适用。

L402  classical

对可能不可判定的适用谓词使用古典分情形讨论。

L403  refine ⟨Reflexive.toScope, ?_, applicationWork_reflexive, ?_⟩

提供一般范围投影和具体受限见证，留下等价关系与缺失系统记录证明。

L404  · constructor

证明适用性或已履行改述的两个方向。

L405    · intro h rule hr s hs

假设条件性范围覆盖，固定登记规则与自有对象。

L406      by_cases ha : rule.applicable s

按该确切规则是否对该对象适用分情况。

L407      · exact Or.inr (h rule hr s hs ha)

适用时，覆盖义务提供已记录活动，满足右析取项。

L408      · exact Or.inl ha

不适用时，该否定适用事实满足左析取项。

L409    · intro h rule hr s hs ha

反向证明假设该析取，并给出对自有对象的实际适用性。

L410      exact (h rule hr s hs).resolve_left (not_not_intro ha)

用ha排除不适用分支，得到所需已记录活动。

L411  · rintro ⟨record, hm, ht, _⟩

假设存在系统评估，提取列表记录及目标一致性。

L412    simp only [applicationWork, List.mem_singleton] at hm

单项applicationWork迫使该记录就是应用过程记录。

L413    subst record

把声称的系统评估记录替换为唯一过程记录。

L414    cases ht

其过程目标不可能等于系统目标，与假设的记录一致性矛盾。

L416end CoreReader.Agency

关闭当前命名空间。