leanified/CoreReader/Engineering/SelfApplication.lean

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

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

展开 Lean 与逐行解读 · 203 行

Lean逐行解读

L1import CoreReader.Engineering.Values

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

L2import CoreReader.Engineering.Reflection

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

L4namespace CoreReader.Engineering

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

L6open CoreReader.Adopted

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

L8inductive ReviewObject | activity | commitment (principle : CoreCommitment) | priority | evolutionMethod

ReviewObject 区分活动、带 Core 原则参数的承诺、优先性和演化方法。

L9  | generationRule | assessmentRule

在同一对象类型中加入实际生成规则与评估规则对象。

L10  deriving DecidableEq, Repr

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

L12abbrev ReviewCase := Candidate × Nat

检查案例是所选 Candidate 与自然数规模组成的二元组。

L14def generationApplies (_ : ReviewObject) (phase : CoreReader.Agency.Phase) : Prop :=

生成适用性忽略对象身份，仅依赖生命周期阶段。

L15  phase ≠ .application

生成恰在 application 以外适用，即形成与修订阶段。

L17def assessmentApplies (_ : ReviewObject) (_ : CoreReader.Agency.Phase) : Prop := True

评估适用性忽略两个参数，对所有对象、所有阶段均为真。

L19def ruleObject : CoreReader.Agency.Activity → ReviewObject

把每种实际活动映射为其对应的方法检查对象。

L20  | .generation => .generationRule

生成活动对应 generationRule。

L21  | .assessment => .assessmentRule

评估活动对应 assessmentRule。

L23/- These inputs test the current reflection functions themselves. Size 10 has

注释说明这些探针针对当前反思函数本身，并引入规模 10 案例。

L24an actual supporting sample; size 5 removes that sample while retaining the

注释比较规模 10 的真实初始样本与规模 5 对该样本的移除。

L25requested claim. The domain batch predictor is not used in this method test. -/

注释保留请求主张，并区分此实际规则测试与领域批处理预测器。

L26def ruleProbe (activity : CoreReader.Agency.Activity) (point : ReviewCase) :

按活动和候选项、规模二元组，为实际方法构造探针。

L27    Reflection.Input ReviewCase ReviewObject where

探针样本类型为 ReviewCase，目标类型为 ReviewObject。

L28  target := ⟨0, ruleObject activity, .revision⟩

所有者固定为 0，阶段固定为修订，对象由活动选取。

L29  contract := ⟨fun _ => true, if point.2 = 10 then [point] else [], [point]⟩

内层测试恒通过；仅规模 10 提供初始样本，claimed 始终含此案例。

L30  requested := [point]

即使初始样本列表为空，仍保留此案例为请求案例。

L31  reasons := ["retain the proposed scope and distinguish actual samples from an empty test set"]

提供非空理由，说明范围保留及空初始列表的区分。

L32  basis := True

探针依据为 True；该字段不提供额外经验论证。

L34def generationRuleTest

generationRuleTest 测试传入的 method 函数，允许实际替换函数。

L35    (method : Reflection.Input ReviewCase ReviewObject → Reflection.Outcome ReviewCase)

方法必须把此精确反思输入类型映射到对应结果类型。

L36    (point : ReviewCase) : Bool :=

对给定案例，返回布尔合约结果。

L37  let input := ruleProbe .generation point

为同一案例构造生成探针。

L38  method input == .generated input.requested input.requested

要求结果恰等于以 requested 为测试和范围的生成结果。

L40def assessmentRuleTest

assessmentRuleTest 按局部区分样本的合约检查显式传入的评估器。

L41    (method : Reflection.Input ReviewCase ReviewObject → Reflection.Verdict)

待评估方法接收此精确输入类型并返回 Verdict。

L42    (point : ReviewCase) : Bool :=

每个候选项、规模案例得到布尔通过或失败结果。

L43  method (ruleProbe .assessment point) ==

把实际方法对评估探针的判定与下行期望判定比较。

L44    (if point.2 = 10 then .supportedWithinScope else .noSupportingSample)

规模 10 期望支持，其余规模期望 noSupportingSample；这是局部合约，不是普遍经验义务。

L46/- A candidate revision supplies the previously missing empty-sample check.

注释介绍加入缺失的空初始列表检查的修订候选。

L47It is kept distinct from the current evaluator and is not silently adopted. -/

注释明确把候选与当前已安装评估器分开。

L48def sampleAwareAssessment (input : Reflection.Input ReviewCase ReviewObject) : Reflection.Verdict :=

在同一输入类型上定义独立的评估器修订候选。

L49  if input.contract.tested.isEmpty then .noSupportingSample else Reflection.evaluate input

先对空初始测试列表返回无支持样本，对非空列表再调用当前 evaluate。

L51/- The method under criticism is the activity's own static batch forecast. Its

注释将 evolutionMethod 分支介绍为对此活动自身静态批次数预测的批评。

L52contract is checked at its original size and at the credible runtime change. -/

注释比较原规模与可信改变后的运行规模。

L53def objectTest (object : ReviewObject) (point : ReviewCase) : Bool :=

objectTest 按实际检查对象选取操作性布尔测试。

L54  match object with

匹配对象构造子以选择其特定测试。

L55  | .activity => decide (Meets currentContinuing.required (currentContinuing.profiles point.1))

对活动，判定所选设计指标是否满足当前必要需求。

L56  | .commitment principle => safeguardExperiment principle true point.1

对原则承诺，在所选设计上运行对应的已启用保障实验。

L57  | .priority => decide (EvolutionPriority currentContinuing point.1)

对优先性，判定 currentContinuing 中的实际 EvolutionPriority 命题。

L58  | .evolutionMethod => staticBatch 21 point.2 == liveBatch 21 point.2

对演化方法，比较 21 项任务在此规模下的静态与实时批次数预测。

L59  | .generationRule => generationRuleTest Reflection.generate point

对生成规则，把实际 Reflection.generate 函数传入测试。

L60  | .assessmentRule => assessmentRuleTest Reflection.evaluate point

对评估规则，把实际 Reflection.evaluate 函数传入测试。

L62def reviewObjects (chosen : Candidate) : List ReviewObject :=

按所选设计构造有限检查对象列表。

L63  [.activity] ++ coreCommitments.map ReviewObject.commitment ++

纳入活动以及五个 Core 承诺，沿用其原有标识。

L64    (if chosen = .evolvable then [.priority] else []) ++

仅在选择 evolvable 时纳入优先性对象。

L65    [.evolutionMethod, .generationRule, .assessmentRule]

始终纳入批处理方法及两个实际规则对象。

L67def requestedCases (chosen : Candidate) : CoreReader.Agency.Phase → List ReviewCase

请求案例依赖所选设计及生命周期阶段。

L68  | .formation | .application => [(chosen, 10)]

形成和应用阶段仅请求规模 10。

L69  | .revision => [(chosen, 10), (chosen, 5)]

修订阶段将请求列表扩展为同一设计的规模 10 与 5。

L71def reviewReasons (object : ReviewObject) (phase : CoreReader.Agency.Phase) : List String :=

逐对象、逐阶段构造理由字符串。

L72  let content := match object with

按实际对象构造子选择第一条理由。

L73    | .activity => "actual order, safety, latency and retention requirements of this activity"

活动理由指出其顺序、安全、延迟与保留需求。

L74    | .commitment principle => criticismFor principle

原则承诺复用由同一原则索引的批评字符串。

L75    | .priority => "credible design revision, successor and agent paths, necessary requirements and concrete costs"

优先性理由指出证据、维护者路径、需求及成本。

L76    | .evolutionMethod => "the same batch forecast at its recorded size and the proposed runtime size"

方法理由比较同一预测在记录规模与提议运行规模下的结果。

L77    | .generationRule => "the actual generator must retain its input's requested tests and scope"

生成器理由要求保留请求测试与范围。

L78    | .assessmentRule => "the actual evaluator's acceptance depends on whether its input has supporting samples"

评估器理由陈述此处对是否存在支持样本的局部要求。

L79  [content, match phase with

返回对象特定理由，再附上阶段特定理由。

L80    | .formation => "identify this object's purpose and the conditions of its initial contract"

形成阶段要求辨明对象目的与初始合约条件。

L81    | .application => "apply that contract to the currently selected design in this continuing activity"

应用阶段指出当前所选设计与持续活动。

L82    | .revision => "examine the proposed wider input scope and retain any counterexample"]

修订阶段要求检查更广输入并保留反例。

L84/- The recorded verdict is independent of the evaluator: the revision of the

注释强调 statedReview 的记录独立于 evaluate 定义。

L85batch method is explicitly reported as a counterexample; other current checks

注释指出批处理方法修订被明确记录为反例。

L86are reported supported only in the scope that will be checked below. -/

注释把其他支持记录限于后续证明检查的有限范围。

L87def statedReview (chosen : Candidate) (activity : CoreReader.Agency.Activity)

statedReview 独立记录给定设计及活动的结果。

L88    (object : ReviewObject) (phase : CoreReader.Agency.Phase) : Reflection.Outcome ReviewCase :=

记录同时依赖对象与阶段，类型为精确的反思结果类型。

L89  match activity with

区分生成记录与评估记录。

L90  | .generation => .generated (requestedCases chosen phase) (requestedCases chosen phase)

生成把该阶段的请求列表记录于两个输出字段。

L91  | .assessment => .assessed (match object, phase with

评估按对象与阶段选取记录判定，不调用 evaluate。

L92    | .evolutionMethod, .revision | .assessmentRule, .revision => .counterexample

批处理方法或评估规则的修订被明确记录为反例。

L93    | _, _ => .supportedWithinScope)

其余对象、阶段的评估均记录为 supportedWithinScope。

L95/- The basis is not a free approval flag. Each inquiry requires the facts

注释把 basis 介绍为对象特定事实内容，而非不受限制的批准标记。

L96relevant to its own object; a counterexample can ground criticism rather than

注释说明反例能支持对同一对象的批评。

L97the truth of the original method's broader claim. -/

注释否认这种批评支持能建立方法原本的更广主张。

L98def reviewBasis (chosen : Candidate) : ReviewObject → CoreReader.Agency.Phase → Prop

reviewBasis 给出对象特定命题；后续为两个普通设计检查证明。

L99  | .activity, _ => ActivityScope currentContinuing.activity ∧

活动检查要求实际活动的范围条件。

L100      Meets currentContinuing.required (currentContinuing.profiles chosen)

还要求所选指标满足当前必要需求。

L101  | .commitment principle, _ => ReasonRelevant principle (reasonFor principle) chosen

原则检查要求该同一原则理由对当前选择具有事实相关性。

L102  | .priority, _ => PriorityConditions currentContinuing ∧ ¬ HasThreat currentContinuing .evolvable

优先性检查要求当前适用条件及 evolvable 不受威胁。

L103  | .evolutionMethod, .revision =>

修订分支为批处理方法检查提供更强依据。

L104      staticBatch 21 10 = liveBatch 21 10 ∧ staticBatch 21 5 ≠ liveBatch 21 5

要求规模 10 成功，且规模 5 存在实际不相等。

L105  | .evolutionMethod, _ => staticBatch 21 10 = liveBatch 21 10

其他批处理方法阶段仅要求规模 10 的相等。

L106  | .generationRule, _ =>

生成器依据包含对实际函数内容的正反测试。

L107      generationRuleTest Reflection.generate (chosen, 10) = true ∧

真实生成器必须在所选设计、规模 10 上通过。

L108      generationRuleTest (fun _ => .generated [] []) (chosen, 10) = false

输出为空的生成器必须在同一案例上失败。

L109  | .assessmentRule, .revision =>

评估规则修订要求两个案例的对比。

L110      assessmentRuleTest Reflection.evaluate (chosen, 10) = true ∧

当前评估器必须在规模 10 上通过局部样本合约测试。

L111      assessmentRuleTest Reflection.evaluate (chosen, 5) = false

它必须在规模 5、初始列表为空时不满足该合约。

L112  | .assessmentRule, _ => assessmentRuleTest Reflection.evaluate (chosen, 10) = true

其他评估规则阶段仅要求规模 10 的正例。

L114def selfModel (chosen : Candidate) : Reflection.Model ReviewCase ReviewObject where

selfModel 为所选设计以这些案例、对象实例化反思模型。

L115  owner := 0

把模型所有者设为 0。独立的 self 关系要求自身目标与之匹配；原始 Model.input 仍可接收并保留任意所有者的目标。

L116  objects := reviewObjects chosen

采用依赖选择的实际对象列表。

L117  contracts object := ⟨objectTest object, [(chosen, 10)], [(chosen, 10)]⟩

每个外层合约采用对应 objectTest，初始测试与声称列表均含规模 10。

L118  requested _ := requestedCases chosen

所有对象共享所选设计的阶段特定 requestedCases。

L119  reasons := reviewReasons

采用实际的对象、阶段理由构造函数。

L120  basis := reviewBasis chosen

采用实质的对象、阶段依据谓词。

L121  generationApplies := generationApplies

安装实际生成适用性函数。

L122  assessmentApplies := assessmentApplies

安装实际评估适用性函数。

L123  recorded := statedReview chosen

采用独立陈述的记录，后续由 currentSelfRecords 验证。

L125/- The named normative object and its finite rationale test are deliberately

注释开始区分实际规范对象与其有限理由实验。

L126distinct: a supported rationale experiment is not proof of universal correctness.

注释否认理由实验成功能证明规范普遍正确。

L127The same commitment identifier controls adoption, reasons and reflection. -/

注释说明采纳、理由与反思之间预期保持同一标识的连接。

L128theorem reviewIdentity (chosen : Candidate) (object : ReviewObject)

对每个设计与对象，reviewIdentity 确认输入各部分的身份。

L129    (phase : CoreReader.Agency.Phase) :

该身份关系对所有生命周期阶段成立。

L130    ((selfModel chosen).input ⟨0, object, phase⟩).target.object = object ∧

输入的目标对象恰为传入对象。

L131    ((selfModel chosen).input ⟨0, object, phase⟩).contract.test = objectTest object ∧

其测试恰为同一对象的 objectTest。

L132    ((selfModel chosen).input ⟨0, object, phase⟩).requested = requestedCases chosen phase ∧

其请求列表恰为所选设计在此阶段的列表。

L133    ((selfModel chosen).input ⟨0, object, phase⟩).reasons = reviewReasons object phase ∧

其理由恰对应同一对象及阶段。

L134    ((selfModel chosen).input ⟨0, object, phase⟩).basis = reviewBasis chosen object phase :=

其依据恰为同一设计、对象、阶段的谓词。

L135  ⟨rfl, rfl, rfl, rfl, rfl⟩

五项身份均由定义反身性成立，不是经验验证。

L137theorem currentSelfRecords (chosen : Candidate)

currentSelfRecords 检查所选设计的记录。

L138    (ordinary : chosen = .presentSimple ∨ chosen = .evolvable) :

前提把 chosen 限为 presentSimple 或 evolvable，排除 maximal。

L139    (selfModel chosen).follows := by

结论为 follows，包含每条适用记录的实际解释要求。

L140  rcases ordinary with rfl | rfl

拆开普通设计前提，分别代入两种设计。

L141  all_goals

将后续证明步骤应用于两个设计目标。

L142    intro activity object phase member applies

引入任意活动、对象、阶段及成员、适用性前提。

L143    cases activity <;> cases object <;> cases phase

穷尽活动、对象、阶段的全部构造子。

L144    all_goals first

对所有剩余目标，依序尝试下列局部策略。

L145      | rename_i principle; cases principle

存在承诺参数时，将其命名为 principle 并拆分五种构造子。

L146      | skip

否则保留目标，不要求存在 principle 参数。

L147    all_goals simp_all [Reflection.interpret, Reflection.Model.input,

用实际解释和输入构造化简全部目标与假设。

L148      Reflection.evaluate, selfModel, statedReview, reviewObjects, coreCommitments,

展开评估器、模型、陈述记录及有限对象列表。

L149      requestedCases, reviewReasons, criticismFor, objectTest, safeguardExperiment,

展开请求案例、理由、对象测试与保障实验。

L150      generationApplies, assessmentApplies, generationRuleTest, assessmentRuleTest,

展开两个适用性谓词与实际规则测试定义。

L151      ruleProbe, Reflection.generate,

展开内层方法探针及实际生成器。

L152      reviewBasis, ReasonRelevant, reasonFor, HasThreat, burdens, ConcreteThreat, cost,

展开依据、相关性以及具体威胁、成本谓词。

L153      EvolutionPriority, PriorityConditions, JustifiedDeparture, currentContinuing,

展开优先性、适用性、偏离与固定当前语境。

L154      Continuing, ActivityScope, Meets, profile, normalRequirements, initialGrounds,

展开活动范围、必要需求、指标与初始证据。

L155      ContinuingCapability, continuingActivity, maintainers, changePath,

展开持续能力、维护者列表及实际改变路径。

L156      changeWork, abstractionComplexity, credible, CredibleDirection, articulateGround,

展开工作量、复杂度以及所述方向的可信性。

L157      supportGround, normalLimits, staticBatch, liveBatch, batchCount, orderedUnique,

展开证据支持、限制、批次数算术与保序输出。

L158      sortedUnique, sortValues, insertOrdered, List.eraseDups]

展开有限检查所需的排序与去重辅助函数。

L159    all_goals decide

在分情况与化简后判定所有剩余封闭有限命题。

L161theorem currentSelfApplication (chosen : Candidate)

currentSelfApplication 为所选设计导出反身性。

L162    (ordinary : chosen = .presentSimple ∨ chosen = .evolvable) :

保留显式的两种普通设计前提。

L163    reflexivitySpecification (selfModel chosen).rules (selfModel chosen).self

规范采用同一 selfModel 的规则与自身目标谓词。

L164      (selfModel chosen).performed :=

其执行关系也取自同一模型。

L165  Reflection.recordedReflexivity _ (currentSelfRecords chosen ordinary)

把实际证明的 currentSelfRecords 作为前提应用通用 recordedReflexivity 定理。

L167/- The activity's own assessment method passes its old observation while the

注释指出活动的批处理评估方法在旧观测上成功。

L168expanded input exposes its actual failed forecast. Neither applying the method

注释说明扩展输入揭示预测失败，并开始限定自应用的作用。

L169to itself nor generating a broader candidate makes the failed forecast true. -/

注释否认自应用或生成更广候选会使失败预测变真。

L170theorem actualSelfCriticism (chosen : Candidate) :

actualSelfCriticism 对任意设计成立，展示批处理方法的有限失败。

L171    objectTest .evolutionMethod (chosen, 10) = true ∧

旧规模 10 的批处理测试通过。

L172    objectTest .evolutionMethod (chosen, 5) = false ∧

规模 5 的批处理测试失败。

L173    Reflection.evaluate ((selfModel chosen).input ⟨0, .evolutionMethod, .revision⟩) = .counterexample ∧

实际修订评估器对同一方法对象报告反例。

L174    statedReview chosen .generation .evolutionMethod .revision =

指定该方法修订的独立生成记录。

L175      .generated [(chosen, 10), (chosen, 5)] [(chosen, 10), (chosen, 5)] ∧

两个生成列表均含同一设计的规模 10 与 5。

L176    staticBatch 21 5 ≠ liveBatch 21 5 := by

结论还保留底层批次数预测的不相等。

L177  refine ⟨?_, ?_, ?_, rfl, by decide⟩

构造五个合取项；生成项由反身性、算术不等由可判定性完成，留下三项检查。

L178  · change (staticBatch 21 10 == liveBatch 21 10) = true

把第一证明目标显化为规模 10 的布尔相等测试。

L179    decide

计算此封闭的规模 10 相等式。

L180  · change (staticBatch 21 5 == liveBatch 21 5) = false

把下一目标显化为规模 5 的布尔测试失败。

L181    decide

计算此封闭的规模 5 失败结果。

L182  · simp [Reflection.evaluate, Reflection.Model.input, selfModel, requestedCases,

为反例目标展开评估器及实际模型输入。

L183      objectTest, staticBatch, liveBatch, batchCount]

化简对象测试和批次数算术以完成反例计算。

L185/- The objects use the very functions in the adopted rules, and the same

注释强调检查对象与已采纳规则实际使用函数的身份一致。

L186applicability functions. Assessment applies in all three phases; generation

注释保留相同适用性函数及全部阶段的评估。

L187applies to formation and revision, including formation/revision of these rules. -/

注释把生成规则自身的形成、修订纳入生成适用阶段。

L188theorem ownRuleIdentity (chosen : Candidate) (activity : CoreReader.Agency.Activity)

ownRuleIdentity 将每个设计、活动连接到实际规则对象与实现。

L189    (phase : CoreReader.Agency.Phase) :

连接对所有阶段陈述，无论生成是否在那里适用。

L190    ruleObject activity ∈ (selfModel chosen).objects ∧

该活动的方法对象实际属于模型对象列表。

L191    ((selfModel chosen).rule activity).meaning = Reflection.interpret activity ∧

模型规则含义恰为实际 interpret activity 函数。

L192    ((selfModel chosen).input ⟨0, ruleObject activity, phase⟩).contract.test =

同一规则对象的输入取得其实际合约测试。

L193      objectTest (ruleObject activity) ∧

该测试为按此相同方法对象索引的 objectTest。

L194    (selfModel chosen).generationApplies (ruleObject activity) phase =

比较模型在此对象、阶段的生成适用性。

L195      generationApplies (ruleObject activity) phase ∧

它等于声明的 generationApplies 对同一参数的值。

L196    (selfModel chosen).assessmentApplies (ruleObject activity) phase =

比较模型在此对象、阶段的评估适用性。

L197      assessmentApplies (ruleObject activity) phase := by

它等于 assessmentApplies 对这些相同参数的值。

L198  refine ⟨?_, rfl, rfl, rfl, rfl⟩

四个函数、字段相等由反身性完成，仅留下实际对象成员资格。

L199  cases activity <;> simp [ruleObject, selfModel, reviewObjects]

拆分活动并计算实际检查对象列表中的成员资格。

L201/- Changing the actual generator changes its object's result despite keeping

注释说明即使对象名称不变，替换生成器内容仍会改变结果。

L202the object name. The evaluator really approves an empty initial sample set;

注释记录实际评估器在初始样本为空时接受；请求案例仍受检查。

L203its own revision review reports that bounded defect instead of a self-proof. -/

注释把外层自身检查界定为报告这一有界局部合约缺陷，而非证明自身普遍有效。

L204theorem ownRuleContentVariation (chosen : Candidate) :

ownRuleContentVariation 为每个设计提供对函数内容敏感的正反案例。

L205    generationRuleTest Reflection.generate (chosen, 10) = true ∧

当前生成器通过规模 10 的保留测试。

L206    generationRuleTest (fun _ => .generated [] []) (chosen, 10) = false ∧

输出为空的生成器未通过同一测试。

L207    assessmentRuleTest Reflection.evaluate (chosen, 10) = true ∧

当前评估器在有规模 10 样本时通过局部样本合约。

L208    assessmentRuleTest Reflection.evaluate (chosen, 5) = false ∧

它在规模 5、初始样本列表为空时未满足该合约。

L209    Reflection.evaluate ((selfModel chosen).input ⟨0, .assessmentRule, .revision⟩) = .counterexample ∧

实际评估规则对象的外层修订评估报告反例。

L210    generationApplies .generationRule .formation ∧

生成适用于自身规则对象的形成。

L211    generationApplies .generationRule .revision ∧

它也适用于自身规则对象的修订。

L212    ¬ generationApplies .generationRule .application ∧

生成不适用于该对象的应用阶段。

L213    (∀ phase, assessmentApplies .assessmentRule phase) := by

评估对自身规则对象在每个阶段均适用。

L214  simp [generationRuleTest, assessmentRuleTest, ruleProbe, Reflection.generate,

在各合取项中展开实际方法测试、探针与生成器。

L215    Reflection.evaluate, Reflection.Model.input, selfModel, requestedCases,

展开评估器、实际输入、模型与请求案例。

L216    objectTest, generationApplies, assessmentApplies]

化简对象测试及两个适用性谓词，完成有限检查。

L218theorem proposedRuleRevision (chosen : Candidate) :

proposedRuleRevision 比较当前与候选评估器，并检查一次适用性变更。

L219    assessmentRuleTest Reflection.evaluate (chosen, 5) = false ∧

当前评估器不满足局部空初始样本合约。

L220    assessmentRuleTest sampleAwareAssessment (chosen, 5) = true ∧

独立的 sampleAwareAssessment 候选通过该规模 5 合约。

L221    assessmentRuleTest sampleAwareAssessment (chosen, 10) = true ∧

候选也保留规模 10 的正例结果。

L222    ((selfModel chosen).rule .generation).applicable ⟨0, .generationRule, .revision⟩ ∧

当前生成规则适用于自身生成规则对象的修订。

L223    ¬ (({ selfModel chosen with generationApplies := fun _ _ => False }).rule .generation).applicable

另一个将 generationApplies 改为恒假的模型更新消除了此适用性。

L224      ⟨0, .generationRule, .revision⟩ := by

被消除的适用性恰针对所有者 0、generationRule 与修订阶段。

L225  simp [assessmentRuleTest, sampleAwareAssessment, ruleProbe, Reflection.evaluate,

展开局部测试、候选评估器、探针与当前评估器。

L226    Reflection.Model.rule, Reflection.Model.self, selfModel, reviewObjects,

展开实际规则、自身目标语义与模型对象成员资格。

L227    generationApplies]

化简生成适用性完成合取；此处未安装任一候选变更。

L229end CoreReader.Engineering

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