leanified/CoreReader/Integration.lean

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

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

展开 Lean 与逐行解读 · 473 行

Lean逐行解读

L1import CoreReader.Agency

导入CoreReader.Agency及其依赖。

L2import CoreReader.Choice

导入CoreReader.Choice及其依赖。

L4namespace CoreReader.Integration

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

L5open CoreReader.Logic CoreReader.Evidence CoreReader.Agency CoreReader.Choice

使列出的命名空间可通过省略前缀的名称引用。

L7/- Canonical articulation preserves the actual assessment contents of each facet. -/

说明后续定义或结果：从同一主张的已检查非空面向清单构造规范表达及Grounds；适用性按清单成员定义。

L8theorem canonicalGrounds {W : Type} (claim : Claim W) (facets : List (Facet W))

从同一主张的已检查非空面向清单构造规范表达及Grounds；适用性按清单成员定义。

L9    (hne : facets ≠ []) (checked : ∀ f ∈ facets, f.claim = claim ∧ FacetDischarged f) :

假设方面列表非空，且每个方面都针对claim并已履责。

L10    Grounds claim canonicalArticulation (fun f => f ∈ facets) facets := by

用各方面自身内容构造的表述建立Grounds，以列表成员关系作为适用谓词。

L11  exact ⟨hne, fun _ h => h, fun f hf =>

提供非空性及按成员定义直接成立的覆盖，再逐个检查列表方面。

L12    ⟨(checked f hf).1, canonicalArticulated f (checked f hf).2,

对每个方面，用checked确立同一主张，并由履责得到非空表述。

L13      canonicalFacetArticulated f, (checked f hf).2⟩⟩

补上该表述的确切内容对应及已给履责证明。

L15theorem canonicalGroundsForSingleton {W : Type} (f : Facet W) (checked : FacetDischarged f) :

对单个已检查面向构造Grounds，适用性只限于该面向本身。

L16    Grounds f.claim canonicalArticulation (fun g => g = f) [f] := by

对单个已履责方面，使恰好该方面对其自身主张适用。

L17  refine ⟨by simp, (by intro g hg; cases hg; simp), ?_⟩

证明单项列表非空，且每个等于f的方面都在其中，留下逐方面内容检查。

L18  intro g hg

取已知属于单项列表[f]的任意方面g。

L19  simp only [List.mem_singleton] at hg

单项成员关系把hg化为等式g=f。

L20  subst g

把g替换为同一个已履责方面f。

L21  exact ⟨rfl, canonicalArticulated f checked, canonicalFacetArticulated f, checked⟩

用相同主张、构造表述的可表达性、确切方面内容匹配及checked履责完成Grounds字段。

L23/- A mode selects whether a system applies or waives the modeled governance rule. -/

说明后续定义或结果：区分执行模型标准与豁免标准两种模式，它们决定实际政策判断。

L24inductive Mode | apply | waive

区分执行模型标准与豁免标准两种模式，它们决定实际政策判断。

L25  deriving DecidableEq, Repr

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

L27/- The four hypotheses vary algorithm and governance independently for the same assessed system. -/

说明后续定义或结果：世界由两个候选实现之一及两个治理模式之一组成，是封闭四世界模型。

L28abbrev World := Candidate × Mode

世界由两个候选实现之一及两个治理模式之一组成，是封闭四世界模型。

L30def actual : World := (.identity, .apply)

指定恒等实现和执行标准模式作为实际世界。

L32/- A method's form and its possible executable realizations belong to one object. -/

说明后续定义或结果：把可修订形式身份与依赖世界的实际实现绑定。

L33structure Method where

把方法形式的种类与版本绑定到随世界变化的实现；仅此结构不证明该形式可修订。

L34  form : Form

保存该方法的形式种类与版本。

L35  realize : World → Implementation

为每个候选与治理世界指定该同一方法的实际实现。

L37/- System fields identify the owner, its method, its current principle form, policy and work. -/

说明后续定义或结果：把主体、方法、原则形式、治理选择和应用要求绑定成系统。

L38structure System where

把主体、方法、原则形式、治理选择和应用要求绑定成系统。

L39  owner : Nat

标识该系统采用其原则与工作记录的所有者。

L40  method : Method

保存系统的方法形式及随世界变化的实现。

L41  principleForm : Form

保存系统自身原则的当前形式。

L42  governance : World → Mode

选择该系统在各世界采用还是豁免治理要求。

L43  requirements : Requirements

固定用于评估该系统实现的输入、输出、预算和价值要求。

L45def policyFor : Mode → Policy

执行模式使用开放政策，豁免模式使用无扩展价值的政策。

L46  | .apply => openPolicy

采用治理时选择重视扩展且允许修订的openPolicy。

L47  | .waive => neutralPolicy

豁免治理时选择缺少所需扩展价值取向的neutralPolicy。

L49def workFor (owner : Nat) : Mode → List WorkRecord

执行模式提供内容已检查的自身工作记录，豁免模式不提供记录。

L50  | .apply => completeOwnWork owner

采用治理时，为此所有者提供完整内容性工作日志。

L51  | .waive => []

豁免治理时，同一所有者的工作日志为空。

L53def System.policy (s : System) (w : World) : Policy := policyFor (s.governance w)

按同一系统的治理选择决定政策。

L54def System.rules (s : System) (_w : World) : List Principle := ownRules s.owner

使用属于该系统主体的登记生成及评估规则。

L55def System.work (s : System) (w : World) : List WorkRecord := workFor s.owner (s.governance w)

按该主体治理模式选取实际工作记录清单。

L57def actualSystem : System where

构造主体零、版本零方法及原则、依候选实现、依世界治理和恒等要求的实际系统。

L58  owner := 0

给共享实际系统分配所有者0。

L59  method := ⟨⟨.method, 0⟩, fun w => implementation w.1⟩

使用版本0的方法形式，由世界的候选分量选择其实例实现。

L60  principleForm := ⟨.principle, 0⟩

把该系统当前原则形式设为原则版本0。

L61  governance := Prod.snd

从世界第二分量读取治理方式，与实现候选独立。

L62  requirements := identityRequirements

用identityRequirements评估同一方法。

L64def systemCapability (s : System) : Claim World :=

要求该系统实际方法在自身请求输入上满足自身期望输出。

L65  fun w => ∀ n, s.requirements.inputs n → (s.method.realize w).run n = s.requirements.expected n

声称该系统实现的方法在每个必需输入上满足指定输出。

L67def systemBudget (s : System) : Claim World :=

按该系统预算检查同一实际实现的成本。

L68  fun w => (s.method.realize w).cost ≤ s.requirements.budget

声称同一实现方法的成本满足该系统自身预算。

L70def systemObservation (s : System) : Record World :=

记录该系统实际实现是否在零输入满足其期望输出。

L71  ⟨fun w => decide ((s.method.realize w).run 0 = s.requirements.expected 0), true⟩

记录测试为true：同一方法在0处的输出等于该处所需输出。

L73def systemHeld (s : System) : Theory World :=

同时持有同一系统的能力与预算主张。

L74  union (singleton (systemCapability s)) (singleton (systemBudget s))

系统同时持有实际输出能力主张和预算主张。

L76inductive Question | correctOutput | affordable

定义上下文使用的输出正确与成本可承担两个问题。

L77  deriving DecidableEq, Repr

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

L79def systemContext (s : System) : Context World Question :=

以同系统观察为假设、能力及预算为含义；范围要求零在域内且采用执行模式。

L80  ⟨singleton (Compatible [systemObservation s]),

情境假设与该系统实际0输入观察相容。

L81    (fun q => match q with | .correctOutput => systemCapability s | .affordable => systemBudget s),

把correctOutput解释为该系统能力，把affordable解释为预算满足。

L82    fun w => (s.method.realize w).domain 0 ∧ w.2 = .apply⟩

把可容许范围限于定义域包含0且采用治理的世界。

L84abbrev capability := systemCapability actualSystem

简写实际系统的参数化输出能力主张。

L85abbrev observation := systemObservation actualSystem

简写实际系统的零输入观察记录。

L86abbrev held := systemHeld actualSystem

简写实际系统同时持有的能力与预算理论。

L87abbrev context := systemContext actualSystem

简写实际系统的问题、假设与范围上下文。

L89/- The output observation identifies the algorithm, without identifying its independently varied governance mode. -/

说明后续定义或结果：计算零点观察只识别恒等候选，而不限制治理模式。

L90theorem observationIdentifies (w : World) : Compatible [observation] w ↔ w.1 = .identity := by

计算零点观察只识别恒等候选，而不限制治理模式。

L91  rcases w with ⟨candidate, mode⟩

把候选算法与独立变化的治理模式分开。

L92  cases candidate <;> simp [Compatible, observation, systemObservation, actualSystem,

逐一检查两个实际候选是否符合观察中的0输出测试为真。

L93    implementation, identityRequirements, identityImpl, successorImpl]

identity返回所需0而successor返回1，因此只有identity匹配，与治理方式无关。

L95theorem capabilityActual : capability actual := fun _ _ => rfl

通过约简证明实际恒等实现满足每个请求的恒等输出。

L97theorem observedCapability : Supports [observation] capability := by

在封闭模型中，由候选识别和已知恒等行为得到全请求输入能力。

L98  intro w hw

取与同一观察相容的任意世界。

L99  have hid := (observationIdentifies w).1 hw

用observationIdentifies推出该世界算法候选是identity。

L100  rcases w with ⟨candidate, mode⟩

分离世界的算法和治理分量以便替换。

L101  change candidate = .identity at hid

把推出的identity等式直接改述为候选变量的等式。

L102  subst candidate

把候选算法换成identity，保留其治理模式。

L103  exact fun _ _ => rfl

按定义，identity在每个输入上的运行等于所需输出，故证明此世界能力。

L105def capabilityFacet : Facet World := .empirical [observation] (fun _ => True) capability (fun _ => True)

把实际观察及能力主张组成经验面向，范围不限、不确定性条件恒真。

L107theorem capabilityFacetChecked : FacetDischarged capabilityFacet := by

提供实际兼容见证、封闭模型支持证明及平凡不确定性条件。

L108  exact ⟨⟨actual, (observationIdentifies actual).2 rfl, trivial⟩,

以actual作为方面无限制范围内的相容世界，避免空世界履责。

L109    (fun w hw _ => observedCapability w hw), fun _ _ => trivial⟩

用observedCapability证明每个相容世界的支持；所述不确定性条件为平凡真。

L111theorem capabilityGrounds : Grounds capability canonicalArticulation

为精确对应的能力面向构造规范Grounds。

L112    (fun f => f = capabilityFacet) [capabilityFacet] :=

只令实际输出能力方面适用，使用其自身单项证据包。

L113  canonicalGroundsForSingleton capabilityFacet capabilityFacetChecked

把单项Grounds构造应用于已经履责的能力方面。

L115theorem actualAdmissible : Admissible held context actual := by

证明实际恒等执行世界同时满足能力、预算、观察假设以及治理和输入域范围。

L116  refine ⟨(modelsUnion _ _ _).2 ⟨(modelsSingleton _ _).2 capabilityActual,

构造实际世界可容许见证，先证明共同持有的两项主张；能力项使用capabilityActual。

L117    (modelsSingleton _ _).2 (by change 1 ≤ 1; decide)⟩,

所持预算主张计算为实际成本1满足预算1。

L118    (modelsSingleton _ _).2 ((observationIdentifies actual).2 rfl), trivial, rfl⟩

补上与0处观察相容、0属于定义域以及actual采用apply模式。

L120theorem jointConsistent : Consistent held context :=

从已证明的实际可接受世界推出一致性。

L121  consequenceConsistency held context ⟨actual, actualAdmissible⟩

以actual及其可容许证明作为必需非空见证，应用语义后果一致性定理。

L123/- The current method/principle forms, judgments, rules and own work are read from this very system and world. -/

说明后续定义或结果：组合该系统生成政策、上下文一致性、完整内容有效反身性及当前方法和原则形式。

L124def Charter (s : System) (w : World) : Prop :=

组合该系统生成政策、上下文一致性、完整内容有效反身性及当前方法和原则形式。

L125  Generative (s.policy w) ∧ Consistent (systemHeld s) (systemContext s) ∧

Charter要求该系统实际政策具有生成取向，且共同持有判断在情境内一致。

L126  Reflexive s.owner (s.rules w) (s.work w) ∧

它还要求该系统实际工作日志满足完整自有规则反身要求。

L127  (s.policy w).current s.method.form ∧ (s.policy w).current s.principleForm

方法形式与原则形式均须在同一政策下属于当前形式。

L129theorem charterChecked : Charter actualSystem actual :=

组合开放政策计算结果、实际一致性和内容已验证自身工作模型。

L130  ⟨⟨Or.inl rfl, fun _ _ => trivial⟩, jointConsistent, completeOwnWork_reflexive 0, rfl, rfl⟩

组合openPolicy价值取向与可修订性、jointConsistent、完整自有日志及两个当前版本0形式。

L132/- Revision adds a supported input-specific assertion about the same system's realized method. -/

说明后续定义或结果：在原持有理论中增加同系统零输入输出事实。

L133def revisedHeld : Theory World := union held

在原持有理论中增加同系统零输入输出事实。

L134  (singleton (fun w => (actualSystem.method.realize w).run 0 = actualSystem.requirements.expected 0))

增加具体断言：同一方法在输入0处满足所需输出。

L136def initialSnapshot : Snapshot World Question := ⟨held, context, 0⟩

以修订标识零保存实际理论及上下文。

L137def revisedSnapshot : Snapshot World Question := ⟨revisedHeld, context, 1⟩

以同一上下文和标识一保存扩充理论。

L139theorem revisionKeepsConsistency :

增加事实后保留同一章程和可接受模型，并要求如实报告修订。

L140    Charter actualSystem actual ∧ Consistent revisedHeld context ∧

实际系统保留Charter，增加该有支持断言后revisedHeld仍一致。

L141    TruthfulReport initialSnapshot revisedSnapshot true ∧

把已识别修订报告为true，满足单向变化报告条件。

L142    ¬ TruthfulReport initialSnapshot revisedSnapshot false := by

把同一修订报告为false，违反该条件。

L143  refine ⟨charterChecked, consequenceConsistency revisedHeld context ⟨actual,

保留charterChecked，以actual作为具体可容许见证证明修订后一致性。

L144    (modelsUnion _ _ _).2 ⟨actualAdmissible.1, (modelsSingleton _ _).2 rfl⟩,

actual满足原所持主张及新增0输入输出断言。

L145    actualAdmissible.2⟩, (fun _ => rfl), ?_⟩

保留actual既有情境与范围证明，并验证true报告，仅余拒绝false报告。

L146  intro h

假设变化后的快照能以report=false满足TruthfulReport。

L147  have bad := h (Or.inr (by decide))

修订编号0和1不同，因此假设的义务迫使false=true。

L148  cases bad

排除不可能的布尔等式，拒绝隐瞒修订。

L150/- A claim about this system's method is assessed as its owner's system claim. -/

说明后续定义或结果：要求该系统评估记录及其自身能力主张的匹配Grounds。

L151def OwnCapabilityDuty (s : System) (w : World) (facets : List (Facet World)) : Prop :=

要求该系统评估记录及其自身能力主张的匹配Grounds。

L152  Performed (s.work w) (.system s.owner) .assessment ∧

OwnCapabilityDuty首先要求实际评估记录针对与系统所有者一致的系统对象。

L153  Grounds (systemCapability s) canonicalArticulation (fun f => f ∈ facets) facets

还要求全部所列适用方面为该系统输出能力提供同主张Grounds。

L155theorem ownCapabilityGrounded :

组合实际内容有效自身评估记录、观察支持能力Grounds及能力结论。

L156    OwnCapabilityDuty actualSystem actual [capabilityFacet] ∧ capability actual := by

陈述实际系统自身能力义务已履行，且其声称能力实际成立。

L157  refine ⟨⟨?_, ?_⟩, capabilityActual⟩

直接提供capabilityActual，留下系统评估记录与对应Grounds。

L158  · exact ownAssessmentPerformed 0 (.system 0) (by simp [ownSubjects])

以完整日志对系统0的评估作为自有系统工作见证。

L159  · exact canonicalGrounds capability [capabilityFacet] (by simp)

从非空单项能力方面列表构造Grounds。

L160      (by intro f hf; simp only [List.mem_singleton] at hf; cases hf; exact ⟨rfl, capabilityFacetChecked⟩)

单项列表唯一方面具有确切目标主张及已证履责。

L162/- This cost observation is true of both algorithms but does not discriminate their output behavior. -/

说明后续定义或结果：记录同系统实现成本至多二；两个候选均通过。

L163def costAllowanceRecord : Record World :=

记录同系统实现成本至多二；两个候选均通过。

L164  ⟨fun w => decide ((actualSystem.method.realize w).cost ≤ 2), true⟩

记录实现成本至多2；两个算法候选都满足这个较弱成本观察。

L166def unsupportedCapabilityFacet : Facet World :=

试图只凭宽松成本观察支持同一输出能力。

L167  .empirical [costAllowanceRecord] (fun _ => True) capability (fun _ => True)

尝试仅以成本证据支持输出能力，不另加限制范围或不确定性条件。

L169theorem costCompatibleWithFailure : Compatible [costAllowanceRecord] (.successor, .apply) := by

计算后继执行世界符合成本观察，却不满足恒等输出。

L170  intro r hr

取单项成本观察列表中的一条记录。

L171  simp only [List.mem_singleton] at hr

单项成员关系确认该记录就是costAllowanceRecord。

L172  subst r

把r替换为实际成本记录。

L173  rfl

successor成本为2，因此记录的至多2观察计算为true。

L175theorem costDoesNotSupportOutput : ¬ Supports [costAllowanceRecord] capability := by

把假定支持应用于兼容后继反世界及零输入，导出矛盾。

L176  intro h

假设成本观察在每个相容世界都支持输出能力。

L177  have bad := h (.successor, .apply) costCompatibleWithFailure 0 trivial

将假设应用于相容successor世界及输入0，得到错误等式1=0。

L178  cases bad

排除不可能的输出等式，反驳仅成本支持。

L180theorem unsupportedGrounds : ¬ Grounds capability canonicalArticulation

从假定Grounds抽取错误面向支持义务，并由成本反模型否定。

L181    (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet] := by

检验使该仅成本能力方面适用的单项证据包。

L182  intro h

假设这个不足的单项证据包仍满足Grounds。

L183  have discharged := (h.2.2 unsupportedCapabilityFacet (by simp)).2.2.2

从Grounds前提提取实际仅成本能力方面的FacetDischarged。

L184  exact costDoesNotSupportOutput (fun w hw => discharged.2.1 w hw trivial)

其支持条款会推出仅成本Supports，与costDoesNotSupportOutput矛盾。

L186/- Five separately adopted requirements govern distinct operations; the mode does not give them priority over one another. -/

说明后续定义或结果：标识五项治理承诺，每项有分别解释的理由与结果。

L187inductive Commitment | generation | consistency | reflexivity | grounds | choice

标识五项治理承诺，每项有分别解释的理由与结果。

L188  deriving DecidableEq, Repr

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

L190/- A Grounds policy governs arbitrary claims, articulations and applicable facets, rather than only one capability claim. -/

说明后续定义或结果：执行模式仅许可Grounds成立的主张包，豁免模式许可所有包。

L191def groundsPermission (mode : Mode) (claim : Claim World) (a : Facet World → Articulation World)

执行模式仅许可Grounds成立的主张包，豁免模式许可所有包。

L192    (applicable : Facet World → Prop) (facets : List (Facet World)) : Prop :=

接收针对同一主张与表述的任意适用谓词和方面包。

L193  match mode with

按治理模式选择许可规则。

L194  | .apply => Grounds claim a applicable facets

apply模式只许可实际满足Grounds的证据包。

L195  | .waive => True

waive模式不检查Grounds，许可所有证据包。

L197def GroundsProvision (mode : Mode) : Prop :=

表达一般规范：所有获许可的主张、表达、适用面与清单组合都必须具有Grounds。

L198  ∀ claim a applicable facets, groundsPermission mode claim a applicable facets →

对任意实际主张、表述族和方面包，条款约束该模式许可的所有包。

L199    Grounds claim a applicable facets

每个被许可包都必须满足其自身对应Grounds义务。

L201theorem groundsProvisionMeaning (mode : Mode) : GroundsProvision mode ↔ mode = .apply := by

证明执行模式履行一般规范，而具体无支持成本包反驳豁免模式。

L202  cases mode with

分别检查apply与waive模式的一般条款。

L203  | apply => exact ⟨fun _ => rfl, fun _ _ _ _ _ h => h⟩

apply模式的许可本就是Grounds，因此返回已给证明即可满足一般条款。

L204  | waive =>

对waive模式，需要证明无限制许可违反一般条款。

L205    constructor

证明waive模式下两侧均不成立的等价关系两个方向。

L206    · intro h

假设该模式豁免检查时一般条款仍成立。

L207      exact False.elim (unsupportedGrounds (h capability canonicalArticulation

把该普遍假设应用于实际不足的能力证据包，将与unsupportedGrounds矛盾。

L208        (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet] trivial))

提供确切单项适用谓词和包；豁免许可为真，迫出无效Grounds结果。

L209    · intro h; cases h

反向蕴涵以前提waive=apply开始，这是不可能的构造器等式。

L211/- The consistency policy checks a whole same-context theory, not isolated judgments. -/

说明后续定义或结果：执行模式要求拟议理论和上下文一致，豁免模式无条件许可。

L212def consistencyPermission (mode : Mode) (t : Theory World) (c : Context World Question) : Prop :=

执行模式要求拟议理论和上下文一致，豁免模式无条件许可。

L213  match mode with | .apply => Consistent t c | .waive => True

apply要求整个理论在情境内一致；waive不施加该约束。

L215def conflictingHeld : Theory World := union (singleton capability) (singleton (fun w => ¬ capability w))

在同一理论中组合实际能力主张及其否定。

L217theorem conflictConsequences :

从同时持有的相反主张中抽取能力正反后果。

L218    Consequence conflictingHeld context .correctOutput true ∧

冲突的所持理论在固定情境下蕴涵输出正确的正判断。

L219    Consequence conflictingHeld context .correctOutput false := by

同一理论和情境也蕴涵其负判断。

L220  exact ⟨fun w hw => hw.1 capability (Or.inl rfl),

可容许世界对conflictingHeld的模型必须满足其中明确包含的能力主张。

L221    fun w hw => hw.1 (fun w => ¬ capability w) (Or.inr rfl)⟩

同一模型也必须满足明确包含的能力否定。

L223theorem conflictingHeldInconsistent : ¬ Consistent conflictingHeld context :=

以同条件正反后果否定一致性。

L224  conflictRequiresChange conflictingHeld context .correctOutput conflictConsequences.1 conflictConsequences.2

用同情境的两个相反后果反驳冲突所持理论的一致性。

L226/- The selection policy applies the actual output/budget and relevant-reason conditions to every implementation. -/

说明后续定义或结果：执行治理采用单独的可行相关选择规范，豁免治理接受任意理由清单。

L227def choicePermission (mode : Mode) (req : Requirements) (i : Implementation) (reasons : List Reason) : Prop :=

执行治理采用单独的可行相关选择规范，豁免治理接受任意理由清单。

L228  match mode with | .apply => JustifiedChoice req i reasons | .waive => True

apply通过JustifiedChoice执行实际可行性与理由相关性要求；waive许可任意选择包。

L230/- The following consequences are computed from distinct rule applications; they are not interchangeable support flags. -/

说明后续定义或结果：执行模式提出后继操作，豁免模式只提出原copy操作。

L231def proposedOperation : Mode → Operation

执行模式提出后继操作，豁免模式只提出原copy操作。

L232  | .apply => .successor

采用生成规则时提出successor，其输出可与copy不同。

L233  | .waive => .copy

豁免该规则时提出未变的copy操作。

L235def selfSamples : Mode → List Nat

执行模式测试零与一，豁免模式只测试会通过的一。

L236  | .apply => [0, 1]

采用反身评估时检查0和1，包括算术反例。

L237  | .waive => [1]

豁免时仅检查1，即算术原则通过的样本。

L239noncomputable def conflictDecision (mode : Mode) : Bool :=

用经典命题可判定性判断具体冲突理论是否获许可；这是非计算定义，不是已部署检查器。

L240  @decide (consistencyPermission mode conflictingHeld context) (Classical.propDecidable _)

用古典命题判定把整个冲突理论许可化为布尔值；未提供可执行判定算法。

L242noncomputable def groundsDecision (mode : Mode) (facet : Facet World) : Bool :=

用经典可判定性判断该模式是否许可指定单面向主张包。

L243  @decide (groundsPermission mode facet.claim canonicalArticulation (fun f => f = facet) [facet])

判定此方面自身主张及其确切单项评估包的许可。

L244    (Classical.propDecidable _)

为该可能不可计算的Grounds命题提供古典可判定性。

L246noncomputable def choiceDecision (mode : Mode) (i : Implementation) (reasons : List Reason) : Bool :=

用经典可判定性判断恒等要求下指定实现和理由是否获许可。

L247  @decide (choicePermission mode identityRequirements i reasons) (Classical.propDecidable _)

在固定恒等要求与提供理由下，古典判定该实现的选择许可。

L249theorem decisionsApply : conflictDecision .apply = false ∧

证明执行模式拒绝矛盾、无支持能力及不可行廉价后继，同时接受实际能力和恒等选择。

L250    groundsDecision .apply unsupportedCapabilityFacet = false ∧

采用Grounds时拒绝仅成本能力证据包。

L251    groundsDecision .apply capabilityFacet = true ∧

采用Grounds时接受得到适当支持的输出观察包。

L252    choiceDecision .apply cheapSuccessor [.method .simplicity] = false ∧

采用选择规范时，尽管简洁性理由相关，仍因输出不可行拒绝cheapSuccessor。

L253    choiceDecision .apply identityImpl objectiveReason = true := by

采用选择规范时，凭实际输出理由接受identity。

L254  classical

启用这些布尔许可定义所需的古典可判定实例。

L255  simp only [conflictDecision, groundsDecision, choiceDecision, consistencyPermission,

展开三个布尔决策及apply模式一致性谓词。

L256    groundsPermission, choicePermission]

也展开Grounds与选择许可，显露每个布尔值判定的实际命题。

L257  exact ⟨decide_eq_false conflictingHeldInconsistent,

已证不一致性迫使conflictDecision apply为false。

L258    decide_eq_false unsupportedGrounds, decide_eq_true capabilityGrounds,

失败的成本证据包判为false，已履责观察包判为true。

L259    decide_eq_false eligibleInternalReasonNotSufficient.2, decide_eq_true identityJustified⟩

不可行的廉价方法判为false；可行且有理由的identity判为true。

L261theorem decisionsWaive : conflictDecision .waive = true ∧

计算豁免模式接受具体矛盾、无支持面向和不可行选择。

L262    groundsDecision .waive unsupportedCapabilityFacet = true ∧

waive模式甚至接受无支持的仅成本能力证据包。

L263    choiceDecision .waive cheapSuccessor [.method .simplicity] = true := by

它也仅凭简洁性接受cheapSuccessor，尽管输出错误。

L264  exact ⟨@decide_eq_true (consistencyPermission .waive conflictingHeld context)

从consistencyPermission开始计算豁免结果；它在此模式按定义为True。

L265    (Classical.propDecidable _) trivial,

用该平凡许可证明得到true的冲突决策布尔值。

L266    @decide_eq_true (groundsPermission .waive unsupportedCapabilityFacet.claim canonicalArticulation

接着判定对确切不足能力方面主张的豁免许可。

L267      (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet]) (Classical.propDecidable _) trivial,

其单项适用谓词和包未变；豁免使许可为True、判定为true。

L268    @decide_eq_true (choicePermission .waive identityRequirements cheapSuccessor [.method .simplicity])

最后判定对同一廉价方法及仅简洁性理由的豁免许可。

L269      (Classical.propDecidable _) trivial⟩

该许可再次平凡为True，完成全部三个豁免决策。

L271/- Each application supplies its own outcome type, adopted objective, constraints and actual option-indexed reasons. -/

说明后续定义或结果：为各承诺把治理模式解释为选项，分别赋予操作结果、目标、约束、实际理由及范围内批评响应。

L272noncomputable def commitmentPositionFor (c : Commitment) (chosenMode : Mode) : ValuePosition World :=

为各承诺把治理模式解释为选项，分别赋予操作结果、目标、约束、实际理由及范围内批评响应。

L273  match c with

为五项承诺分别选择不同的操作性价值立场适配接口。

L274  | .generation => {

构造生成承诺的价值立场。

L275      Position := Mode, Outcome := Operation, adopted := chosenMode, selected := actualSystem.governance,

其立场为治理模式、后果为操作，采纳选项与同一系统所选治理对应。

L276      outcome := fun _ mode => proposedOperation mode,

把模式映射为实际提出的successor或copy操作。

L277      objective := fun op => op.run 0 ≠ Operation.copy.run 0,

采纳的生成目标要求0处输出不同于copy的0输出。

L278      constraints := fun _ mode => Generative (policyFor mode),

还要求该模式实际政策满足采纳的Generative约束。

L279      starting := singleton (fun w => actualSystem.governance w = chosenMode),

明确以同一系统选择chosenMode为起始承诺，不是推导出的普遍事实。

L280      reasons := [fun _ mode => (proposedOperation mode).run 0 = 1 ∧ Operation.copy.run 0 = 0],

其随选项变化的理由比较拟议操作0→1与copy的0→0表现。

L281      limits := fun w => w.1 = .identity,

将此生成立场限于实现候选为identity的世界。

L282      relevantCriticism := fun _ => ¬ Expanded baseState inflatedState,

把实际库存膨胀却未扩展作为生成承诺的相关批评。

L283      response := fun _ => some "Pursuing expansion does not guarantee it; assess the actual before and after capabilities separately" }

回应取向不保证进步且须另评前后能力；保存的回应是非空文本。

L284  | .consistency => {

构造一致性承诺的不同价值立场。

L285      Position := Mode, Outcome := Bool, adopted := chosenMode, selected := actualSystem.governance,

以模式为立场、布尔冲突许可决策为后果，关联同一所选治理。

L286      outcome := fun _ mode => conflictDecision mode,

实际后果是该模式对整个冲突理论的决策。

L287      objective := fun accepted => accepted = false,

要求该决策拒绝冲突理论。

L288      constraints := fun _ mode => consistencyPermission mode held context,

同时要求实际所持理论与情境通过同一模式的一致性许可。

L289      starting := singleton (fun w => actualSystem.governance w = chosenMode),

把同一系统采纳chosenMode陈述为此立场明确起始假设。

L290      reasons := [fun _ _ => Consequence conflictingHeld context .correctOutput true ∧

一致性理由首先包括冲突理论的输出正确正后果。

L291        Consequence conflictingHeld context .correctOutput false],

它还包括完全相同问题与情境下的相反后果。

L292      limits := fun w => w.1 = .identity,

将此一致性立场限于identity候选世界。

L293      relevantCriticism := fun _ => ¬ Entails (emptyTheory : Theory Bool) (fun w => w = true),

以空Bool理论不能蕴涵每个世界都为true作为实际不完整性批评。

L294      response := fun _ => some "Consistency alone does not establish sufficient support; assess the claim with its grounds as well" }

回应一致性本身不确立充分支持，仍须评估主张的根据。

L295  | .reflexivity => {

构造反身评估的价值立场。

L296      Position := Mode, Outcome := List Nat, adopted := chosenMode, selected := actualSystem.governance,

以模式为立场、实际样本输入列表为后果，关联同一所选治理。

L297      outcome := fun _ mode => selfSamples mode,

该模式选择样本集[0,1]或[1]。

L298      objective := fun samples => ∃ n ∈ samples, ownArithmeticPrinciple n = false,

要求某个实际选中样本揭示同一算术原则的假结果。

L299      constraints := fun _ mode => Reflexive 0 (ownRules 0) (workFor 0 mode),

还要求同一模式下所有者0的规则与工作满足完整反身要求。

L300      starting := singleton (fun w => actualSystem.governance w = chosenMode),

明确把同一系统采纳chosenMode作为起始承诺。

L301      reasons := [fun _ _ => ownArithmeticPrinciple 0 = false ∧ ownArithmeticPrinciple 1 = true],

理由指明算术原则在0实际失败、在1成功。

L302      limits := fun w => w.1 = .identity,

将此反身立场限制于identity候选世界。

L303      relevantCriticism := fun _ => selfTest [1] = true ∧ ownArithmeticPrinciple 0 = false,

保留1处通过测试与0处实际失败这对事实作为批评。

L304      response := fun _ => some "A passing self-test does not certify the principle; retain the relevant counterexample and its scope" }

回应通过自测不认证原则正确，须保留反例及其范围。

L305  | .grounds => {

构造针对Grounds条款自身的价值立场。

L306      Position := Mode, Outcome := Bool, adopted := chosenMode, selected := actualSystem.governance,

以模式为立场、布尔证据包决策为后果，属于同一系统治理。

L307      outcome := fun _ mode => groundsDecision mode unsupportedCapabilityFacet,

实际后果检验无支持的仅成本能力方面。

L308      objective := fun accepted => accepted = false,

要求拒绝该无支持证据包。

L309      constraints := fun _ mode => groundsPermission mode capability canonicalArticulation

还要求许可实际能力主张及按内容构造的表述。

L310        (fun f => f = capabilityFacet) [capabilityFacet],

该正约束恰使用已适当履责的单项capabilityFacet证据包。

L311      starting := singleton (fun w => actualSystem.governance w = chosenMode),

把同一系统采纳chosenMode陈述为明确起始承诺。

L312      reasons := [fun _ _ => Compatible [costAllowanceRecord] (.successor, .apply) ∧

Grounds理由记录successor/apply世界与成本观察相容。

L313        ¬ capability (.successor, .apply)],

把该相容性与同一世界中声称输出能力的实际失败配对。

L314      limits := fun w => w.1 = .identity,

将此Grounds立场限制于identity候选世界。

L315      relevantCriticism := fun _ => OutputContract outputOnlyProcess ∧ ¬ ExplanationContract outputOnlyProcess,

批评指向同一过程满足输出合同却没有附带解释合同。

L316      response := fun _ => some "Grounds allows an external output assessment without requiring this process to provide an internal explanation" }

回应外部输出评估可提供Grounds，而不要求此过程解释其内部生成。

L317  | .choice => {

构造实现选择的独立价值立场。

L318      Position := Mode, Outcome := Bool, adopted := chosenMode, selected := actualSystem.governance,

以模式为立场、布尔方法许可决策为后果，关联同一治理选择。

L319      outcome := fun _ mode => choiceDecision mode cheapSuccessor [.method .simplicity],

受检选择是仅以简洁性为理由的廉价successor。

L320      objective := fun accepted => accepted = false,

要求拒绝该错误输出选择。

L321      constraints := fun _ mode => choicePermission mode identityRequirements identityImpl objectiveReason,

还要求在相同要求下凭实际输出理由接受identity。

L322      starting := singleton (fun w => actualSystem.governance w = chosenMode),

明确为此系统采纳chosenMode；价值起点不是从中性事实证明的。

L323      reasons := [fun _ _ => cheapSuccessor.run 0 = 1 ∧ identityRequirements.expected 0 = 0 ∧

选择理由比较同一输入上cheapSuccessor输出1与所需输出0。

L324        cheapSuccessor.cost ≤ identityRequirements.budget],

还记录该方法满足预算，因此低成本不能掩盖输出失败。

L325      limits := fun w => w.1 = .identity,

将此选择立场限于identity候选世界。

L326      relevantCriticism := fun _ => identityImpl.conventional = true ∧ identityImpl.established = true,

把identity实际具有的惯用及既有地位，保留为对排除既有方法的相关批评。

L327      response := fun _ => some "An existing conventional method remains eligible when actual output and budget reasons justify it" }

回应惯用既有方法在实际输出与预算理由支持时仍可被选择。

L329noncomputable def commitmentPosition (c : Commitment) : ValuePosition World := commitmentPositionFor c .apply

把各自解释的立场具体化为采纳执行治理模式。

L331/- The fact used as a reason has content before evaluating the adopted rule's consequence. -/

说明后续定义或结果：在同一实际世界和采纳模式下，以计算或具体反例检查每项承诺理由。

L332theorem positionReasons (c : Commitment) :

在同一实际世界和采纳模式下，以计算或具体反例检查每项承诺理由。

L333    ∀ r ∈ (commitmentPosition c).reasons, r actual (commitmentPosition c).adopted := by

承诺c实际列出的每个理由，都须在actual世界对其采纳的apply选项成立。

L334  cases c <;> intro r hr <;> dsimp [commitmentPosition, commitmentPositionFor] at hr ⊢ <;>

分别处理五项承诺，展开各自实际理由列表，并固定其中理由r。

L335    rcases List.mem_singleton.mp hr with rfl

每个列表都是单项，成员前提把r确定为该承诺的具体理由。

L336  · exact ⟨rfl, rfl⟩

生成理由计算为successor 0=1且copy 0=0。

L337  · exact conflictConsequences

一致性理由使用已证同一冲突理论的正反后果。

L338  · exact ⟨rfl, rfl⟩

反身理由计算同一算术原则在0失败、在1成功。

L339  · refine ⟨costCompatibleWithFailure, ?_⟩

对Grounds，提供successor世界的成本相容性，留下能力失败待证。

L340    intro h

假设同一successor世界仍具有所需输出能力。

L341    have bad := h 0 trivial

在必需输入0处，该假设给出successor输出1等于所需0。

L342    cases bad

排除不可能的1=0，证明理由中的能力失败部分。

L343  · exact ⟨rfl, rfl, by decide⟩

选择理由计算得到输出1、所需0及廉价方法满足预算的成本。

L345/- Each adopted rule has its stated consequence in this explicitly defined application; this is not ultimate value justification. -/

说明后续定义或结果：用实际判断及遵守定理证明每个采纳模式满足自身目标与约束，不断言终极规范正确。

L346theorem positionConsequence (c : Commitment) (w : World) : (commitmentPosition c).consequence w := by

用实际判断及遵守定理证明每个采纳模式满足自身目标与约束，不断言终极规范正确。

L347  cases c <;> dsimp [commitmentPosition, commitmentPositionFor, ValuePosition.consequence]

将每项承诺后果展开为实际目标与随模式变化的约束。

L348  · exact ⟨by decide, ⟨Or.inl rfl, fun _ _ => trivial⟩⟩

生成的apply选项在0处不同于copy，且openPolicy满足价值取向与可修订性。

L349  · exact ⟨decisionsApply.1, jointConsistent⟩

一致性的apply选项拒绝冲突理论，同时实际所持理论保持一致。

L350  · exact ⟨⟨0, by simp [selfSamples], rfl⟩, completeOwnWork_reflexive 0⟩

反身性从[0,1]选择实际反例0，并提供完整内容性自有工作反身履责。

L351  · exact ⟨decisionsApply.2.1, capabilityGrounds⟩

Grounds拒绝无支持成本包，同时正确能力证据包具有Grounds。

L352  · exact ⟨decisionsApply.2.2.2.1, identityJustified⟩

选择规范拒绝cheapSuccessor，保留有理由且可行的identity实现。

L354theorem positionProcedure (c : Commitment) : ValueProcedure (commitmentPosition c) := by

为每项承诺构造非空理由、联合采纳、已检查后果及非空响应；已独立证明的后果无需再用理由假设。

L355  refine ⟨?_, ?_, ?_, ?_⟩

把ValueProcedure分为非空理由、联合采纳、带范围后果规则及批评回应。

L356  · cases c <;> simp [commitmentPosition, commitmentPositionFor]

检查每项承诺实际理由列表都包含其单项理由。

L357  · refine ⟨actual, ?_, ?_, ?_, positionReasons c⟩

用同一actual世界作为JointAdoption见证，并提供positionReasons c；余下检查起始理论、限度与采纳。

L358    · cases c <;> exact (modelsSingleton _ _).2 rfl

在actual中治理为apply，因此选择采纳模式的单项起始理论成立。

L359    · cases c <;> rfl

对每项承诺，actual的identity候选满足其声明限度。

L360    · cases c <;> rfl

对每项承诺，actual所选治理等于采纳的apply选项。

L361  · intro w _ _ _

为程序后果条款取任意世界及起始、限度、全部理由前提。

L362    exact positionConsequence c w

使用已对每个世界证明apply选项目标与约束的positionConsequence；此处不需要这些前提。

L363  · intro w _ _

为回应条款，取具有适用范围内相关批评的世界。

L364    cases c <;> exact ⟨_, rfl, by decide⟩

每项承诺都返回其实际保存的非空回应字符串，满足回应存在要求。

L366/- Criticism is instantiated within the adopted position's actual limit rather than made vacuous. -/

说明后续定义或结果：为每项承诺提供实际范围内批评情形，避免这些实例的响应义务空真。

L367theorem criticismWithinScope (c : Commitment) :

为每项承诺提供实际范围内批评情形，避免这些实例的响应义务空真。

L368    (commitmentPosition c).limits actual ∧ (commitmentPosition c).relevantCriticism actual := by

要求actual既属于此承诺限度，且该承诺具体批评确在该处适用。

L369  constructor

将实际限度检查与实际批评检查分开。

L370  · cases c <;> rfl

每个限度都要求identity，而actual候选按定义正是identity。

L371  · cases c

分别检查每项承诺的不同批评，不空泛假设存在批评。

L372    · simp [commitmentPosition, commitmentPositionFor, Expanded, baseState, inflatedState]

生成批评成立，因为膨胀基线列表没有新增理解或构造操作。

L373    · exact consistentIncomplete.2.1

一致性批评使用空理论不能蕴涵所选Bool主张的已证结果。

L374    · exact ⟨rfl, rfl⟩

反身批评计算得到1处样本通过而0处失败。

L375    · exact ⟨outputNotExplanation.1, outputNotExplanation.2.1⟩

Grounds批评组合outputOnlyProcess的实际输出正确性与缺失解释合同。

L376    · exact ⟨rfl, rfl⟩

选择批评成立，因为identity实际为惯用且既有实现。

L378/- Waiving the rule changes the actual computed outcome or an explicit adopted constraint; old reasons cannot certify it unchanged. -/

说明后续定义或结果：证明豁免选项不满足各项未改变的目标或约束。

L379theorem oppositeConsequenceFails (c : Commitment) (w : World) :

证明豁免选项不满足各项未改变的目标或约束。

L380    ¬ (commitmentPositionFor c .waive).consequence w := by

陈述任意世界中每项承诺的waive选项都会违反声明目标或约束。

L381  cases c <;> intro h

分别处理各承诺，并假设对应waive后果成立以求矛盾。

L382  · exact permissionNotValuation.2.2 h.2

生成后果会要求Generative neutralPolicy，与许可不等于赋值例中已证失败矛盾。

L383  · have bad : conflictDecision .waive = false := h.1

一致性假设目标声称waive必须拒绝冲突理论。

L384    rw [decisionsWaive.1] at bad

但decisionsWaive得到接受值true，使该目标化为true=false。

L385    cases bad

排除一致性选项的不可能布尔等式。

L386  · obtain ⟨n, hn, hf⟩ := h.1

反身性假设目标提供选中样本n，使算术原则在该处为假。

L387    change n ∈ [1] at hn

waive模式选中样本恰为[1]。

L388    have he : n = 1 := List.mem_singleton.mp hn

属于该单项列表迫使所谓失败输入n等于1。

L389    subst n

在声称失败的证明中把n替换为1。

L390    cases hf

该原则在1实际返回true，与声称的false结果矛盾。

L391  · have bad : groundsDecision .waive unsupportedCapabilityFacet = false := h.1

Grounds假设目标声称waive拒绝具体无支持能力包。

L392    rw [decisionsWaive.2.1] at bad

decisionsWaive却说明同一包被接受，得到true=false。

L393    cases bad

排除不可能等式，故豁免Grounds后果失败。

L394  · have bad : choiceDecision .waive cheapSuccessor [.method .simplicity] = false := h.1

选择的假设目标声称waive拒绝仅凭简洁性的cheapSuccessor。

L395    rw [decisionsWaive.2.2] at bad

decisionsWaive证明该确切选择被接受，再次得到true=false。

L396    cases bad

排除该等式，完成全部五个waive后果的失败证明。

L398theorem oppositeProcedureRejected (c : Commitment) : ¬ ValueProcedure (commitmentPositionFor c .waive) := by

将假定联合采纳见证与后果失败结合，拒绝相反模式的程序。

L399  intro h

假设相反的waive价值立场仍满足ValueProcedure。

L400  obtain ⟨w, hs, hl, _, hr⟩ := h.2.1

提取其JointAdoption见证w、起始理论证明hs、限度证明hl及全部理由证明hr。

L401  exact oppositeConsequenceFails c w (h.2.2.1 w hs hl hr)

将假设程序的后果条款应用于同一联合见证，得到waive后果；oppositeConsequenceFails c w正反驳该后果。

L403/- Each statement names adoption of a particular rule; its defined policy gives that option its meaning. -/

说明后续定义或结果：抽取各立场采纳主张；都使用同一治理选择器，但分别评估结果和理由。

L404noncomputable def commitmentClaim (c : Commitment) : Claim World := (commitmentPosition c).commitment

抽取各立场采纳主张；都使用同一治理选择器，但分别评估结果和理由。

L406noncomputable def commitmentFacet (c : Commitment) : Facet World := .value (commitmentPosition c)

把具体解释的承诺立场包装成价值面向。

L408theorem reasonsBelongToCommitments (c : Commitment) :

为每项承诺提供Grounds、真实联合采纳、实际相关批评及同目标下相反政策的拒绝。

L409    Grounds (commitmentClaim c) canonicalArticulation

要求为承诺c的实际采纳主张提供Grounds，表述由其方面内容构造。

L410      (fun f => f = commitmentFacet c) [commitmentFacet c] ∧

仅令commitmentFacet c适用，并只提供同一方面。

L411    JointAdoption (commitmentPosition c) ∧

还要求该立场具有非空的联合可容许采纳见证。

L412    (commitmentPosition c).relevantCriticism actual ∧

要求此特定承诺的批评在actual实际成立。

L413    ¬ ValueProcedure (commitmentPositionFor c .waive) := by

还证明相反waive立场不满足同一价值程序要求。

L414  exact ⟨canonicalGroundsForSingleton (commitmentFacet c) (positionProcedure c),

使用该承诺已检查的positionProcedure构造单项Grounds。

L415    (positionProcedure c).2.1, (criticismWithinScope c).2, oppositeProcedureRejected c⟩

补上其联合见证、实际批评及相反立场的已证拒绝。

L417/- This claim concerns the Grounds rule for arbitrary claim/facet packages, not a single capability duty. -/

说明后续定义或结果：证明Grounds立场采纳主张与所选治理模式的一般Grounds规范外延相同。

L418theorem groundsCommitmentIsProvision : commitmentClaim .grounds = (fun w => GroundsProvision w.2) := by

证明Grounds立场采纳主张与所选治理模式的一般Grounds规范外延相同。

L419  funext w

为证明两个主张相等，固定任意世界w并比较该处命题。

L420  apply propext

使用命题外延性：两个命题等价即可得到相等。

L421  exact (groundsProvisionMeaning w.2).symm

groundsProvisionMeaning说明一般条款恰在apply模式成立，与此采纳主张按反向对应。

L423theorem groundsSelfAssessment :

把价值Grounds应用到一般Grounds规范自身，保留实际范围、批评及被拒绝豁免变体。

L424    Grounds (fun w => GroundsProvision w.2) canonicalArticulation

用按内容构造的表述评估量化主张与方面包的一般GroundsProvision自身。

L425      (fun f => f = commitmentFacet .grounds) [commitmentFacet .grounds] ∧

适用价值方面恰为grounds承诺自身的方面。

L426    (commitmentPosition .grounds).limits actual ∧

要求actual满足该承诺声明限度。

L427    (commitmentPosition .grounds).relevantCriticism actual ∧

也要求其批评在actual实际适用。

L428    ¬ ValueProcedure (commitmentPositionFor .grounds .waive) := by

要求相反的豁免Grounds承诺不满足ValueProcedure。

L429  rw [← groundsCommitmentIsProvision]

把一般条款改写为外延相同的grounds采纳主张。

L430  exact ⟨(reasonsBelongToCommitments .grounds).1,

复用针对同一grounds承诺的实际Grounds证明。

L431    (criticismWithinScope .grounds).1, (criticismWithinScope .grounds).2,

提供分别检查过的实际限度与实际相关批评。

L432    oppositeProcedureRejected .grounds⟩

提供相反豁免Grounds立场的已证失败。

L434/- This existing principle form implements the same system's choice rule on two actual proposals.

说明后续定义或结果：保存当前哲学原则形式及其实际治理模式。

L435Input 0 names the identity proposal; input 1 names the cheap successor proposal. -/

说明后续定义或结果：保存当前哲学原则形式及其实际治理模式。

L436structure PhilosophyMethod where

保存当前哲学原则形式及其实际治理模式。

L437  form : Form

保存该哲学方法实现的实际原则形式。

L438  mode : Mode

保存同一哲学方法采用还是豁免治理检查。

L440def currentPhilosophy (s : System) (w : World) : PhilosophyMethod :=

从同一系统原则形式及治理选择派生被审哲学对象。

L441  ⟨s.principleForm, s.governance w⟩

以该系统自身原则形式及其在w中的治理构造哲学方法。

L443noncomputable def PhilosophyMethod.review (p : PhilosophyMethod) (input : Nat) : Nat :=

按该哲学实际治理模式，对零处恒等提案及其他处廉价不可行提案给出许可结果。

L444  if input = 0 then

输入0指认identity方法提案；其余输入走廉价successor提案分支。

L445    if choiceDecision p.mode identityImpl objectiveReason then 1 else 0

对identity，运行该哲学方法实际选择政策，接受返回1、拒绝返回0。

L446  else if choiceDecision p.mode cheapSuccessor [.method .simplicity] then 1 else 0

对其他输入，以同一政策评估仅凭简洁性的cheapSuccessor，同样以1/0编码接受与拒绝。

L448noncomputable def PhilosophyMethod.implementation (p : PhilosophyMethod) : Implementation where

把实际哲学审查程序呈为实现，域为零与一，并提供对应输出及轨迹代理。

L449  name := "Current philosophy's proposal review"

将实现命名为当前哲学的实际提案审查方法。

L450  conventional := true

将该提案审查实现标记为惯用。

L451  established := true

也标记同一实现为既有；后续证明检查仅此是否足以支持优先性。

L452  run := p.review

实现实际运行恰为该哲学方法的review函数。

L453  cost := 1

给该审查实现赋成本1。

L454  domain n := n = 0 ∨ n = 1

仅将提案编号0和1声明为其应用定义域。

L455  explanation := p.review

在实现解释字段中提供同一review函数。

L456  trace n := [n, p.review n]

记录由提案编号和实际审查结果组成的双条轨迹。

L458def proposalRequirements : Requirements where

要求接受提案零、拒绝提案一，并满足预算一。

L459  inputs n := n = 0 ∨ n = 1

该应用恰测试提案编号0和1。

L460  expected n := if n = 0 then 1 else 0

要求identity提案0被接受为1，另一受测提案被拒绝为0。

L461  budget := 1

给予该审查方法成本预算1。

L462  values _ := True

本例不通过要求中的values谓词增加限制。

L464theorem currentReviewCorrect : ∀ n, proposalRequirements.inputs n →

从执行治理结果计算两个被要求提案的实际判断。

L465    (currentPhilosophy actualSystem actual).review n = proposalRequirements.expected n := by

对每个必需提案，实际系统当前哲学审查须等于应用期望判定。

L466  intro n hn

取提案n及其属于必需输入的证明hn。

L467  rcases hn with rfl | rfl <;>

用hn把n限定为具体identity或廉价successor提案编号。

L468    simp [PhilosophyMethod.review, currentPhilosophy, actualSystem, actual,

展开同一当前哲学方法和实际系统，显露真实提案决策。

L469      proposalRequirements, decisionsApply.2.2.2.1, decisionsApply.2.2.2.2]

用decisionsApply将接受identity、拒绝廉价successor与所需判定匹配。

L471/- Status alone fails for this actual principle method; its demonstrated proposal decisions give a relevant reason. -/

说明后续定义或结果：将实现绑定当前原则及治理对象，拒绝纯地位优先，并由两个实际提案判断提供正当理由。

L472theorem existingPhilosophyNotPrivileged :

将实现绑定当前原则及治理对象，拒绝纯地位优先，并由两个实际提案判断提供正当理由。

L473    (currentPhilosophy actualSystem actual).form = actualSystem.principleForm ∧

检查该哲学方法形式恰为实际系统当前原则形式。

L474    (currentPhilosophy actualSystem actual).mode = actualSystem.governance actual ∧

检查其治理模式恰为同一系统在actual的模式。

L475    ¬ JustifiedChoice proposalRequirements

开始陈述仅地位不足以支持选择此实际审查实现。

L476      (currentPhilosophy actualSystem actual).implementation [.status .standing] ∧

对同一哲学实现，被拒绝理由列表恰为[.status .standing]。

L477    JustifiedChoice proposalRequirements

另陈述该实现在实际提案要求下具有有根据选择。

L478      (currentPhilosophy actualSystem actual).implementation [.method .output] ∧

该正向选择使用实际输出理由，而非仅其名称或既有标记。

L479    (currentPhilosophy actualSystem actual).review 0 = 1 ∧

同一哲学审查实际以结果1接受identity提案0。

L480    (currentPhilosophy actualSystem actual).review 1 = 0 := by

它实际以结果0拒绝廉价successor提案1。

L481  refine ⟨rfl, rfl, statusOnlyFails _ _ _, ?_, currentReviewCorrect 0 (Or.inl rfl),

提供同形式与模式、纯地位拒绝及提案0正确计算，留下正向输出理由选择待证。

L482    currentReviewCorrect 1 (Or.inr rfl)⟩

也为必需提案1提供currentReviewCorrect，证明实际拒绝。

L483  exact ⟨⟨currentReviewCorrect, by change 1 ≤ 1; decide⟩,

由两个提案输出正确及成本1≤预算1构造正向选择可行性。

L484    .method .output, by simp, trivial, currentReviewCorrect⟩

以列表中的.method .output理由及currentReviewCorrect作为实际相关性见证。

L486/- Applications choose their contract and requirements; the resulting claim is about this system's actual method. -/

说明后续定义或结果：将任意给定应用合同和要求用于该系统实际依世界方法。

L487def applicationClaim (s : System) (req : Requirements)

将任意给定应用合同和要求用于该系统实际依世界方法。

L488    (contract : Requirements → Implementation → Prop) : Claim World :=

接收关联Requirements与被评实现的任意应用合同。

L489  fun w => contract req (s.method.realize w)

在每个世界，把同一合同和要求应用于该系统实际方法实现。

L491def ApplicationDuties (s : System) (w : World) (req : Requirements)

把同系统完整反身性与精确参数化应用主张的Grounds结合。

L492    (contract : Requirements → Implementation → Prop)

ApplicationDuties把选定应用合同保留为明确参数。

L493    (articulations : Facet World → Articulation World)

也接收为每个潜在相关方面提供的表述。

L494    (applicable : Facet World → Prop) (facets : List (Facet World)) : Prop :=

把实际适用谓词与提供的方面列表分开。

L495  Reflexive s.owner (s.rules w) (s.work w) ∧

要求同一系统所有者在w的实际规则和工作满足完整反身要求。

L496  Grounds (applicationClaim s req contract) articulations applicable facets

要求为该系统、这些要求与此合同产生的主张提供匹配Grounds。

L498/- These are consequences of an explicitly adopted duty, not a proof that arbitrary applications fulfill it. -/

说明后续定义或结果：从明确假定的应用遵守接口抽取反身性、适用覆盖及匹配面向检查，不凭空确立遵守。

L499theorem applicationRetainsDuties (s : System) (w : World) (req : Requirements)

从明确假定的应用遵守接口抽取反身性、适用覆盖及匹配面向检查，不凭空确立遵守。

L500    (contract : Requirements → Implementation → Prop)

该定理保留任意应用合同，不固定单一能力定义。

L501    (articulations : Facet World → Articulation World)

保留该应用各方面的实际表述族。

L502    (applicable : Facet World → Prop) (facets : List (Facet World))

保留该应用自身适用谓词及所提供方面列表。

L503    (h : ApplicationDuties s w req contract articulations applicable facets) :

关键前提是假设ApplicationDuties已对这些确切对象成立；定理不创造履责事实。

L504    Reflexive s.owner (s.rules w) (s.work w) ∧

结论从假设义务保留同所有者规则与工作的完整反身要求。

L505    (∀ f, applicable f → f ∈ facets) ∧

它要求每个实际适用方面都在提供列表中，与标签无关。

L506    (∀ f ∈ facets, f.claim = applicationClaim s req contract ∧

对每个所列方面，其被评主张须等于该系统实际参数化应用主张。

L507      Articulated (articulations f) ∧ FacetArticulated (articulations f) f ∧ FacetDischarged f) :=

同一方面须具有可表达且内容匹配的表述，并实际满足履责条件。

L508  ⟨h.1, h.2.2.1, h.2.2.2⟩

投影h.1为反身要求，h.2.2.1为适用方面覆盖，h.2.2.2为每个所列方面的同主张、表述与履责检查。

L510def outputContract (req : Requirements) (i : Implementation) : Prop :=

要求实现满足应用在每个请求输入上的期望输出。

L511  ∀ n, req.inputs n → i.run n = req.expected n

输出合同在每个必需输入上核对该实现实际运行与所选期望输出。

L513def successorRequirements : Requirements :=

把同一应用的期望输出由恒等改为后继，保留其他字段。

L514  { identityRequirements with expected := fun n => n + 1 }

保留identityRequirements的输入及其他字段，但把期望输出改为n+1。

L516/- Holding the system and observation fixed while changing the actual objective changes the capability claim. -/

说明后续定义或结果：保留旧观察，把被评主张改成后继目标，以检验同对象证据是否仍足够。

L517def changedObjectiveFacet : Facet World :=

保留旧观察，把被评主张改成后继目标，以检验同对象证据是否仍足够。

L518  .empirical [observation] (fun _ => True)

为无限制范围的经验方面复用旧实际观察。

L519    (applicationClaim actualSystem successorRequirements outputContract) (fun _ => True)

把其被评主张改为同一系统满足successorRequirements；不确定性谓词仍平凡为真。

L521theorem applicationVariation :

在此实例中，原恒等合同仍保有已履行义务；改后的后继合同在同一实际方法上失败，且指定保留观察包不能为它提供根据。

L522    ApplicationDuties actualSystem actual identityRequirements outputContract

原恒等输出应用在实际系统和世界上履行ApplicationDuties。

L523      canonicalArticulation (fun f => f = capabilityFacet) [capabilityFacet] ∧

该正实例使用已支持的capabilityFacet及按其自身内容构造的表述。

L524    ¬ applicationClaim actualSystem successorRequirements outputContract actual ∧

但同一实际系统不满足改变后的后继输出合同。

L525    ¬ Grounds (applicationClaim actualSystem successorRequirements outputContract)

改变后的主张也不能从保留观察包取得Grounds。

L526      canonicalArticulation (fun f => f = changedObjectiveFacet) [changedObjectiveFacet] := by

此失败恰针对changedObjectiveFacet单项包，不针对所有可能证据包。

L527  refine ⟨⟨completeOwnWork_reflexive 0, capabilityGrounds⟩, ?_, ?_⟩

由完整自有反身要求及capabilityGrounds构造原义务，留下改变后行为与证据失败待证。

L528  · intro h

假设实际identity方法满足新的successor合同。

L529    have bad := h 0 trivial

在必需输入0处，这会迫使实际输出0等于期望1。

L530    cases bad

排除不可能的0=1，反驳改变后的实际能力主张。

L531  · intro h

假设保留观察单项包仍为改变后的主张提供Grounds。

L532    have discharged := (h.2.2 changedObjectiveFacet (by simp)).2.2.2

从假设Grounds包提取实际changedObjectiveFacet的履责。

L533    have bad := discharged.2.1 actual ((observationIdentifies actual).2 rfl) trivial 0 trivial

将其支持规则应用于相容actual世界和输入0，得到同一错误输出等式0=1。

L534    cases bad

排除该等式，证明指定保留观察包不能为新主张提供根据。

L536/- The very system satisfies the charter while its true cost evidence fails to establish its output capability. -/

说明后续定义或结果：给出实际遵守章程系统与兼容成本证据，但该指定能力面向无支持；不排除其他有效根据。

L537theorem charterNotGrounds :

给出实际遵守章程系统与兼容成本证据，但该指定能力面向无支持；不排除其他有效根据。

L538    Charter actualSystem actual ∧

同一实际系统满足全部已表示Charter条件。

L539    Compatible [costAllowanceRecord] actual ∧

其实际世界与真实的至多2成本观察相容。

L540    ¬ Grounds capability canonicalArticulation

然而该成本证据不能为其输出能力提供Grounds。

L541      (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet] := by

被否定的是特定unsupportedCapabilityFacet单项Grounds，不是所有可能评估包。

L542  exact ⟨charterChecked, (by intro r hr; cases List.mem_singleton.mp hr; rfl), unsupportedGrounds⟩

组合charterChecked、actual与成本记录的直接相容性，以及已证unsupportedGrounds反例。

L544/- A single inhabited system/context carries the charter, its own actual claim and support,

说明后续定义或结果：构造同一系统和世界，满足实际判断、完整反身性、能力根据、可行选择及各解释承诺Grounds；这是有界模型而非哲学普遍正确性。

L545contentful principle work, and separately reasoned governance commitments. -/

说明后续定义或结果：构造同一系统和世界，满足实际判断、完整反身性、能力根据、可行选择及各解释承诺Grounds；这是有界模型而非哲学普遍正确性。

L546theorem jointWitness :

构造同一系统和世界，满足实际判断、完整反身性、能力根据、可行选择及各解释承诺Grounds；这是有界模型而非哲学普遍正确性。

L547    ∃ s : System, ∃ w : World,

要求存在实际系统与世界对作为联合见证，使组合主张非空。

L548      Admissible (systemHeld s) (systemContext s) w ∧ Charter s w ∧

同一对象对必须对其共同持有主张和情境可容许，并满足Charter。

L549      OwnCapabilityDuty s w [capabilityFacet] ∧ systemCapability s w ∧

它还须由capabilityFacet履行自身能力义务，且拥有声称能力。

L550      JustifiedChoice s.requirements (s.method.realize w) objectiveReason ∧

同一实际方法须在自身要求下凭objectiveReason得到可行的有根据选择。

L551      (∀ c : Commitment, Grounds (commitmentClaim c) canonicalArticulation

对五项承诺中的每一项，对应实际采纳主张都须具有Grounds。

L552        (fun f => f = commitmentFacet c) [commitmentFacet c]) ∧

每项承诺使用自身确切单项价值方面及对应适用性。

L553      s = actualSystem ∧ w = actual := by

最后确认见证就是actualSystem和actual，防止换成无关存在对象。

L554  exact ⟨actualSystem, actual, actualAdmissible, charterChecked,

选择该确切对象对，提供实际可容许性与已检查Charter。

L555    ownCapabilityGrounded.1, capabilityActual, identityJustified,

补上同一系统自身能力义务、实际能力及有根据的identity选择。

L556    fun c => (reasonsBelongToCommitments c).1, rfl, rfl⟩

使用每项承诺已有Grounds证明，再按构造完成两个见证一致性等式。

L558end CoreReader.Integration

关闭当前命名空间。