leanified/CoreReader/Reflexivity.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 · 356 lines

LeanLine explanation

L1import Std

Imports Std and its dependencies into this module.

L3namespace CoreReader.Agency

Opens namespace CoreReader.Agency; file boundaries do not change declaration identity.

L5inductive Phase | formation | application | revision

Defines formation, application and revision phase tags.

L6  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L8structure PrincipleKey where

Identifies a registered principle by owner and local identifier.

L9  owner : Nat

Stores the owning subject identifier.

L10  localId : Nat

Stores the principle identifier within its owner.

L11  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L13inductive Subject

Distinguishes system, principle and phase-indexed principle-process objects.

L14  | system (owner : Nat)

Represents the system itself, identified by its owner number.

L15  | principle (owner id : Nat)

Represents a particular principle by owner and local principle identifier.

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

Represents that principle's formation, application or revision process as a separate subject.

L17  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L19def Subject.owner : Subject → Nat

Extracts the owner's identifier from every subject constructor.

L20  | .system n => n

Extracts the owner directly from a system subject.

L21  | .principle n _ => n

Extracts a principle's owner while ignoring its local identifier.

L22  | .process n _ _ => n

Extracts a process subject's owner independently of its principle identifier and phase.

L24inductive Activity | generation | assessment

Distinguishes generation work from assessment work.

L25  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L27inductive QuestionKind | conformity | formationBasis | applicability | revisionGrounds

Separates conformity, formation basis, applicability and revision-ground questions.

L28  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L30inductive SampleProgram | alwaysTrue | onlyAtZero

Provides a constant-true program and a program true only at zero.

L31  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L33def SampleProgram.run : SampleProgram → Nat → Bool

Evaluates those two programs on natural inputs.

L34  | .alwaysTrue, _ => true

The alwaysTrue sample program accepts every natural-number input.

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

The onlyAtZero program returns true precisely at input zero.

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

Documents the following definition or result: Stores tested inputs separately from the claimed scope, allowing overextended claims.

L38structure MethodDraft where

Stores tested inputs separately from the claimed scope, allowing overextended claims.

L39  testedInputs : List Nat

Records the inputs on which this method draft actually tests a program.

L40  claimedScope : List Nat

Separately records the input scope the draft proposes to authorize.

L41  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

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

Accepts a program when it succeeds on all listed test inputs; untested inputs are unchecked.

L44  draft.testedInputs.all program.run

Accepts a program when every tested input returns true; claimedScope is not checked here.

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

Documents the following definition or result: Binds a target and question kind to requested scope and the target's current method content.

L47structure Inquiry where

Binds a target and question kind to requested scope and the target's current method content.

L48  target : Subject

Identifies the exact subject whose method is being examined.

L49  kind : QuestionKind

Distinguishes conformity, formation reasons, applicability and revision reasons as inquiry purposes.

L50  requestedScope : List Nat

Records the input scope this particular inquiry asks the method to cover.

L51  currentMethod : MethodDraft

Attaches the actual method draft under examination, including its tested and claimed inputs.

L52  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L54inductive ReasonContent

Represents purposes, declared scopes, observations and concrete program/input counterexamples.

L55  | purpose (inputs : List Nat)

A purpose reason names the inputs the method is intended to address.

L56  | declaredScope (inputs : List Nat)

A scope reason states the method's declared input limits.

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

An observation reason records a specific input and Boolean output.

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

A counterexample reason names an actual sample program and input to check.

L59  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L61def ReasonContent.identifier : ReasonContent → Nat

Assigns a small code to each reason constructor; the code alone is not evidential content.

L62  | .purpose _ => 0

Uses local reference 0 for purpose reasons; this is a category identifier, not a unique global identity.

L63  | .declaredScope _ => 1

Uses local reference 1 for declared-scope reasons.

L64  | .observation _ _ => 2

Uses local reference 2 for observation reasons.

L65  | .counterexample _ _ => 3

Uses local reference 3 for counterexample reasons.

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

Documents the following definition or result: Attaches a reason's content and reference to the subject it concerns.

L68structure ReasonObject where

Attaches a reason's content and reference to the subject it concerns.

L69  reference : Nat

Stores a local reference identifying this reason in the modeled inquiry.

L70  target : Subject

Identifies the subject this reason actually concerns.

L71  content : ReasonContent

Stores the purpose, scope, observation or counterexample contents of the reason.

L72  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L74inductive AssessmentResult | supportedWithinScope | insufficient | notApplicable | undetermined

Allows scoped support, insufficiency, nonapplicability and undetermined results.

L75  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L77inductive WorkOutcome

Separates an assessment result from a generated method draft.

L78  | assessment (result : AssessmentResult)

Packages a verdict as an assessment outcome; a negative verdict is still an assessment.

L79  | generated (draft : MethodDraft)

Packages a newly generated method draft, without asserting that the draft is correct.

L80  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

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

Documents the following definition or result: Registers a rule's identity, activity, declared method, applicability, inquiries, reasons, limits and explicit outcome semantics.

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

Documents the following definition or result: Registers a rule's identity, activity, declared method, applicability, inquiries, reasons, limits and explicit outcome semantics.

L84structure Principle where

Registers a rule's identity, activity, declared method, applicability, inquiries, reasons, limits and explicit outcome semantics.

L85  key : PrincipleKey

Gives the principle an owner/local identifier used to resolve its records.

L86  activity : Activity

Specifies whether this principle governs generation or assessment activity.

L87  declaredMethod : MethodDraft

States the method draft belonging to this registered principle.

L88  applicable : Subject → Prop

States the subjects on which this principle is applicable.

L89  inquiry : Subject → Inquiry

Assigns the actual question to examine for each subject.

L90  reasons : Subject → List ReasonObject

Assigns the reasons supplied for each subject's question.

L91  limits : Subject → List Nat

Assigns the retained input limits for each subject's application.

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

Defines when an outcome follows this principle's question, reasons and limits; no adequacy law is imposed by this field alone.

L94structure WorkRecord where

Stores the actual rule identity, target, activity, inquiry, reasons, limits and outcome used by an application.

L95  usedPrinciple : PrincipleKey

Records the exact registered principle key claimed to have been used.

L96  target : Subject

Records the subject on which this work was performed.

L97  activity : Activity

Records whether this work was generation or assessment.

L98  inquiry : Inquiry

Stores the concrete inquiry actually recorded for this work.

L99  reasons : List ReasonObject

Stores the concrete reasons used in this work record.

L100  limits : List Nat

Stores the input limits retained in this work record.

L101  outcome : WorkOutcome

Stores the recorded assessment verdict or generated method draft.

L102  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

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

Requires equal registered keys to identify the same principle, preventing ambiguous duplicate identities.

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

Two registered principles sharing one key must be the same principle, preventing ambiguous lookup.

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

Requires each assessed target to resolve to a registered owner or exact principle key.

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

A system subject is resolved when the registry contains some principle with that owner.

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

Principle and process subjects require a registry entry with their exact owner and local identifier.

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

Documents the following definition or result: Connects the inquiry's current method to the registered target principle's declared method.

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

Documents the following definition or result: Connects the inquiry's current method to the registered target principle's declared method.

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

Connects the inquiry's current method to the registered target principle's declared method.

L114  match question.target with

Chooses the lookup rule from the inquiry's actual target kind.

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

A system inquiry examines the declared method of its owner's registered principle zero.

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

For a principle or its process, retain that target's actual owner and identifier for lookup.

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

Requires both exact key lookup and equality between the inquiry's method and that registered principle's method.

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

Requires an actual stored record with the requested target and activity; validity is checked separately.

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

Performed means a listed record has this exact subject and activity; by itself it checks no reason contents.

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

Documents the following definition or result: Retains the owner-and-applicability-conditioned record-coverage interface.

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

Retains the owner-and-applicability-conditioned record-coverage interface.

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

Every applicable registered rule must have a performed activity on subjects belonging to the specified owner.

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

Documents the following definition or result: Checks rule registration, applicability, object identities, resolved method content, nonempty targeted reasons, exact limits and agreement with the rule's semantics.

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

Documents the following definition or result: Checks rule registration, applicability, object identities, resolved method content, nonempty targeted reasons, exact limits and agreement with the rule's semantics.

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

Checks rule registration, applicability, object identities, resolved method content, nonempty targeted reasons, exact limits and agreement with the rule's semantics.

L129    (record : WorkRecord) : Prop where

The following proof fields certify one particular work record as a valid use of rule on s.

L130  registered : rule ∈ rules

Requires the rule used by the record to belong to this registry.

L131  applicable : rule.applicable s

Requires that same rule to be applicable to the assessed subject.

L132  usedIdentity : record.usedPrinciple = rule.key

Checks the record's used-principle key against this rule's exact key.

L133  targetIdentity : record.target = s

Checks that the work record targets this exact subject s.

L134  targetResolved : TargetResolved rules s

Requires the record's subject to resolve within the same rule registry.

L135  activityIdentity : record.activity = rule.activity

Checks that the recorded activity is the activity governed by this rule.

L136  inquiryIdentity : record.inquiry = rule.inquiry s

Checks that the recorded inquiry equals the inquiry this rule assigns to s.

L137  inquiryTarget : record.inquiry.target = s

Separately checks that the inquiry itself targets s, rather than an unrelated subject.

L138  targetContent : TargetContentResolved rules record.inquiry

Checks that the inquiry's method belongs to its resolved registered target.

L139  reasonsIdentity : record.reasons = rule.reasons s

Checks the recorded reasons equal those specified by this rule for s.

L140  reasonsNonempty : record.reasons ≠ []

Requires at least one actual reason in this record.

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

Requires every recorded reason to concern the same subject s.

L142  limitsIdentity : record.limits = rule.limits s

Checks that recorded limits equal the rule's limits for s.

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

Requires the record's outcome to satisfy the rule's actual meaning relation on its inquiry, reasons and limits.

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

Documents the following definition or result: Requires a coherent registry and a valid recorded application for every applicable same-owner subject and registered rule; this remains a model compliance condition.

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

Requires a coherent registry and a valid recorded application for every applicable same-owner subject and registered rule; this remains a model compliance condition.

L147  RegistryCoherent rules ∧

Reflexive first requires unambiguous principle registration.

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

It then ranges over each registered rule and owned subject where that rule is applicable.

L149    ∃ record ∈ records, ValidApplication rules rule s record

For each such application, some listed record must satisfy all ValidApplication content checks.

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

Forgets content-validity details while extracting target/activity record coverage from full reflexivity.

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

Assumes full contentful Reflexive compliance and derives its weaker scope-only coverage.

L153  intro rule hr s hs ha

Takes a registered rule, an owned subject and its applicability premise for the scope obligation.

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

Uses full Reflexive compliance to obtain the actual listed record and its ValidApplication proof.

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

Keeps that record's membership, target identity and activity identity to prove Performed.

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

Instantiates full reflexivity at a registered applicable same-owner subject, then extracts its performance record.

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

Requires full Reflexive compliance and actual membership of the rule in the registry.

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

Also requires the target's owner to match and the rule to be applicable to it.

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

Specializes the derived scope obligation to those premises, yielding this target's performed activity.

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

Tests input zero and declares scope zero.

L164def inquiryFor (s : Subject) : Inquiry :=

Maps formation to basis, application to applicability, revision to grounds over zero and one, and other objects to conformity.

L165  match s with

Chooses the inquiry from the subject's process phase, retaining the same subject as target.

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

For formation, asks about the basis for a method covering input zero.

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

For application, asks whether the local method applies on input zero.

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

For revision, asks about extending the same local method's scope to inputs zero and one.

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

For a system or principle itself, asks conformity on the local scope {0}.

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

Documents the following definition or result: Supplies question-specific purpose/scope/observation data, adding a failing untested-input program for revision review.

L172def sourceReasonContents : QuestionKind → List ReasonContent

Supplies question-specific purpose/scope/observation data, adding a failing untested-input program for revision review.

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

Formation reasons state the purpose {0}, declared scope {0}, and the observed true result at zero.

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

Applicability and conformity use the declared local scope plus the same observation at zero.

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

Revision reasons request {0,1} while acknowledging a declared scope of {0} and only a zero observation.

L176      .counterexample .onlyAtZero 1]

Adds the concrete onlyAtZero program at input one as a revision counterexample.

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

Attaches every chosen reason's content to this exact inquiry target.

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

Wraps each source reason with its category reference and the same subject s, preserving its actual content.

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

Documents the following definition or result: Computes scoped results from actual reason contents and method scope; a program passing current tests but failing a requested input yields insufficiency for revision.

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

Documents the following definition or result: Computes scoped results from actual reason contents and method scope; a program passing current tests but failing a requested input yields insufficiency for revision.

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

Computes scoped results from actual reason contents and method scope; a program passing current tests but failing a requested input yields insufficiency for revision.

L184  let contents := reasons.map ReasonObject.content

Extracts reason contents for checking their substantive purpose, scope, observations and counterexamples.

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

Returns undetermined if supplied limits differ from the examined method's declared scope.

L186  match question.kind with

After checking limits, evaluates the specific kind of question asked.

L187  | .formationBasis =>

Selects the formation-basis assessment branch.

L188      if ReasonContent.purpose question.requestedScope ∈ contents ∧

Requires a purpose reason covering the inquiry's requested inputs.

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

Also requires an explicit limit declaration and equality of requested and declared scopes.

L190      then .supportedWithinScope else .undetermined

Formation is supportedWithinScope only when those content checks pass; otherwise it is undetermined.

L191  | .applicability | .conformity =>

Uses the same local checks for applicability and conformity questions.

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

First tests that every requested input belongs to the supplied limits.

L193        if ReasonContent.declaredScope limits ∈ contents ∧

Within those limits, requires a reason explicitly declaring that same scope.

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

Also requires the true observation at zero and a requested scope exactly equal to [0].

L195        then .supportedWithinScope else .undetermined

Passing these local checks yields supportedWithinScope; incomplete evidence yields undetermined.

L196      else .notApplicable

A requested input outside the supplied limits yields notApplicable.

L197  | .revisionGrounds =>

Selects the revision-grounds branch, which searches for an actual scope counterexample.

L198      if ReasonContent.purpose question.requestedScope ∈ contents ∧

Requires a reason stating the revised requested scope as the intended purpose.

L199          ReasonContent.declaredScope limits ∈ contents ∧

Requires the old limits to be explicitly present as a declared-scope reason.

L200          ReasonContent.observation 0 true ∈ contents ∧

Requires the original successful observation at input zero.

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

Searches the supplied reason contents for a counterexample satisfying the following concrete checks.

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

A counterexample's input must be inside the newly requested scope.

L203                question.currentMethod.accepts program &&

Its program must nevertheless pass the current method's tested inputs.

L204                !(program.run input)

That same program must fail at the counterexample input.

L205            | _ => false)

Other reason kinds cannot themselves satisfy this counterexample search.

L206      then .insufficient else .undetermined

A witnessed testing/scope gap yields insufficient; without those contents, the result is undetermined.

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

Generation keeps tested inputs and adopts requested scope; assessment executes the reason-sensitive inquiry evaluator.

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

Supplies the same reasons and limits to the activity-specific result function.

L210  match activity with

Chooses between generating a draft and evaluating an inquiry.

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

Generation keeps the method's tested inputs but proposes the inquiry's requested scope; correctness is not certified.

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

Assessment computes assessInquiry from this question's actual reasons and limits.

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

Defines acceptable outcome by equality with the disclosed finite evaluation algorithm, not an assumed successful result.

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

Receives the specific recorded outcome whose compliance with this activity's method is checked.

L216  outcome = finiteMethodResult activity question reasons limits

An outcome follows the method exactly when it equals the computed finiteMethodResult.

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

Enumerates the owner system, both registered principles and all three phases of each principle.

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

Includes the system itself and its two principle identities as owned subjects.

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

Includes formation, application and revision of principle zero as separate subjects.

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

Also includes all three phases of principle one, giving nine owned subjects total.

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

Documents the following definition or result: Excludes application-phase processes from this particular generation rule while retaining the other objects.

L224def generationEligible : Subject → Bool

Excludes application-phase processes from this particular generation rule while retaining the other objects.

L225  | .process _ _ .application => false

Treats applying an already existing principle as ineligible for generation in this application model.

L226  | _ => true

All other represented subject kinds remain eligible for generation.

L228def generatingRule (owner : Nat) : Principle where

Registers principle zero for generation with the local method, explicit inquiries/reasons and restricted applicability.

L229  key := ⟨owner,0⟩

Registers the generation principle under local key zero for this owner.

L230  activity := .generation

Makes this rule govern generation work.

L231  declaredMethod := localMethod

Assigns the local test-and-scope draft [0]/[0] to the generation rule.

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

Generation requires both membership in this owner's nine subjects and generation eligibility.

L233  inquiry := inquiryFor

Uses inquiryFor to supply the subject's actual phase-sensitive question.

L234  reasons := reasonsFor

Uses reasonsFor to supply the original target-linked reason contents.

L235  limits _ := [0]

Retains [0] as the generation rule's limit for every subject.

L236  meaning := finiteMethodMeaning .generation

Requires the generated outcome to match finiteMethodResult's generation branch.

L238def assessingRule (owner : Nat) : Principle where

Registers principle one for assessment of every enumerated own subject with explicit finite evaluation semantics.

L239  key := ⟨owner,1⟩

Registers the assessment principle under distinct local key one.

L240  activity := .assessment

Makes this rule govern assessment work.

L241  declaredMethod := localMethod

The assessment principle declares the same local [0]/[0] method contract.

L242  applicable s := s ∈ ownSubjects owner

Assessment applies to all nine subjects belonging to this owner.

L243  inquiry := inquiryFor

Assigns the same phase-sensitive inquiry function to the assessment rule.

L244  reasons := reasonsFor

Assigns the same original target-linked reasons to its assessments.

L245  limits _ := [0]

Retains [0] as the assessment rule's declared limit.

L246  meaning := finiteMethodMeaning .assessment

Requires assessment outcomes to equal the evaluator's actual result.

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

Returns the two distinct registered generation and assessment principles.

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

Documents the following definition or result: Constructs expected generated drafts and scoped/insufficient assessment results, which are subsequently checked against evaluation.

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

Constructs expected generated drafts and scoped/insufficient assessment results, which are subsequently checked against evaluation.

L252  match activity with

Chooses the independently stated record outcome by activity.

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

The recorded generated draft retains tested inputs and adopts the inquiry's requested scope.

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

For assessment records, chooses a stated verdict from the inquiry kind rather than calling assessInquiry here.

L255      | .revisionGrounds => .insufficient

Revision inquiries are recorded as insufficient.

L256      | _ => .supportedWithinScope)

The remaining represented inquiries are recorded as supportedWithinScope.

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

Builds a record from the supplied rule and subject; registry membership and content validity require the later ValidApplication proof.

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

Builds a record from this rule's identity, inquiry, reasons and limits, but uses the separately stated outcome.

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

Exhausts subject/phase constructors to prove each concrete inquiry has reasons.

L262  cases s with

Checks reason-list nonemptiness for each kind of subject.

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

System inquiries use the conformity reasons, which contain scope and observation entries.

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

Principle inquiries likewise have the nonempty scope-and-observation list.

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

Each process phase reduces to its actual nonempty formation, application or revision reason list.

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

Uses the reason-list map construction to prove every reason targets the same subject.

L268  intro reason h

Takes any reason known to occur in this subject's constructed reason list.

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

Inverts the map construction to recover the source content and replace the reason with its target-tagged wrapper.

L270  rfl

That wrapper's target is s by construction, so target equality is reflexive.

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

Checks each constructor to prove the generated inquiry retains its subject identity.

L273  cases s with

Checks the inquiry target for system, principle and process subjects separately.

L274  | system owner => rfl

The system inquiry was constructed with that same system as target.

L275  | principle owner id => rfl

The principle inquiry likewise retains that same principle target.

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

Every process phase uses the original process subject as its inquiry target.

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

Documents the following definition or result: Computes every subject/phase assessment and generation case, showing stored expected outcomes agree with the actual algorithm, including insufficiency.

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

Computes every subject/phase assessment and generation case, showing stored expected outcomes agree with the actual algorithm, including insufficiency.

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

Requires the independently stated outcome to equal actual evaluation of this subject's question, reasons and [0] limits.

L281  cases activity with

Splits this equality check between generated drafts and assessment verdicts.

L282  | generation => rfl

Both generation definitions construct the identical tested-input/requested-scope draft.

L283  | assessment =>

For assessment, the stated verdict must now be checked against the actual evaluator.

L284      cases s with

Separates the finite assessment check by subject kind.

L285      | system owner => rfl

The system's conformity contents compute to the stated supportedWithinScope verdict.

L286      | principle owner id => rfl

The principle's conformity contents compute to that same supportedWithinScope verdict.

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

Formation/application compute support; revision computes insufficient from the program passing zero but failing one.

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

Separates local identifiers zero and one to prove the two-rule registry has no ambiguous key.

L290  intro p hp q hq hkey

Takes two registered principles whose keys are assumed equal.

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

Restricts both registry memberships to the actual generation or assessment rule.

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

Examines the four resulting pairs of concrete rules.

L293  · rfl

When both are the generation rule, principle equality holds directly.

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

Generation key 0 cannot equal assessment key 1; projecting localId produces a contradiction.

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

The reverse mixed pair would require localId 1=0, also impossible.

L296  · rfl

When both are the assessment rule, principle equality holds directly.

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

Checks all nine enumerated subjects resolve to an actual registered owner/principle.

L299    TargetResolved (ownRules owner) s := by

The subject selected from ownSubjects must resolve to this owner's actual registry.

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

Expands membership hs into the nine concrete owned subjects.

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

Handles each of those nine subjects with its original owner and principle identifier fixed.

L302    simp [TargetResolved, ownRules, generatingRule, assessingRule]

Finds the generation or assessment registry entry matching each target key.

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

Checks each inquiry's method matches its registered target's declared local method.

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

Requires the selected subject's inquiry to examine its own registered declared method.

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

Again enumerates the nine concrete subjects from the actual membership premise.

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

Checks target-method correspondence separately for each system, principle and phase subject.

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

Both registered rules declare localMethod, exactly the method inquiryFor assigns to every enumerated target.

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

Combines identity, reason-target, scope, registry and actual evaluation facts to validate each applicable generated record.

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

Assumes the chosen registered rule is applicable to this subject s.

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

Proves the concrete recordFor rule s satisfies every ValidApplication field.

L313  have hs : s ∈ ownSubjects owner := by

First derives that applicability places s in this owner's subject list.

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

Uses registry membership to restrict rule to one of the two owned rules.

L315    rcases hr with rfl | rfl

Separates the generation and assessment applicability conditions.

L316    · exact ha.1

Generation applicability includes owned-subject membership as its first conjunct.

L317    · exact ha

Assessment applicability is exactly that owned-subject membership.

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

Establishes that this actual rule uses inquiryFor as its inquiry function.

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

Reduces registered-rule membership to generation or assessment to inspect its inquiry field.

L320    rcases hr with rfl | rfl <;> rfl

Both possible rules define their inquiry field as inquiryFor.

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

Establishes that the chosen rule uses reasonsFor as its reason provider.

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

Again restricts the rule to the two actual registry entries before inspecting reasons.

L323    rcases hr with rfl | rfl <;> rfl

Both entries supply exactly reasonsFor.

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

Establishes that this rule's limits for s are exactly [0].

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

Resolves registry membership before inspecting the selected rule's limits.

L326    rcases hr with rfl | rfl <;> rfl

Both owned rules retain [0] as their limit.

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

Establishes that the chosen rule's meaning is the result function for its own activity.

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

Resolves registry membership to inspect generation versus assessment meaning.

L329    rcases hr with rfl | rfl <;> rfl

In either case, the rule's meaning is finiteMethodMeaning specialized to that rule's activity.

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

Builds ValidApplication using registry/applicability premises, record identities and resolved target; leaves inquiry, reasons and computed meaning checks to follow.

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

The remaining inquiry-target goal is about this rule's actual inquiry on s.

L332    rw [hq]; exact inquiryFor_target s

Replaces the rule's inquiry with inquiryFor, whose target-preservation theorem proves it targets s.

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

The remaining method-identity goal checks the registered target of this rule's inquiry.

L334    rw [hq]; exact ownTargetContent owner s hs

Rewrites to inquiryFor and uses the concrete owned-target method-resolution theorem.

L335  · change rule.reasons s ≠ []

Reduces record reason nonemptiness to nonemptiness of this rule's supplied reasons.

L336    rw [hg]; exact reasonsFor_nonempty s

Rewrites those reasons to reasonsFor and applies its nonempty-list theorem.

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

Reduces reason-target consistency to every supplied reason targeting s.

L338    rw [hg]; exact reasonsFor_target s

Rewrites to reasonsFor and uses its target-preserving construction theorem.

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

The final obligation compares the separately stated outcome against this rule's actual inquiry, reasons, limits and meaning.

L340    rw [hm, hq, hg, hl]

Substitutes the four established identities for meaning, inquiry, reasons and [0] limits.

L341    exact ownContentEvaluates rule.activity s

Uses ownContentEvaluates to prove the recorded outcome equals the actual method result.

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

Constructs records for all nine subjects, including generation only where its eligibility condition holds.

L344  (ownSubjects owner).flatMap fun s =>

Builds the full log by concatenating the records assigned to each owned subject.

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

Eligible subjects receive both a generation record and an assessment record.

L346    else [recordFor (assessingRule owner) s]

Application-phase subjects receive assessment only, matching generation's explicit applicability restriction.

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

Places each subject's assessment record in the flat-mapped complete work list.

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

Claims this owned subject's assessment record occurs in the constructed full log.

L350  apply List.mem_flatMap.mpr

Uses flatMap membership: choose a subject whose assigned record list contains the desired record.

L351  refine ⟨s,hs,?_⟩

Chooses the same s and its supplied owned-subject membership hs.

L352  cases generationEligible s <;> simp

Whether generation is eligible or not, the assigned list contains s's assessment record.

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

Places a subject's generation record in the work list under explicit generation eligibility.

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

Adds generation eligibility to owned membership before claiming a generation record in the full log.

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

Selects s's flatMap branch; hg makes that branch include the requested generation record.

L358theorem completeOwnWork_reflexive (owner : Nat) :

Combines coherent registry, membership and content-valid applications to establish the concrete nonempty reflexivity model.

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

States full contentful reflexivity for the actual two-rule registry and constructed work log.

L360  refine ⟨ownRegistryCoherent owner, ?_⟩

Provides the proved registry coherence and leaves contentful coverage for each applicable subject.

L361  intro rule hr s _ ha

Takes an actual registered rule and applicable subject; applicability itself will supply needed owned membership.

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

Chooses recordFor rule s and its already proved content validity, leaving only its presence in the full log.

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

Resolves rule membership to the generation or assessment entry.

L364  rcases hr with rfl | rfl

Splits record membership by those two actual rule cases.

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

For generation, ha supplies owned membership and eligibility, which place its record in the full log.

L366  · exact assessingRecord_member owner s ha

For assessment, ha directly supplies the owned membership needed for its record.

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

Extracts the constructed assessment record for a listed own subject.

L369    Performed (completeOwnWork owner) s .assessment :=

Claims a performed assessment on s in the same complete work log.

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

Uses s's assessment record, its proved log membership and exact target/activity identities as the Performed witness.

L372def applicationRule : Principle :=

Restricts an assessment rule to one application-phase subject and assigns it a resolvable key.

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

Restricts the assessment rule to exactly principle-zero's application process, with key (0,0).

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

Stores the one fully specified application assessment record.

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

Checks the singleton registry and record satisfy full content-valid reflexivity on their restricted applicability.

L378  constructor

Separates singleton-registry coherence from coverage of its sole applicable subject.

L379  · intro p hp q hq _

Takes any two rules in that singleton registry; key equality is unnecessary because membership already identifies both.

L380    simp only [List.mem_singleton] at hp hq

Singleton membership makes both rules equal to applicationRule.

L381    rw [hp,hq]

Substituting these identities proves the two rules are equal.

L382  · intro rule hr s _ ha

Takes an applicable subject for a rule in the singleton application registry.

L383    simp only [List.mem_singleton] at hr

Uses singleton membership to identify the rule as applicationRule.

L384    subst rule

Replaces rule with that exact applicationRule throughout the coverage obligation.

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

Unfolds applicability to show s is exactly owner-zero principle-zero's application process.

L386    subst s

Substitutes that exact process for s, fixing the work target.

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

Selects the sole record in applicationWork and proves its membership; content validity remains to check.

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

Fills immediate registry, applicability and record-identity fields; leaves target resolution, reasons and computed outcome checks.

L389    · exact ⟨applicationRule, by simp, rfl⟩

The target key resolves to applicationRule itself in the singleton registry.

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

That same registered rule supplies the localMethod actually examined by the inquiry.

L391    · exact reasonsFor_nonempty _

The application inquiry's reasons are nonempty by reasonsFor_nonempty.

L392    · exact reasonsFor_target _

Every application reason targets this exact application-process subject.

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

The remaining meaning obligation is equality of the stated application assessment and its actual finite evaluation.

L394      exact ownContentEvaluates .assessment _

Uses ownContentEvaluates to certify that equality for the application-phase assessment.

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

Derives record scope from full reflexivity, proves its classical conditional/disjunctive equivalence, and gives a valid restricted example with no system assessment.

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

The first clause retains the implication from full contentful reflexivity to scope coverage.

L398    (ReflexiveScope owner rules records ↔

The second clause restates conditional scope coverage as an either/or obligation.

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

For each owned subject and registered rule, either the rule is inapplicable or its activity was performed.

L400    (Reflexive 0 [applicationRule] applicationWork ∧

The concrete singleton application log satisfies full reflexivity under its restricted rule.

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

Yet that same log contains no assessment of the system itself, where this rule is not applicable.

L402  classical

Uses classical case splitting on possibly undecidable applicability predicates.

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

Supplies the general scope projection and concrete restricted witness; leaves the equivalence and missing-system-record proof.

L404  · constructor

Proves both directions of the applicability-or-performance reformulation.

L405    · intro h rule hr s hs

Assumes conditional scope coverage and fixes a registered rule with an owned subject.

L406      by_cases ha : rule.applicable s

Splits on whether that exact rule is applicable to this subject.

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

When applicable, coverage supplies the performed activity, satisfying the right disjunct.

L408      · exact Or.inl ha

When inapplicable, that negative applicability fact satisfies the left disjunct.

L409    · intro h rule hr s hs ha

For the reverse direction, assumes the disjunction and actual applicability on the owned subject.

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

Rules out the inapplicable disjunct using ha, leaving the required performed activity.

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

Assumes a system assessment exists and extracts its listed record plus target identity.

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

The singleton applicationWork list forces that record to be its application-process record.

L413    subst record

Replaces the alleged system-assessment record with that sole process record.

L414    cases ht

Its process target cannot equal the system target, contradicting the assumed record identity.

L416end CoreReader.Agency

Closes the current namespace.