leanified/CoreReader/Agency.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 · 215 lines

LeanLine explanation

L1import CoreReader.Reflexivity

Imports CoreReader.Reflexivity and its dependencies into this module.

L3namespace CoreReader.Agency

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

L5inductive FormKind | organization | method | principle | appearance | artifact

Defines exactly five form tags; their names carry no additional semantics.

L6  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L8structure Form where

A form is a kind tag and a natural-number version.

L9  kind : FormKind

Stores whether this form is an organization, method, principle, appearance or artifact.

L10  version : Nat

Stores a natural-number form version; it does not prove any change occurred.

L11  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L13inductive Aim | expandUnderstandingAndConstruction | preserveSafeOperation

Defines two aim tags: expanding understanding/construction and preserving safe operation; the datatype alone does not value either aim.

L14  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L16/- A policy records an adopted valuation, current forms, and permission. It does not assert that valuation is correct or enacted. -/

Documents the following definition or result: A policy supplies four unrelated predicate fields; no law ties version permission to valuation or revisability.

L17structure Policy where

A policy supplies four unrelated predicate fields; no law ties version permission to valuation or revisability.

L18  worthPursuing : Aim → Prop

Specifies which of the two represented aims this policy regards as worth pursuing.

L19  current : Form → Prop

Specifies the form kind/version pairs currently held by this policy.

L20  revisable : Form → Prop

Specifies which form kind/version pairs this policy leaves revisable.

L21  permitsVersion : Nat → Nat → Prop

Specifies permission between version numbers independently of actual execution.

L23/- The normative specification keeps valuation and revisability separate from realized transitions. -/

Documents the following definition or result: A policy satisfies this predicate when it values the designated expansion aim and declares every current form revisable. This states no actual progress condition.

L24def Generative (p : Policy) : Prop :=

A policy satisfies this predicate when it values the designated expansion aim and declares every current form revisable. This states no actual progress condition.

L25  p.worthPursuing .expandUnderstandingAndConstruction ∧

Requires this policy to value expanding understanding and construction.

L26    ∀ f, p.current f → p.revisable f

Requires every form currently held by this policy to remain revisable.

L28def openPolicy : Policy where

Constructs a policy valuing both aims, selecting version zero, and permitting every revision and version pair.

L29  worthPursuing a := a = .expandUnderstandingAndConstruction ∨ a = .preserveSafeOperation

Values both expansion and preserving safe operation in openPolicy.

L30  current f := f.version = 0

Treats precisely version-zero forms as current, regardless of kind.

L31  revisable _ := True

Allows revision of every form, including forms not currently held.

L32  permitsVersion _ _ := True

Permits every pair of version numbers; this does not execute a change.

L34def neutralPolicy : Policy := { openPolicy with worthPursuing := fun _ => False }

Copies the open policy but makes every aim unworthy of pursuit; the permission fields are unchanged.

L36/- Permitting a real version change does not supply an adopted value position. -/

Documents the following definition or result: Shows permission for version 0 to 1 and distinct versions coexist with failure of the generation predicate.

L37theorem permissionNotValuation :

Shows permission for version 0 to 1 and distinct versions coexist with failure of the generation predicate.

L38    neutralPolicy.permitsVersion 0 1 ∧ (0 : Nat) ≠ 1 ∧ ¬ Generative neutralPolicy := by

States that neutralPolicy permits 0→1, the versions differ, and its missing valuation defeats Generative.

L39  simp [neutralPolicy, openPolicy, Generative]

Unfolds the two policies: permission is true, 0≠1 computes true, and the required valuation is false.

L41/- This is an explicit consequence of the adopted specification, not evidence of actual revision. -/

Documents the following definition or result: Extracts revisability of a specified current kind/version from an assumed generation predicate; it does not revise that form.

L42theorem revisabilityCovers (p : Policy) (h : Generative p) (k : FormKind) (v : Nat)

Extracts revisability of a specified current kind/version from an assumed generation predicate; it does not revise that form.

L43    (hc : p.current ⟨k, v⟩) : p.revisable ⟨k, v⟩ := h.2 _ hc

Uses h's revisability clause on the same kind/version form that hc identifies as current.

L45inductive Operation | copy | successor

Defines the only two encoded operations: identity and successor on natural numbers.

L46  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L48def Operation.run : Operation → Nat → Nat

Interprets an operation as a function on natural numbers.

L49  | .copy, n => n

Executing copy returns its input unchanged.

L50  | .successor, n => n + 1

Executing successor returns the input plus one.

L52inductive InventoryKind | document | term | tool | artifact

Defines four inventory tags whose operational content is stored separately.

L53  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L55structure Item where

An inventory item consists of a tag and one of the two operations.

L56  kind : InventoryKind

Classifies this inventory item as a document, term, tool or artifact.

L57  content : Operation

Records the operation represented by this item, independently of its category.

L58  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L60/- Available represented operations are the contents present, not their number of occurrences. -/

Documents the following definition or result: Availability means that some item in the supplied list has exactly the requested operation as its content.

L61def Available (xs : List Item) (op : Operation) : Prop :=

Availability means that some item in the supplied list has exactly the requested operation as its content.

L62  ∃ item ∈ xs, item.content = op

An operation is available exactly when some listed item contains that operation.

L64/- Duplicating any inventory category preserves exactly the represented operation content. -/

Documents the following definition or result: Proves that duplicating a uniformly tagged list of operations does not change which operations are available.

L65theorem inventoryNotCapability (kind : InventoryKind) (ops : List Operation) (op : Operation) :

Proves that duplicating a uniformly tagged list of operations does not change which operations are available.

L66    Available ((ops.map fun x => Item.mk kind x) ++ (ops.map fun x => Item.mk kind x)) op ↔

Tests availability after duplicating the list of items built from ops and the fixed category.

L67      Available (ops.map fun x => Item.mk kind x) op := by

Compares it with availability in the original single copy of that same list.

L68  simp only [Available, List.mem_append]

Expands availability and turns membership in the duplicated list into membership in either copy.

L69  constructor

Proves both directions: duplication neither adds nor removes represented operations.

L70  · rintro ⟨x, hx | hx, hop⟩ <;> exact ⟨x, hx, hop⟩

An item found in either copy is already an original-list witness for the same operation.

L71  · rintro ⟨x, hx, hop⟩

For the reverse direction, take an original item x with membership hx and matching content hop.

L72    exact ⟨x, Or.inl hx, hop⟩

Places that same item in the first copy, preserving its matching operation.

L74structure State where

A state is five lists; understanding and construction are represented only by membership in the two-operation datatype.

L75  understood : List Operation

Lists operations represented as understood in this state.

L76  constructed : List Operation

Lists operations represented as constructed in this state.

L77  inventory : List Item

Stores inventory items; their multiplicity is distinct from capability membership.

L78  abstractionLayers : List Operation

Stores abstraction-layer entries without identifying their count with understanding.

L79  vocabulary : List Operation

Stores vocabulary entries without identifying their count with constructed capability.

L80  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L82/- A gain must identify an operation newly understood or constructed; this is a disclosed finite capability representation. -/

Documents the following definition or result: Expansion is the appearance of at least one previously absent operation in either understanding or construction. It allows losing other operations.

L83def Expanded (before after : State) : Prop :=

Expansion is the appearance of at least one previously absent operation in either understanding or construction. It allows losing other operations.

L84  (∃ op, op ∈ after.understood ∧ op ∉ before.understood) ∨

Expansion may be witnessed by an operation understood after the change but not before.

L85  (∃ op, op ∈ after.constructed ∧ op ∉ before.constructed)

Alternatively, a newly constructed operation witnesses expansion.

L87def baseState : State :=

Constructs a state with only copy in every operation list and one copy artifact.

L88  ⟨[.copy], [.copy], [⟨.artifact, .copy⟩], [.copy], [.copy]⟩

The baseline understands and constructs copy, with one copy artifact, layer and vocabulary entry.

L90def inflatedState : State :=

Constructs a larger inventory/layer/vocabulary state with unchanged understanding and construction.

L91  { baseState with

Starts from baseState, retaining fields unless explicitly overwritten below.

L92    inventory := baseState.inventory ++ baseState.inventory

Duplicates the one-item inventory while leaving understood and constructed operations unchanged.

L93    abstractionLayers := [.copy, .copy]

Replaces one abstraction-layer entry with two copies of copy.

L94    vocabulary := [.copy, .copy] }

Similarly doubles the vocabulary list; no new operation is introduced.

L96def stableTrace (_time : Nat) : State := baseState

Returns the same base state at every natural-number time.

L98/- A revisable policy can govern an unchanged trace; no improvement is hidden in revisability. -/

Documents the following definition or result: Exhibits a policy meeting the generation interface and universal revisability while its independently chosen constant trace never expands.

L99theorem revisionWithoutProgress :

Exhibits a policy meeting the generation interface and universal revisability while its independently chosen constant trace never expands.

L100    Generative openPolicy ∧

Asserts openPolicy meets the adopted valuation-and-revisability specification.

L101    (∀ k : FormKind, openPolicy.revisable ⟨k, 0⟩) ∧

Additionally exposes revision permission for version zero of every form category.

L102    (∀ t, ¬ Expanded (stableTrace t) (stableTrace (t + 1))) := by

Every adjacent pair in the constant trace lacks a newly understood or constructed operation.

L103  simp [Generative, openPolicy, stableTrace, Expanded]

Reduces the policy clauses to true and every expansion claim to impossible new membership in an unchanged list.

L105structure ExternalResources where

Stores three optional natural numbers representing external-resource slots.

L106  experience : Option Nat

An optional external experience value; none makes assistedExecution fail at its first read.

L107  knowledge : Option Nat

An optional knowledge value required after the experience input.

L108  collaborator : Option Nat

An optional collaborator value required before producing the result.

L109  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L111/- This interpreter actually needs all three external inputs to produce the modeled result. -/

Documents the following definition or result: An Option computation succeeds only when all three slots are present, then returns their sum through identity. This dependency is programmed into the example.

L112def assistedExecution (r : ExternalResources) : Option Nat := do

An Option computation succeeds only when all three slots are present, then returns their sum through identity. This dependency is programmed into the example.

L113  let e ← r.experience

Reads experience into e, immediately returning none when that resource is absent.

L114  let k ← r.knowledge

Reads knowledge into k; absence aborts the same Option computation.

L115  let c ← r.collaborator

Reads the collaborator's value into c, also propagating absence.

L116  pure (Operation.copy.run (e + k + c))

Returns the sum e+k+c through the copy operation inside some.

L118def availableResources : ExternalResources := ⟨some 1, some 2, some 3⟩

Provides resource values 1, 2 and 3 for the concrete success case.

L120/- Stability has a concrete stated reason in this workload: preserve its operation while staying within the one-item budget. -/

Documents the following definition or result: Defines a particular non-growth reason: construction lists match, the old inventory has length at most one, and the proposed one exceeds one.

L121def StableReason (before proposed : State) : Prop :=

Defines a particular non-growth reason: construction lists match, the old inventory has length at most one, and the proposed one exceeds one.

L122  before.constructed = proposed.constructed ∧

A reason to retain the old state requires both states to have exactly the same constructed operations.

L123  before.inventory.length ≤ 1 ∧ ¬ proposed.inventory.length ≤ 1

The old inventory must fit the one-item limit while the proposed inventory exceeds it.

L125/- The policy, current capabilities, execution interface and workload constraints belong to one generating system. -/

Documents the following definition or result: Binds one owner's policy, current state, resource-dependent executor, budget and required operations.

L126structure GeneratingSystem where

Binds one owner's policy, current state, resource-dependent executor, budget and required operations.

L127  owner : Nat

Identifies the owner of this generating system.

L128  policy : Policy

Attaches the valuation and revisability policy to this same system.

L129  current : State

Stores the system's current represented capability and inventory state.

L130  execute : ExternalResources → Option Nat

Stores this system's actual resource-consuming execution function.

L131  applicationBudget : Nat

Specifies the inventory-size budget used to evaluate stable and proposed states.

L132  requiredOperations : List Operation

Specifies operations that the workload requires to remain constructed.

L133/- The modeled system uses the assisted interpreter under a one-item budget and a copy-operation requirement. -/

Documents the following definition or result: Instantiates owner zero with the open policy, base state, three-slot executor, budget one and required copy operation.

L134def generatingSystem : GeneratingSystem where

Instantiates owner zero with the open policy, base state, three-slot executor, budget one and required copy operation.

L135  owner := 0

Assigns owner identifier zero to the concrete generating system.

L136  policy := openPolicy

Installs openPolicy in that same concrete system.

L137  current := baseState

Sets its current capabilities and inventory to baseState.

L138  execute := assistedExecution

Uses the three-resource assisted interpreter as this system's execution interface.

L139  applicationBudget := 1

Sets this workload's inventory budget to exactly one item.

L140  requiredOperations := [.copy]

Requires the concrete workload to preserve the copy operation.

L141/- A stable action retains this system's own current state. -/

Documents the following definition or result: Returns this system's current state as its stability-preserving action.

L142def GeneratingSystem.stableAction (system : GeneratingSystem) : State := system.current

Returns this system's current state as its stability-preserving action.

L143def GeneratingSystem.requirementsMet (system : GeneratingSystem) (state : State) : Prop :=

Checks every operation required by this same system is constructed in the assessed state.

L144  ∀ operation, operation ∈ system.requiredOperations → operation ∈ state.constructed

For this system and proposed state, every required operation must occur in the state's constructed list.

L145def GeneratingSystem.withinBudget (system : GeneratingSystem) (state : State) : Prop :=

Compares the assessed state's inventory length against this system's declared budget.

L146  state.inventory.length ≤ system.applicationBudget

Checks the state's inventory count against this same system's declared application budget.

L147/- An expansion report identifies the actual before/after states and the operation/performance it asserts was added. -/

Documents the following definition or result: Stores reporting owner, exact before/after states, claimed new operation, tested input and expected output.

L148structure Announcement where

Stores reporting owner, exact before/after states, claimed new operation, tested input and expected output.

L149  owner : Nat

Records whose expansion announcement this is.

L150  before : State

Stores the exact baseline state named by the announcement.

L151  after : State

Stores the exact resulting state named by the announcement.

L152  reportedNewOperation : Operation

Names the operation alleged to be newly constructed.

L153  input : Nat

Fixes the input at which the announced operation's behavior is claimed.

L154  expectedOutput : Nat

Stores the claimed output of that operation at the stated input.

L155  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L156/- Reports are generated by this system and identify its actual current state as their baseline. -/

Documents the following definition or result: Builds a report from this system's owner/current state and the supplied proposal and operation contract.

L157def GeneratingSystem.report (system : GeneratingSystem) (after : State)

Builds a report from this system's owner/current state and the supplied proposal and operation contract.

L158    (operation : Operation) (input expectedOutput : Nat) : Announcement :=

Receives the allegedly new operation and the concrete input/output pair for this report.

L159  ⟨system.owner, system.current, after, operation, input, expectedOutput⟩

Builds a report tied to the system's owner and current baseline, using the supplied after-state and claim data.

L160/- Report content is interpreted against those very states and the named operation's actual behavior. -/

Documents the following definition or result: Requires the reported operation to be newly constructed and to produce the stated output at the stated input.

L161def Announcement.claim (report : Announcement) : Prop :=

Requires the reported operation to be newly constructed and to produce the stated output at the stated input.

L162  report.reportedNewOperation ∈ report.after.constructed ∧

The reported new operation must actually occur in the announcement's after-state.

L163  report.reportedNewOperation ∉ report.before.constructed ∧

The same operation must be absent from the announcement's baseline constructed list.

L164  report.reportedNewOperation.run report.input = report.expectedOutput

Its actual run at the reported input must equal the announced expected output.

L165/- A true report of this form entails a represented construction expansion. -/

Documents the following definition or result: Uses the genuinely new constructed operation from an assumed report claim as the expansion witness.

L166theorem announcementClaimImpliesExpansion (report : Announcement) (h : report.claim) :

Uses the genuinely new constructed operation from an assumed report claim as the expansion witness.

L167    Expanded report.before report.after := Or.inr ⟨report.reportedNewOperation, h.1, h.2.1⟩

Uses the claim's after-membership and before-absence to construct Expanded's construction branch.

L168/- This concrete self-report asserts a successor operation for the actual inventory-only inflation. -/

Documents the following definition or result: This system reports successor at input zero for an inventory-only inflation proposal.

L169def inflatedAnnouncement : Announcement := generatingSystem.report inflatedState .successor 0 1

This system reports successor at input zero for an inventory-only inflation proposal.

L170/- The report asserts a real successor result but its named operation is absent from its own after-state. -/

Documents the following definition or result: Computes the exact report objects and shows its claimed new operation and actual expansion both fail.

L171theorem inflatedAnnouncementRefuted :

Computes the exact report objects and shows its claimed new operation and actual expansion both fail.

L172    inflatedAnnouncement.before = baseState ∧ inflatedAnnouncement.after = inflatedState ∧

Confirms the concrete announcement refers to baseState and inflatedState themselves.

L173    inflatedAnnouncement.reportedNewOperation = .successor ∧

Confirms the alleged new operation is successor.

L174    inflatedAnnouncement.input = 0 ∧ inflatedAnnouncement.expectedOutput = 1 ∧

Confirms the announced test is input zero with expected output one.

L175    ¬ inflatedAnnouncement.claim ∧ ¬ Expanded inflatedAnnouncement.before inflatedAnnouncement.after := by

States both that the announcement's substantive claim fails and that its own state pair has no expansion.

L176  simp [inflatedAnnouncement, GeneratingSystem.report, generatingSystem, Announcement.claim, Expanded, baseState, inflatedState]

Computes the report fields and unchanged capability lists; successor is absent from the after-state despite its correct 0→1 behavior.

L178/- These transitions share one initial state; only extension adds an actual new operation. -/

Documents the following definition or result: Restricts the achievement model to inventory inflation and genuine operation extension.

L179inductive TransitionCase | inflate | extend

Restricts the achievement model to inventory inflation and genuine operation extension.

L180  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L182def extendedState : State :=

Adds successor to the base state's understanding and construction lists.

L183  { baseState with understood := [.copy, .successor], constructed := [.copy, .successor] }

Adds successor to both understood and constructed lists while retaining the baseline's other fields.

L184def transitionBefore (_transition : TransitionCase) : State := baseState

Both modeled transitions share the same base-state baseline.

L185def transitionAfter : TransitionCase → State

Chooses inflatedState or extendedState according to the transition constructor.

L186  | .inflate => inflatedState

The inflate transition ends at the inventory-only inflated state.

L187  | .extend => extendedState

The extend transition ends at the state with newly understood and constructed successor.

L188/- Both alternatives are assessed under the same concrete input condition. -/

Documents the following definition or result: Uses zero as the explicit tested input for both transition cases.

L189def transitionInput (_transition : TransitionCase) : Nat := 0

Uses zero as the explicit tested input for both transition cases.

L190def transitionAnnouncement (transition : TransitionCase) : Announcement :=

Reports successor output one at input zero for this same system and selected after-state.

L191  generatingSystem.report (transitionAfter transition) .successor (transitionInput transition) 1

Both alternatives announce successor at the shared input zero, but name their own actual after-state.

L193/- Eleven boundary branches share a content-bearing trace and executable dependency model. They do not assert a universal law of human capability. -/

Documents the following definition or result: Checks all concrete branches on the bound system: unchanged capability despite list inflation, resource dependence, justified stable action and an untrue same-object achievement report.

L194theorem generationLimits :

Checks all concrete branches on the bound system: unchanged capability despite list inflation, resource dependence, justified stable action and an untrue same-object achievement report.

L195    Generative generatingSystem.policy ∧

The concrete system retains the adopted generative policy.

L196    generatingSystem.policy.permitsVersion 0 0 ∧

Its policy allows keeping version zero, so generativity does not require every action to change versions.

L197    ¬ Expanded generatingSystem.current inflatedState ∧

Inflating this system's inventory does not expand its represented capabilities.

L198    generatingSystem.current.inventory.length < inflatedState.inventory.length ∧

The inflated state has strictly more inventory entries than this system's current state.

L199    generatingSystem.current.abstractionLayers.length < inflatedState.abstractionLayers.length ∧

Its abstraction-layer count also strictly increases without capability expansion.

L200    generatingSystem.current.vocabulary.length < inflatedState.vocabulary.length ∧

Its vocabulary count strictly increases under the same unchanged capability content.

L201    generatingSystem.execute availableResources = some 6 ∧

With resources 1,2,3, this system's execution actually returns some 6.

L202    generatingSystem.execute { availableResources with experience := none } = none ∧

Removing experience from that same resource bundle makes the system's execution fail.

L203    generatingSystem.execute { availableResources with knowledge := none } = none ∧

Removing knowledge alone likewise makes its execution return none.

L204    generatingSystem.execute { availableResources with collaborator := none } = none ∧

Removing the collaborator input alone also makes execution fail.

L205    generatingSystem.execute ⟨none, none, none⟩ = none ∧

With all three external inputs absent, this same execution interface returns none.

L206    ¬ Expanded generatingSystem.current generatingSystem.stableAction ∧

The system's stable action yields no represented capability expansion.

L207    generatingSystem.stableAction = generatingSystem.current ∧

That stable action is exactly retention of the system's current state.

L208    generatingSystem.requirementsMet generatingSystem.stableAction ∧

Retention preserves the workload's required copy operation.

L209    generatingSystem.withinBudget generatingSystem.stableAction ∧

The retained one-item state fits this system's one-item application budget.

L210    ¬ generatingSystem.withinBudget inflatedState ∧

The duplicated inventory has two entries and exceeds this same system's one-item budget.

L211    StableReason generatingSystem.current inflatedState ∧

Stability has the stated reason: construction is unchanged, but only the current state fits the budget.

L212    (inflatedAnnouncement = generatingSystem.report inflatedState .successor 0 1 ∧

Identifies the report as this system's announcement about inflatedState, successor, input zero and output one.

L213      inflatedAnnouncement.owner = generatingSystem.owner ∧

The report's owner equals this generating system's owner.

L214      inflatedAnnouncement.before = generatingSystem.current ∧ inflatedAnnouncement.after = inflatedState ∧

The report uses this system's current state as baseline and inflatedState as result.

L215      inflatedAnnouncement.reportedNewOperation = .successor ∧

The operation this actual report calls new is successor.

L216      inflatedAnnouncement.input = 0 ∧ inflatedAnnouncement.expectedOutput = 1 ∧

The report's claimed performance remains the concrete pair 0→1.

L217      ¬ inflatedAnnouncement.claim ∧ ¬ Expanded inflatedAnnouncement.before inflatedAnnouncement.after) := by

Despite that report, its claim is false and its own before/after pair has no capability expansion.

L218  simp [generatingSystem, GeneratingSystem.stableAction, GeneratingSystem.requirementsMet,

Begins computing all generationLimits clauses by exposing the concrete system, retention action and required-operation check.

L219    GeneratingSystem.withinBudget, GeneratingSystem.report, Generative, openPolicy, Expanded,

Also exposes the one-item budget, report constructor and policy/expansion predicates so their claims reduce to concrete data.

L220    baseState, inflatedState, assistedExecution, availableResources, Operation.run,

Uses the actual baseline/inflated lists and three-resource interpreter to decide the size, membership and execution results.

L221    StableReason, inflatedAnnouncement, Announcement.claim]

Finally unfolds the stability reason and owned announcement claim, completing all conjunction branches by computation.

L223/- The empty work log omits an actually applicable system assessment despite an open generative policy. -/

Documents the following definition or result: Exhibits a policy meeting generation while empty records fail the nonempty concrete reflexivity requirements.

L224theorem generationNotReflexivity :

Exhibits a policy meeting generation while empty records fail the nonempty concrete reflexivity requirements.

L225    Generative openPolicy ∧ ¬ Reflexive 0 (ownRules 0) [] := by

Combines a generative openPolicy with failure of owned reflexivity when the work log is empty.

L226  constructor

Separates establishing Generative from refuting the empty-log Reflexive claim.

L227  · simp [Generative, openPolicy]

Computes openPolicy's expansion valuation and unconditional revisability.

L228  · intro h

Assumes, for contradiction, that the empty log satisfies the owned reflexivity contract.

L229    have bad := noSelfExemption 0 (ownRules 0) [] h (assessingRule 0) (by simp [ownRules])

Applies noSelfExemption to the registered assessingRule, forcing a performed assessment from the assumed empty-log compliance.

L230      (.system 0) rfl (by simp [assessingRule, ownSubjects])

Chooses the very system subject with matching owner and proves that assessment is applicable to it.

L231    simp [Performed] at bad

Unfolding Performed reveals an impossible member of the empty work list.

L233/- The same proposed arithmetic principle is used in the self-test and in the universal correctness claim. -/

Documents the following definition or result: Decides the arithmetic equation n+1=2*n for each natural number.

L234def ownArithmeticPrinciple (n : Nat) : Bool := decide (n + 1 = 2 * n)

Decides the arithmetic equation n+1=2*n for each natural number.

L236def selfTest (samples : List Nat) : Bool := samples.all ownArithmeticPrinciple

Returns true precisely when the equation holds at every listed sample; no unlisted input is tested.

L238/- A genuine evaluation on the selected sample succeeds, while the same principle fails at zero. -/

Documents the following definition or result: Computes success on sample 1 and failure at 0, refuting universal success. This concerns the particular arithmetic predicate, not a universal impossibility theorem about all self-tests.

L239theorem selfTestDoesNotProve :

Computes success on sample 1 and failure at 0, refuting universal success. This concerns the particular arithmetic predicate, not a universal impossibility theorem about all self-tests.

L240    selfTest [1] = true ∧ ownArithmeticPrinciple 0 = false ∧

The same arithmetic principle passes sample 1 but evaluates false at 0.

L241      ¬ (∀ n, ownArithmeticPrinciple n = true) := by

Therefore that principle does not return true for every natural-number input.

L242  constructor

Separates the passing sample computation from the two failure claims.

L243  · decide

Evaluates the singleton sample: 1+1 equals 2×1, so selfTest [1] is true.

L244  constructor

Separates the concrete failure at zero from refuting universal success.

L245  · decide

Computes 0+1≠2×0, making ownArithmeticPrinciple 0 false.

L246  · intro h

Assumes the same principle succeeds for every input.

L247    have bad := h 0

Specializes that universal assumption to input zero.

L248    contradiction

Contradicts the computed false result at zero, refuting universal correctness.

L250end CoreReader.Agency

Closes the current namespace.