leanified/CoreReader/Engineering/SelfApplication.lean

Back to claims · Declarations and proofs

Philosophy 0.2.1 · considered Core 0.1.2. This view uses the repository’s public target catalog, readers and Lean files. Presentation does not change their judgments.

Expand Lean and line explanations · 203 lines

LeanLine explanation

L1import CoreReader.Engineering.Values

Import CoreReader.Engineering.Values, making its declarations and transitive dependencies available; this line adds no new proposition.

L2import CoreReader.Engineering.Reflection

Import CoreReader.Engineering.Reflection, making its declarations and transitive dependencies available; this line adds no new proposition.

L4namespace CoreReader.Engineering

Open namespace CoreReader.Engineering for the following declarations.

L6open CoreReader.Adopted

Allow unqualified references to declarations in CoreReader.Adopted; their meaning is unchanged.

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

ReviewObject distinguishes the activity, each parameterized Core commitment, priority and evolution method.

L9  | generationRule | assessmentRule

Add actual generation-rule and assessment-rule objects to the same object type.

L10  deriving DecidableEq, Repr

Derive DecidableEq, Repr: decidable equality and printable representations of these constructors.

L12abbrev ReviewCase := Candidate × Nat

A review case is a pair of selected Candidate and natural-number size.

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

Generation applicability ignores object identity and depends only on lifecycle phase.

L15  phase ≠ .application

Generation applies exactly outside application: formation and revision.

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

Assessment applicability ignores both arguments and is true in all phases for every object.

L19def ruleObject : CoreReader.Agency.Activity → ReviewObject

Map each actual activity to its corresponding method review object.

L20  | .generation => .generationRule

Generation is represented by generationRule.

L21  | .assessment => .assessmentRule

Assessment is represented by assessmentRule.

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

Comment says these probes target current reflection functions themselves and introduces the size-10 case.

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

Comment contrasts a real initial sample at size 10 with its removal at size 5.

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

Comment retains the requested claim and distinguishes this actual-rule test from the domain batch predictor.

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

Build a probe for an actual method, parameterized by activity and Candidate/size pair.

L27    Reflection.Input ReviewCase ReviewObject where

The probe's samples are ReviewCase and its targets are ReviewObject.

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

Fix owner 0 and revision phase, with object chosen from the activity.

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

The inner test always passes; only size 10 supplies an initial sample, while claimed always contains the point.

L30  requested := [point]

Retain the point as the requested case even when the initial sample list is empty.

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

Supply a nonempty reason describing scope retention and distinguishing an empty initial list.

L32  basis := True

The probe basis is True; this field supplies no additional empirical justification.

L34def generationRuleTest

generationRuleTest tests the function supplied as method, allowing real function replacement.

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

The method must map this exact reflection input type to the corresponding outcome type.

L36    (point : ReviewCase) : Bool :=

For a case, return a Boolean contract result.

L37  let input := ruleProbe .generation point

Construct the generation probe for this same case.

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

Require exact outcome equality to generated requested tests and requested scope.

L40def assessmentRuleTest

assessmentRuleTest checks an explicitly supplied evaluator against a local sample-aware contract.

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

The evaluated method has this exact input type and returns a Verdict.

L42    (point : ReviewCase) : Bool :=

Each Candidate/size case receives a Boolean pass/fail result.

L43  method (ruleProbe .assessment point) ==

Compare the actual method's verdict on the assessment probe with the expected verdict below.

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

Expect support at size 10 and noSupportingSample otherwise; this is a local contract, not a universal empirical duty.

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

Comment introduces a candidate revision adding the missing empty-initial-list check.

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

Comment explicitly keeps the candidate separate from the currently installed evaluator.

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

Define a distinct candidate evaluator revision over the same input type.

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

Reject an empty initial tested list before delegating nonempty cases to current evaluate.

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

Comment introduces the evolutionMethod branch as criticism of this activity's own static batch forecast.

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

Comment contrasts the original size with the credible changed runtime size.

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

objectTest selects an operational Boolean test by actual review object.

L54  match object with

Pattern-match the object's constructor to choose its specific test.

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

For activity, decide whether the chosen design profile meets current necessary requirements.

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

For a commitment, run its enabled safeguard experiment on the chosen design.

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

For priority, decide the actual EvolutionPriority proposition in currentContinuing.

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

For evolutionMethod, compare the static and live batch forecasts for 21 items at this size.

L59  | .generationRule => generationRuleTest Reflection.generate point

For generationRule, pass the actual Reflection.generate function to its test.

L60  | .assessmentRule => assessmentRuleTest Reflection.evaluate point

For assessmentRule, pass the actual Reflection.evaluate function to its test.

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

Construct a finite review-object list depending on the chosen design.

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

Include the activity and all five Core commitments using their original identifiers.

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

Include the priority object only for the evolvable selection.

L65    [.evolutionMethod, .generationRule, .assessmentRule]

Always include the batch method and both actual rule objects.

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

Requested cases depend on chosen design and lifecycle phase.

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

Formation and application request only size 10.

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

Revision expands the requested list to sizes 10 and 5 of the same design.

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

Construct reason strings specifically for each object and phase.

L72  let content := match object with

Choose the first reason by the actual object constructor.

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

The activity reason names its order, safety, latency and retention requirements.

L74    | .commitment principle => criticismFor principle

A commitment reuses the criticism string indexed by the same principle.

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

The priority reason identifies evidence, maintainer paths, requirements and costs.

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

The method reason compares the same forecast at recorded and proposed runtime sizes.

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

The generator reason demands retention of requested tests and scope.

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

The evaluator reason states this local dependence on the presence of supporting samples.

L79  [content, match phase with

Return the object-specific reason plus a phase-specific reason.

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

Formation asks for the object's purpose and initial contract conditions.

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

Application names the current chosen design and continuing activity.

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

Revision asks to examine wider inputs and retain counterexamples.

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

Comment emphasizes that statedReview records are defined independently of evaluate.

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

Comment identifies the batch-method revision as an explicitly recorded counterexample.

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

Comment limits other supported records to the finite scopes checked by the subsequent proof.

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

statedReview independently records an outcome for a chosen design and activity.

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

The record also depends on object and phase and has the exact reflection outcome type.

L89  match activity with

Separate generation records from assessment records.

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

Generation records the phase's requested list in both output fields.

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

Assessment chooses its recorded verdict by object/phase, rather than calling evaluate.

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

Revision of the batch method or assessment rule is explicitly recorded as a counterexample.

L93    | _, _ => .supportedWithinScope)

Every other object/phase assessment is recorded as supportedWithinScope.

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

Comment introduces basis as object-specific factual content instead of an unrestricted approval flag.

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

Comment explains that a counterexample can support criticism of the same object.

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

Comment denies that such critical support establishes the method's broader original claim.

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

reviewBasis gives object-specific propositions; proofs will be checked for the ordinary designs.

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

Activity inquiry requires the actual activity's scope condition.

L100      Meets currentContinuing.required (currentContinuing.profiles chosen)

It additionally requires the chosen profile to meet current necessary requirements.

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

Commitment inquiry requires factual relevance of the reason for that same principle and selection.

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

Priority inquiry requires current applicability and absence of a threat to evolvable.

L103  | .evolutionMethod, .revision =>

The revision branch gives a stronger basis for the batch-method inquiry.

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

Require success at size 10 and an actual inequality at size 5.

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

Other batch-method phases require only the size-10 equality.

L106  | .generationRule, _ =>

The generator's basis is a positive and negative test of actual function content.

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

The real generator must pass at this chosen design and size 10.

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

An empty-output generator must fail on the same case.

L109  | .assessmentRule, .revision =>

Assessment-rule revision requires a two-case contrast.

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

The current evaluator must pass its sample-aware test at size 10.

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

It must fail that contract at size 5, where the initial list is empty.

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

Other assessment-rule phases require the size-10 positive case only.

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

selfModel instantiates reflection with these cases and objects for the chosen design.

L115  owner := 0

Set the model owner to 0. The separate self relation requires self-owned targets to match it; raw Model.input still accepts and retains a target with any owner.

L116  objects := reviewObjects chosen

Use the choice-dependent actual object list.

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

Each outer contract uses its objectTest, with initial tested and claimed lists containing size 10.

L118  requested _ := requestedCases chosen

All objects share the phase-specific requestedCases for the chosen design.

L119  reasons := reviewReasons

Use actual object/phase reason construction.

L120  basis := reviewBasis chosen

Use the substantive object/phase basis predicates.

L121  generationApplies := generationApplies

Install the actual generation applicability function.

L122  assessmentApplies := assessmentApplies

Install the actual assessment applicability function.

L123  recorded := statedReview chosen

Use independently stated records, which currentSelfRecords later verifies.

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

Comment begins the distinction between the actual normative object and its finite rationale experiment.

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

Comment denies that success of the rationale experiment proves universal normative correctness.

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

Comment states the intended same-identifier link across adoption, reasons and reflection.

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

For every chosen design and object, reviewIdentity identifies all input components.

L129    (phase : CoreReader.Agency.Phase) :

The identity holds for every lifecycle phase.

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

The input's target object is exactly the supplied object.

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

Its test is exactly objectTest for that same object.

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

Its requested list is exactly the chosen design's list at this phase.

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

Its reasons are exactly those of the same object and phase.

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

Its basis is exactly the same chosen/object/phase predicate.

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

All five identities hold by definitional reflexivity, not empirical validation.

L137theorem currentSelfRecords (chosen : Candidate)

currentSelfRecords checks the records of a selected design.

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

The premise restricts chosen to presentSimple or evolvable; maximal is excluded.

L139    (selfModel chosen).follows := by

The conclusion is follows, including each applicable record's actual interpretation.

L140  rcases ordinary with rfl | rfl

Split the ordinary premise and substitute each of the two designs.

L141  all_goals

Apply subsequent proof steps to both design goals.

L142    intro activity object phase member applies

Introduce arbitrary activity, object, phase, membership and applicability premises.

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

Exhaust all constructors of activity, object and phase.

L144    all_goals first

On every remaining goal, try the following local tactics in order.

L145      | rename_i principle; cases principle

When a commitment parameter exists, name it principle and split its five constructors.

L146      | skip

Otherwise leave the goal unchanged rather than requiring a principle parameter.

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

Simplify all goals and hypotheses using the actual interpretation and input construction.

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

Expand evaluator, model, stated records and finite object lists.

L149      requestedCases, reviewReasons, criticismFor, objectTest, safeguardExperiment,

Expand requested cases, reasons, object tests and safeguard experiments.

L150      generationApplies, assessmentApplies, generationRuleTest, assessmentRuleTest,

Expand both applicability predicates and actual rule-test definitions.

L151      ruleProbe, Reflection.generate,

Expand the inner method probe and actual generator.

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

Expand basis, relevance and concrete threat/cost predicates.

L153      EvolutionPriority, PriorityConditions, JustifiedDeparture, currentContinuing,

Expand priority, applicability, departure and the fixed current context.

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

Expand activity scope, necessary requirements, profiles and initial evidence.

L155      ContinuingCapability, continuingActivity, maintainers, changePath,

Expand continuing capability, maintainer list and actual change paths.

L156      changeWork, abstractionComplexity, credible, CredibleDirection, articulateGround,

Expand work, complexity and credibility of the stated directions.

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

Expand evidence support, limits, batch arithmetic and ordered output.

L158      sortedUnique, sortValues, insertOrdered, List.eraseDups]

Expand the sorting and duplicate-removal helpers needed for finite checks.

L159    all_goals decide

Decide any remaining closed finite propositions after the case splits and simplification.

L161theorem currentSelfApplication (chosen : Candidate)

currentSelfApplication derives reflexivity for a selected design.

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

Retain the explicit two-design ordinary premise.

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

The specification uses the same selfModel's rules and self-target predicate.

L164      (selfModel chosen).performed :=

Its performance relation is also taken from that same model.

L165  Reflection.recordedReflexivity _ (currentSelfRecords chosen ordinary)

Apply the generic recordedReflexivity theorem with the actually proved currentSelfRecords premise.

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

Comment identifies success of the old observation for the activity's batch assessment method.

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

Comment says expanded input reveals the failed forecast and begins the limit of self-application.

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

Comment denies that self-application or a broader generated candidate makes the failed forecast true.

L170theorem actualSelfCriticism (chosen : Candidate) :

actualSelfCriticism holds for every chosen design and exhibits the batch method's finite failure.

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

The old size-10 batch test passes.

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

The size-5 batch test fails.

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

The actual revision evaluator reports counterexample for that same method object.

L174    statedReview chosen .generation .evolutionMethod .revision =

The separately recorded generation result for that method's revision is specified.

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

Both generated lists contain size 10 and size 5 for the same chosen design.

L176    staticBatch 21 5 ≠ liveBatch 21 5 := by

The conclusion also retains the underlying arithmetic forecast inequality.

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

Construct five conjuncts; generation is reflexive and arithmetic inequality decidable, leaving three checks.

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

Expose the size-10 Boolean equality test as the first proof goal.

L179    decide

Compute that closed size-10 equality.

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

Expose the size-5 Boolean inequality result as the next goal.

L181    decide

Compute that closed size-5 failure.

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

Expand the evaluator and actual model input for the counterexample goal.

L183      objectTest, staticBatch, liveBatch, batchCount]

Reduce object test and batch arithmetic to close that counterexample calculation.

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

Comment stresses identity between review objects and the functions actually used in adopted rules.

L186applicability functions. Assessment applies in all three phases; generation

Comment retains identical applicability functions and all-phase assessment.

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

Comment includes formation/revision of the generation rules themselves in generation's applicable phases.

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

ownRuleIdentity links every chosen design and activity to the actual rule object and implementation.

L189    (phase : CoreReader.Agency.Phase) :

The link is stated for every phase, regardless of whether generation applies there.

L190    ruleObject activity ∈ (selfModel chosen).objects ∧

The activity's method object actually belongs to the model's objects.

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

The model rule's meaning is exactly the actual interpret activity function.

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

The input for this same rule object obtains its actual contract test.

L193      objectTest (ruleObject activity) ∧

That test is objectTest indexed by this identical method object.

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

Compare the model's generation applicability at this object/phase.

L195      generationApplies (ruleObject activity) phase ∧

It equals the declared generationApplies function on the same arguments.

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

Compare the model's assessment applicability at this object/phase.

L197      assessmentApplies (ruleObject activity) phase := by

It equals assessmentApplies on those identical arguments.

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

Four function/field equalities are reflexive; leave actual object membership as the only goal.

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

Split activity and compute membership in the actual review-object list.

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

Comment describes a content-sensitive generator replacement despite unchanged object naming.

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

Comment records the actual evaluator's acceptance with an empty initial sample list; requested cases are still checked.

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

Comment characterizes the outer self-review as reporting this bounded local-contract defect, not proving itself universally valid.

L204theorem ownRuleContentVariation (chosen : Candidate) :

ownRuleContentVariation supplies function-sensitive positive and negative cases for every design.

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

The current generator passes the size-10 retention test.

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

An empty-output generator fails the identical test.

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

The current evaluator passes the local sample-aware contract with a size-10 sample.

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

It fails that contract at size 5 with an empty initial sample list.

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

The outer revision assessment of the actual assessment-rule object reports counterexample.

L210    generationApplies .generationRule .formation ∧

Generation applies to formation of its own rule object.

L211    generationApplies .generationRule .revision ∧

It also applies to revision of its own rule object.

L212    ¬ generationApplies .generationRule .application ∧

Generation does not apply to application phase of that object.

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

Assessment applies to its own rule object for every phase.

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

Unfold actual method tests, probe and generator in all conjuncts.

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

Expand evaluator, actual input/model and requested cases.

L216    objectTest, generationApplies, assessmentApplies]

Reduce the object test and both applicability predicates to finish the finite checks.

L218theorem proposedRuleRevision (chosen : Candidate) :

proposedRuleRevision compares current and candidate evaluators and an applicability mutation.

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

The current evaluator fails the local empty-initial-sample contract.

L220    assessmentRuleTest sampleAwareAssessment (chosen, 5) = true ∧

The separate sampleAwareAssessment candidate passes that size-5 contract.

L221    assessmentRuleTest sampleAwareAssessment (chosen, 10) = true ∧

The candidate also retains the size-10 positive result.

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

The current generation rule applies to revision of its own generation-rule object.

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

A separate model update making generationApplies always False removes that applicability.

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

The removed applicability concerns exactly owner 0, generationRule and revision.

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

Expand the local test, candidate evaluator, probe and current evaluator.

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

Expand actual rule/self-target semantics and model object membership.

L227    generationApplies]

Reduce generation applicability to complete the conjunction; neither candidate is installed here.

L229end CoreReader.Engineering

Close namespace CoreReader.Engineering; no further mathematical claim is asserted.