leanified/CoreReader/Choice.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 · 228 lines

LeanLine explanation

L1import CoreReader.Evidence

Import CoreReader.Evidence, making its checked declarations available to this module; this line states no new philosophical result.

L3namespace CoreReader.Choice

Open namespace CoreReader.Choice so subsequent declarations receive this module-qualified name.

L4open CoreReader.Logic CoreReader.Evidence

Make names from CoreReader.Logic CoreReader.Evidence available without qualification; this changes name resolution, not assumptions.

L6inductive StatusKind | name | convention | standing

Declare the alternatives StatusKind. Defines three status tags; no ranking or evidential meaning is attached by the datatype alone.

L7  deriving DecidableEq, Repr

Derive decidable equality and printable representations for these finite constructors; these are computational conveniences, not choice criteria.

L9inductive MethodReason | output | explanation | applicability | simplicity | procedure

Declare the alternatives MethodReason. Defines five method-reason tags whose actual content is supplied by MethodContent.

L10  deriving DecidableEq, Repr

Derive decidable equality and printable representations for these finite constructors; these are computational conveniences, not choice criteria.

L12inductive Reason | status (kind : StatusKind) | method (kind : MethodReason)

Declare the alternatives Reason. Separates tagged status reasons from tagged method reasons.

L13  deriving DecidableEq, Repr

Derive decidable equality and printable representations for these finite constructors; these are computational conveniences, not choice criteria.

L15/- An implementation has observable behavior, a stated domain, an explanation formula and an execution trace. -/

Document the intended scope of Implementation. The corresponding declaration concerns: Packages an implementation's metadata, behavior, cost, domain, explanation function and trace function as independently supplied fields. This comment is explanatory, not a proof premise.

L16structure Implementation where

Declare the data interface Implementation. Packages an implementation's metadata, behavior, cost, domain, explanation function and trace function as independently supplied fields.

L17  name : String

Store the implementation’s descriptive name; it does not confer priority.

L18  conventional : Bool

Record whether the implementation is conventional as a Boolean status fact.

L19  established : Bool

Record whether the implementation is established, independently of its actual behavior.

L20  run : Nat → Nat

Store the actual natural-number input/output function.

L21  cost : Nat

Store the cost checked against an application’s budget.

L22  domain : Nat → Prop

Store the implementation’s claimed domain as a predicate on inputs.

L23  explanation : Nat → Nat

Store explanatory output content to be compared with actual run results.

L24  trace : Nat → List Nat

Store an input-indexed execution trace whose last element can be compared with actual output.

L26/- An application selects relevant objectives and constraints; no universal ranking or score is prescribed. -/

Document the intended scope of Requirements. The corresponding declaration concerns: Packages the input scope, expected output, fixed budget and valued reason kinds. This comment is explanatory, not a proof premise.

L27structure Requirements where

Declare the data interface Requirements. Packages the input scope, expected output, fixed budget and valued reason kinds.

L28  inputs : Nat → Prop

Specify which inputs the application actually requires.

L29  expected : Nat → Nat

Specify the expected output at each input.

L30  budget : Nat

Specify the application’s budget constraint.

L31  values : MethodReason → Prop

Specify which method-reason categories this application values; this choice is an adopted input.

L33/- These are explicit, content-based interpretations of possible method reasons in this application. -/

Document the intended scope of MethodContent. The corresponding declaration concerns: Assigns a proposition to each method tag, using these particular behavioral and cost proxies. This comment is explanatory, not a proof premise.

L34def MethodContent (req : Requirements) (i : Implementation) : MethodReason → Prop

Define MethodContent. Assigns a proposition to each method tag, using these particular behavioral and cost proxies.

L35  | .output => ∀ x, req.inputs x → i.run x = req.expected x

An output reason requires this implementation’s actual output to equal the application’s expected output at every required input.

L36  | .explanation => ∀ x, req.inputs x → i.explanation x = i.run x

An explanation reason requires explanatory output to match this very implementation’s actual run at every required input.

L37  | .applicability => ∀ x, req.inputs x → i.domain x

An applicability reason requires every application-required input to belong to this implementation’s domain.

L38  | .simplicity => i.cost ≤ req.budget

The simplicity reason is the selected application’s actual cost-within-budget condition.

L39  | .procedure => ∀ x, req.inputs x → (i.trace x).getLast? = some (i.run x)

A procedure reason requires the actual trace’s last element to equal this implementation’s real output at every required input.

L41/- The extra choice commitment requires both selected relevance and actual reason content; pure status supplies neither. -/

Document the intended scope of Relevant. The corresponding declaration concerns: A reason is relevant when it is an allowed method kind whose content holds; status kinds are excluded outright. This comment is explanatory, not a proof premise.

L42def Relevant (req : Requirements) (i : Implementation) : Reason → Prop

Define Relevant. A reason is relevant when it is an allowed method kind whose content holds; status kinds are excluded outright.

L43  | .status _ => False

Status reasons are defined as irrelevant under this adopted choice norm, regardless of their status subtype.

L44  | .method kind => req.values kind ∧ MethodContent req i kind

A method reason must both belong to a category valued by these requirements and satisfy that category’s actual MethodContent.

L46def Feasible (req : Requirements) (i : Implementation) : Prop :=

Define Feasible. Feasibility requires universal requested-input output correctness and fixed cost within budget; it does not include explanation, domain or trace checks.

L47  (∀ x, req.inputs x → i.run x = req.expected x) ∧ i.cost ≤ req.budget

Feasibility requires correct actual output at every required input and actual cost within this application’s budget.

L49/- In this application, a relevant reason is eligible only after its stated output and budget requirements hold. -/

Document the intended scope of JustifiedChoice. The corresponding declaration concerns: Requires both output/budget feasibility and at least one listed valued method reason with its concrete content satisfied. This comment is explanatory, not a proof premise.

L50def JustifiedChoice (req : Requirements) (i : Implementation) (reasons : List Reason) : Prop :=

Define JustifiedChoice. Requires both output/budget feasibility and at least one listed valued method reason with its concrete content satisfied.

L51  Feasible req i ∧ ∃ reason ∈ reasons, Relevant req i reason

Require feasibility and at least one actually listed relevant reason; a relevant reason alone does not establish feasibility.

L53/- This proves the structural effect of the adopted choice commitment for each of its three status-only cases. -/

Document the intended scope of statusOnlyFails. The corresponding declaration concerns: For any requirements and implementation, a singleton status reason cannot justify choice because its relevance is defined as false. This comment is explanatory, not a proof premise.

L54theorem statusOnlyFails (req : Requirements) (i : Implementation) (k : StatusKind) :

State the checked result statusOnlyFails. For any requirements and implementation, a singleton status reason cannot justify choice because its relevance is defined as false.

L55    ¬ JustifiedChoice req i [.status k] := by

Deny justified selection when the only listed reason is status, for the supplied arbitrary requirements and implementation.

L56  rintro ⟨_, reason, hr, hv⟩

Unpack an alleged status-only justified choice, extracting its listed reason and proof of relevance; feasibility alone cannot supply the missing relevance.

L57  simp only [List.mem_singleton] at hr

Simplify singleton membership to show that the extracted reason is exactly the given status reason.

L58  subst reason

Substitute the identified status reason into its alleged relevance proof.

L59  exact hv

Relevance of a status reason is defined as False, so the extracted hv is already a contradiction.

L61def identityImpl : Implementation where

Define identityImpl. Builds an identity implementation with both status flags true, cost one, unrestricted domain, matching explanation and singleton output trace.

L62  name := "Existing identity implementation"

Name the concrete existing identity implementation without using its name as a proof of quality.

L63  conventional := true

Mark the identity implementation’s conventional and established status as true; these facts remain distinct from its actual method reasons.

L64  established := true

Mark the identity implementation’s conventional and established status as true; these facts remain distinct from its actual method reasons.

L65  run n := n

Define actual identity output as the unchanged input n.

L66  cost := 1

Set identity’s actual cost to 1.

L67  domain _ := True

Let identity’s applicability domain contain all natural inputs.

L68  explanation n := n

Provide an explanatory result equal to the input, matching identity’s actual output.

L69  trace n := [n]

Use the singleton input as the actual trace, whose last element equals identity’s output.

L71def successorImpl : Implementation where

Define successorImpl. Builds a successor implementation with false status flags, cost two, unrestricted domain, matching explanation and a two-entry trace.

L72  name := "Successor implementation"

Name the alternative successor implementation.

L73  conventional := false

Mark successor as neither conventional nor established in this example; this status alone does not determine feasibility.

L74  established := false

Mark successor as neither conventional nor established in this example; this status alone does not determine feasibility.

L75  run n := n + 1

Define successor’s actual output as n+1.

L76  cost := 2

Set its original cost to 2, above the identity application’s budget 1.

L77  domain _ := True

Let successor’s applicability domain also include every natural input.

L78  explanation n := n + 1

Provide its explanatory result n+1, faithful to its own actual output.

L79  trace n := [n, n + 1]

Record input and then actual successor output in its trace.

L81def changedOutsideZero : Implementation :=

Define changedOutsideZero. Copies identity metadata/fields except the explicitly replaced ones, producing an implementation equal at zero but different elsewhere.

L82  { identityImpl with

Start from identityImpl’s fields and explicitly override the following components.

L83    name := "Changed outside zero"

Name the modified implementation by its change outside input zero.

L84    conventional := false

Change this modified implementation’s conventional/established flags to false.

L85    established := false

Change this modified implementation’s conventional/established flags to false.

L86    run := fun n => if n = 0 then 0 else n + 1

Keep output 0 at input 0 but return n+1 at every other input.

L87    explanation := fun n => if n = 0 then 0 else n + 1

Make its explanation follow the same actual piecewise output function.

L88    trace := fun n => [if n = 0 then 0 else n + 1] }

Use that same piecewise result as its singleton trace; finish the implementation override.

L90def identityRequirements : Requirements where

Define identityRequirements. Requires identity behavior at all natural inputs, budget one, and values every method-reason kind.

L91  inputs _ := True

Require every natural-number input in the identity application.

L92  expected n := n

Set the desired output to the unchanged input.

L93  budget := 1

Adopt budget 1 for the application.

L94  values _ := True

Admit all represented method-reason categories; their actual content must still be checked.

L96def objectiveReason : List Reason := [.method .output]

Define objectiveReason. Defines a reason list containing only the output-correctness method tag.

L98theorem identityOutputReason : Relevant identityRequirements identityImpl (.method .output) := by

State the checked result identityOutputReason. Proves the identity implementation has a relevant output reason under universal identity requirements by definitional output equality. The following tactic block proves this explicit type.

L99  exact ⟨trivial, fun _ _ => rfl⟩

The output reason is admitted by these requirements, and identityImpl’s actual output equals the expected output at every allowed input by reflexivity.

L101theorem identityFeasible : Feasible identityRequirements identityImpl :=

State the checked result identityFeasible. Proves universal identity output and cost one within budget one. The supplied proof term uses the displayed constructed witnesses or earlier lemmas, rather than adding an axiom.

L102  ⟨fun _ _ => rfl, by decide⟩

For identity, every required output is correct by reflexivity; compute cost 1 within budget 1.

L104theorem identityJustified : JustifiedChoice identityRequirements identityImpl objectiveReason :=

State the checked result identityJustified. Uses the output reason as the existential witness justifying identity under the given requirements. The supplied proof term uses the displayed constructed witnesses or earlier lemmas, rather than adding an axiom.

L105  ⟨identityFeasible, .method .output, by simp [objectiveReason], identityOutputReason⟩

Combine identity’s feasibility with the actual output reason, prove it belongs to objectiveReason and supply its content-based relevance.

L107/- A conventional existing implementation can be selected for an actual requirement, not for status alone. -/

Document the intended scope of conventionWithReason. The corresponding declaration concerns: Shows conventional and established metadata can coexist with justified choice when the list also contains a valid output reason; status does not provide the witness. This comment is explanatory, not a proof premise.

L108theorem conventionWithReason :

State the checked result conventionWithReason. Shows conventional and established metadata can coexist with justified choice when the list also contains a valid output reason; status does not provide the witness.

L109    identityImpl.conventional = true ∧ identityImpl.established = true ∧

Keep both actual status facts true for identity.

L110    JustifiedChoice identityRequirements identityImpl [.status .convention, .method .output] := by

Claim justified selection using a list containing convention and an actual output reason; the output reason supplies relevance.

L111  exact ⟨rfl, rfl, identityFeasible, .method .output, by simp, identityOutputReason⟩

Compute the conventional/established status facts, retain actual feasibility, and select the listed output reason with its separately proved relevance.

L113inductive Candidate | identity | successor

Declare the alternatives Candidate. Closes the candidate universe to exactly identity and successor.

L114  deriving DecidableEq, Repr

Derive decidable equality and printable representations for these finite constructors; these are computational conveniences, not choice criteria.

L116def implementation : Candidate → Implementation

Define implementation. Maps each of the two candidate constructors to its concrete implementation.

L117  | .identity => identityImpl

Interpret the identity candidate as the actual identityImpl object.

L118  | .successor => successorImpl

Interpret the successor candidate as the actual successorImpl object.

L120/- Feasibility is decided by the same stated behavior and resource requirement for either candidate. -/

Document the intended scope of singleFeasible. The corresponding declaration concerns: Proves identity is the sole feasible member of the two-constructor candidate type under identity requirements, and separately supplies its output justification. This comment is explanatory, not a proof premise.

L121theorem singleFeasible :

State the checked result singleFeasible. Proves identity is the sole feasible member of the two-constructor candidate type under identity requirements, and separately supplies its output justification.

L122    (∀ candidate, Feasible identityRequirements (implementation candidate) ↔ candidate = .identity) ∧

Over the explicitly two-valued candidate type, require feasibility exactly for identity.

L123    JustifiedChoice identityRequirements identityImpl objectiveReason := by

Also retain identity’s actual output-reason justification.

L124  constructor

Separate the exact feasible-candidate characterization from the existing proof of identity’s justified selection.

L125  · intro candidate

Fix any candidate in the explicit identity/successor type before checking its feasibility equivalence.

L126    cases candidate

Exhaust the actual two-candidate type: identity or successor; no unlisted implementation is considered.

L127    · simp [Feasible, identityRequirements, implementation, identityImpl]

For identity, unfold actual outputs and cost; the identity-output and budget conditions are satisfied.

L128    · simp [Feasible, identityRequirements, implementation, successorImpl]

For successor, unfold the same requirements; the candidate cannot meet identity outputs and its original cost also exceeds the budget.

L129  · exact identityJustified

Reuse identityJustified to finish the concrete selected-candidate obligation.

L131/- The same observed input can conceal a relevant difference at another input. -/

Document the intended scope of localNotGlobal. The corresponding declaration concerns: Shows identity and the piecewise implementation agree when input is zero but disagree at input one; this refutes inference from local agreement to global equality. This comment is explanatory, not a proof premise.

L132theorem localNotGlobal :

State the checked result localNotGlobal. Shows identity and the piecewise implementation agree when input is zero but disagree at input one; this refutes inference from local agreement to global equality.

L133    (∀ x, x = 0 → identityImpl.run x = changedOutsideZero.run x) ∧

Compare actual outputs only under the input-0 scope.

L134    identityImpl.run 1 ≠ changedOutsideZero.run 1 := by

Separately require a real output difference at input 1.

L135  constructor

Separate equality under the input-0 scope from actual inequality at input 1.

L136  · intro x hx; subst x; rfl

Substitute the local-scope assumption x=0; the two implementations then have definitionally equal outputs.

L137  · decide

Compute their actual outputs at input 1 to verify the claimed inequality.

L139/- This candidate is cheap enough but misses the required identity output. -/

Document the intended scope of cheapSuccessor. The corresponding declaration concerns: Lowers successor's fixed cost to one without fixing its identity-output failure. This comment is explanatory, not a proof premise.

L140def cheapSuccessor : Implementation := { successorImpl with cost := 1 }

Define cheapSuccessor. Lowers successor's fixed cost to one without fixing its identity-output failure.

L142theorem eligibleInternalReasonNotSufficient :

State the checked result eligibleInternalReasonNotSufficient. Shows cost simplicity is relevant for cheap successor, yet output infeasibility prevents justified choice.

L143    Relevant identityRequirements cheapSuccessor (.method .simplicity) ∧

Require that cheapSuccessor’s cost reason is actually relevant under the chosen requirements.

L144    ¬ JustifiedChoice identityRequirements cheapSuccessor [.method .simplicity] := by

Nevertheless reject its justified choice with that reason alone because feasibility includes correct outputs.

L145  refine ⟨⟨trivial, by change 1 ≤ 1; decide⟩, ?_⟩

Show the cheap successor has an admitted cost reason with cost 1 ≤ budget 1, then separately refute justified choice.

L146  intro h

Assume cheapSuccessor is justified using its cost reason, in order to extract and refute its required output feasibility.

L147  have bad := h.1.1 0 trivial

An alleged justified choice includes feasible outputs; apply that requirement at input 0, where successor returns 1 instead of expected 0.

L148  cases bad

Eliminate the resulting impossible output equality; a relevant cost reason did not repair the wrong output.

L150/- Each of the four internal-method reasons is eligible because of its actual selected requirement and content. -/

Document the intended scope of internalReasons. The corresponding declaration concerns: Provides four valid internal reasons for identity and a cost-relevant successor counterexample to automatic sufficiency. This comment is explanatory, not a proof premise.

L151theorem internalReasons :

State the checked result internalReasons. Provides four valid internal reasons for identity and a cost-relevant successor counterexample to automatic sufficiency.

L152    Relevant identityRequirements identityImpl (.method .explanation) ∧

Require a faithful explanation reason for the same actual identity implementation.

L153    Relevant identityRequirements identityImpl (.method .applicability) ∧

Require its actual applicability to cover the required inputs.

L154    Relevant identityRequirements identityImpl (.method .simplicity) ∧

Require its actual cost to meet the valued simplicity/budget condition.

L155    Relevant identityRequirements identityImpl (.method .procedure) ∧

Require its actual trace content to meet the valued procedure condition.

L156    (Relevant identityRequirements cheapSuccessor (.method .simplicity) ∧

Include a separate cheap-successor case where its cost reason is eligible.

L157      ¬ JustifiedChoice identityRequirements cheapSuccessor [.method .simplicity]) := by

That cheap candidate still fails justified selection; the combined theorem begins its proof here.

L158  exact ⟨⟨trivial, fun _ _ => rfl⟩, ⟨trivial, fun _ _ => trivial⟩,

Provide admitted, actually faithful explanation and applicability reasons for identity, checking their content at every required input.

L159    ⟨trivial, by change 1 ≤ 1; decide⟩, ⟨trivial, fun _ _ => rfl⟩, eligibleInternalReasonNotSufficient⟩

Provide the actual budget and trace reasons, then include the cheap-but-wrong example showing relevance alone is insufficient.

L161/- Openness about reasons does not make two actual behaviors identical or reject the existing implementation. -/

Document the intended scope of openNotEquivalent. The corresponding declaration concerns: Combines identity's justification with differing identity/successor outputs at zero. It proves behavioral distinction between these examples, not a general openness property. This comment is explanatory, not a proof premise.

L162theorem openNotEquivalent :

State the checked result openNotEquivalent. Combines identity's justification with differing identity/successor outputs at zero. It proves behavioral distinction between these examples, not a general openness property.

L163    JustifiedChoice identityRequirements identityImpl objectiveReason ∧

Retain justified selection of the existing identity implementation based on its actual output reason.

L164    identityImpl.run 0 ≠ successorImpl.run 0 := by

Also require that identity and successor actually produce different outputs at input 0.

L165  exact ⟨identityJustified, by decide⟩

Retain the existing identity justification and compute the distinct actual outputs of identity and successor at 0.

L167/- A priority interpretation chooses one of the same two actual implementations. -/

Document the intended scope of priorityClaim. The corresponding declaration concerns: Defines the priority claim as selection of the identity constructor. This comment is explanatory, not a proof premise.

L168def priorityClaim : Claim Candidate := fun selected => selected = .identity

Define priorityClaim. Defines the priority claim as selection of the identity constructor.

L170def statusFacts : Theory Candidate := union

Define statusFacts. Forms a theory containing two status facts about identity that are constant across candidate worlds.

L171  (singleton (fun _ => identityImpl.conventional = true))

The first status premise records actual conventional status of identity, regardless of the candidate interpretation.

L172  (singleton (fun _ => identityImpl.established = true))

The second status premise records actual established status of that same implementation.

L174/- Both interpretations have exactly the same true conventional and established status facts. -/

Document the intended scope of statusFactsModel. The corresponding declaration concerns: Proves every candidate world models these status facts because both concern fixed metadata, independent of selection. This comment is explanatory, not a proof premise.

L175theorem statusFactsModel (selected : Candidate) : Models statusFacts selected := by

State the checked result statusFactsModel. Proves every candidate world models these status facts because both concern fixed metadata, independent of selection. The following tactic block proves this explicit type.

L176  exact (modelsUnion _ _ _).2 ⟨(modelsSingleton _ _).2 rfl, (modelsSingleton _ _).2 rfl⟩

Both status predicates concern the same actual identity implementation and are true independently of which candidate interpretation is selected; combine their singleton models.

L178def priorityArticulation : Articulation Candidate :=

Define priorityArticulation. Constructs a nonempty articulation of the constant status theory, with the same two status predicates as reasons and unrestricted limits.

L179  ⟨["priority", "conventional use", "established status"], statusFacts,

Articulate priority and actual status concepts using statusFacts as the premise theory.

L180    [fun _ => identityImpl.conventional = true, fun _ => identityImpl.established = true],

List the same actual conventional and established facts as articulated reasons.

L181    fun _ => True⟩

Use unrestricted candidate scope for this status-priority articulation.

L183/- This procedure reports whether the actual status premises entail that very priority claim over its stated two-candidate scope. -/

Document the intended scope of AssessmentAccurate. The corresponding declaration concerns: Defines report accuracy as equivalence between report=true and semantic entailment of the priority claim by status facts. This comment is explanatory, not a proof premise.

L184def AssessmentAccurate (report : Bool) : Prop :=

Define AssessmentAccurate. Defines report accuracy as equivalence between report=true and semantic entailment of the priority claim by status facts.

L185  report = true ↔ Entails statusFacts priorityClaim

Define report accuracy by equivalence between report=true and semantic entailment of this exact priority question from these status facts.

L187theorem statusDoesNotEntailPriority : ¬ Entails statusFacts priorityClaim := by

State the checked result statusDoesNotEntailPriority. Refutes priority entailment using successor, which models all fixed identity-status facts but is not identity. The following tactic block proves this explicit type.

L188  intro h

Assume the actual status facts entail identity priority across all candidate interpretations.

L189  have bad := h .successor (statusFactsModel .successor)

Apply alleged status-to-priority entailment to successor, which satisfies all the same true status facts but is not identity.

L190  cases bad

Distinct candidate constructors refute the priority equality derived at successor.

L192theorem statusAssessmentNonEntailment :

State the checked result statusAssessmentNonEntailment. Retains the original factual countermodel: status facts are articulated and accurately assessed but do not entail identity priority.

L193    Articulated priorityArticulation ∧ AssessmentAccurate false ∧

Require procedural articulation and a correctly negative report for the same status-priority assessment.

L194    (∀ selected, Models statusFacts selected) ∧

Keep all candidate interpretations as models of the same actual status facts.

L195    priorityClaim .identity ∧ ¬ priorityClaim .successor ∧

The priority predicate holds at identity and fails at successor.

L196    ¬ Entails statusFacts priorityClaim ∧

Deny entailment of that priority predicate from status facts alone.

L197    ¬ JustifiedChoice identityRequirements identityImpl [.status .standing] := by

Also reject selecting identity with standing as the only actual reason.

L198  refine ⟨⟨by simp [priorityArticulation], by simp [priorityArticulation]⟩,

Check that priorityArticulation has nonempty concepts and actual status reasons.

L199    ⟨(by intro h; cases h), (fun h => False.elim (statusDoesNotEntailPriority h))⟩,

Prove report=false is accurate: it cannot equal true, and any entailment assumption contradicts the actual successor countermodel.

L200    statusFactsModel, rfl, (by intro h; cases h), statusDoesNotEntailPriority,

Retain models of the same facts for both candidates, priority at identity but not successor, and the established failed entailment.

L201    statusOnlyFails _ _ _⟩

Reuse the general status-only failure theorem for the explicit identity choice with standing as its sole reason.

L203/- An assessment identifies the exact premises and priority question whose entailment it reports. -/

Document the intended scope of PriorityAssessment. The corresponding declaration concerns: Stores the actual premise theory, question and Boolean assessment report independently of a choice policy. This comment is explanatory, not a proof premise.

L204structure PriorityAssessment where

Declare the data interface PriorityAssessment. Stores the actual premise theory, question and Boolean assessment report independently of a choice policy.

L205  premises : Theory Candidate

Store the actual premise theory audited by this assessment.

L206  question : Claim Candidate

Store the exact priority claim whose entailment is assessed.

L207  report : Bool

Store the reported Boolean answer separately from facts and question.

L208/- Accuracy concerns the actual reported entailment question, independently of a later choice policy. -/

Document the intended scope of PriorityAssessment.accurate. The corresponding declaration concerns: Matches the report to semantic entailment for this exact premise/question pair. This comment is explanatory, not a proof premise.

L209def PriorityAssessment.accurate (assessment : PriorityAssessment) : Prop :=

Define PriorityAssessment.accurate. Matches the report to semantic entailment for this exact premise/question pair.

L210  assessment.report = true ↔ Entails assessment.premises assessment.question

Require this assessment’s actual report to agree exactly with entailment from its own premises to its own question.

L211/- Both policies receive this same correctly negative status-only priority audit. -/

Document the intended scope of statusPriorityAudit. The corresponding declaration concerns: Records a false entailment report for the actual fixed status facts and priority question. This comment is explanatory, not a proof premise.

L212def statusPriorityAudit : PriorityAssessment := ⟨statusFacts, priorityClaim, false⟩

Define statusPriorityAudit. Records a false entailment report for the actual fixed status facts and priority question.

L213/- Priority reasons are a policy component independent of the assessment's report and objects. -/

Document the intended scope of ChoicePolicy. The corresponding declaration concerns: Separates chosen candidate, priority reasons and the independently stored assessment. This comment is explanatory, not a proof premise.

L214structure ChoicePolicy where

Declare the data interface ChoicePolicy. Separates chosen candidate, priority reasons and the independently stored assessment.

L215  selected : Candidate

Store the candidate this policy actually selects.

L216  priorityReasons : List Reason

Store the policy’s actual priority reasons independently of its assessment record.

L217  assessment : PriorityAssessment

Store the actual assessment whose procedure the policy completed.

L218/- This is completion of the specified assessment procedure only, not full compliance with philosophical Grounds. -/

Document the intended scope of GeneralAssessmentFulfilled. The corresponding declaration concerns: Requires nonempty actual articulation and the exact accurate status audit, without imposing the additional choice criterion. This comment is explanatory, not a proof premise.

L219def GeneralAssessmentFulfilled (policy : ChoicePolicy) : Prop :=

Define GeneralAssessmentFulfilled. Requires nonempty actual articulation and the exact accurate status audit, without imposing the additional choice criterion.

L220  Articulated priorityArticulation ∧ policy.assessment = statusPriorityAudit ∧ policy.assessment.accurate

Require nonempty articulation, exactly the shared statusPriorityAudit, and its accuracy; this is specified procedure fulfillment, not full philosophical Grounds.

L221/- The additional choice norm separately tests the reasons actually used to prioritize the selected implementation. -/

Document the intended scope of AdditionalChoiceNorm. The corresponding declaration concerns: Applies the separate feasibility-and-relevance choice norm to this policy's selected implementation and reasons. This comment is explanatory, not a proof premise.

L222def AdditionalChoiceNorm (policy : ChoicePolicy) : Prop :=

Define AdditionalChoiceNorm. Applies the separate feasibility-and-relevance choice norm to this policy's selected implementation and reasons.

L223  JustifiedChoice identityRequirements (implementation policy.selected) policy.priorityReasons

Separately apply JustifiedChoice to the policy’s actual selected implementation and its actual reason list.

L224/- This policy retains status alone as its priority reason despite receiving the correctly negative status audit. -/

Document the intended scope of statusPriorityPolicy. The corresponding declaration concerns: Selects identity solely on standing while retaining the accurate non-entailment audit. This comment is explanatory, not a proof premise.

L225def statusPriorityPolicy : ChoicePolicy := ⟨.identity, [.status .standing], statusPriorityAudit⟩

Define statusPriorityPolicy. Selects identity solely on standing while retaining the accurate non-entailment audit.

L226/- This policy selects the same implementation using its actual relevant output reason after the same audit. -/

Document the intended scope of outputPriorityPolicy. The corresponding declaration concerns: Keeps the same choice and audit but uses the actual output reason. This comment is explanatory, not a proof premise.

L227def outputPriorityPolicy : ChoicePolicy := ⟨.identity, objectiveReason, statusPriorityAudit⟩

Define outputPriorityPolicy. Keeps the same choice and audit but uses the actual output reason.

L228/- The shared negative result is mathematically accurate for its actual status premises and question. -/

Document the intended scope of statusPriorityAuditAccurate. The corresponding declaration concerns: Uses the successor countermodel to establish the recorded false entailment report is accurate. This comment is explanatory, not a proof premise.

L229theorem statusPriorityAuditAccurate : statusPriorityAudit.accurate := by

State the checked result statusPriorityAuditAccurate. Uses the successor countermodel to establish the recorded false entailment report is accurate. The following tactic block proves this explicit type.

L230  constructor

Split accuracy of the negative audit into the two directions of its equivalence with entailment.

L231  · intro h; cases h

The audit’s actual false report cannot equal true, so this direction has an impossible premise.

L232  · intro h; exact False.elim (statusDoesNotEntailPriority h)

Any asserted entailment contradicts statusDoesNotEntailPriority; this establishes the reverse accuracy direction for the false report.

L233/- These independently variable policies share facts, selected implementation and completed audit, but differ on the extra choice norm. -/

Document the intended scope of PolicyIndependenceExample. The corresponding declaration concerns: Requires two policies with the same actual selection/audit but different reasons, both satisfying represented assessment duties and only the output policy satisfying the extra norm. This comment is explanatory, not a proof premise.

L234def PolicyIndependenceExample : Prop :=

Define PolicyIndependenceExample. Requires two policies with the same actual selection/audit but different reasons, both satisfying represented assessment duties and only the output policy satisfying the extra norm.

L235  statusPriorityPolicy.selected = outputPriorityPolicy.selected ∧

Fix identical selected candidates in both policies.

L236  statusPriorityPolicy.assessment = outputPriorityPolicy.assessment ∧

Fix the same actual assessment in both policies.

L237  statusPriorityPolicy.assessment.premises = statusFacts ∧

Bind that assessment’s premises to the actual shared statusFacts.

L238  statusPriorityPolicy.assessment.question = priorityClaim ∧

Bind its question to the same priorityClaim.

L239  statusPriorityPolicy.assessment.report = false ∧

Fix the common report to false, rather than allowing policy changes to alter the audit answer.

L240  (∀ selected, Models statusPriorityPolicy.assessment.premises selected) ∧

Retain models of these same assessment premises for every candidate interpretation.

L241  statusPriorityPolicy.priorityReasons ≠ outputPriorityPolicy.priorityReasons ∧

Require the actual priority reason lists to differ despite the shared candidate and audit.

L242  GeneralAssessmentFulfilled statusPriorityPolicy ∧ GeneralAssessmentFulfilled outputPriorityPolicy ∧

Require both policies to complete the same specified assessment procedure accurately.

L243  ¬ AdditionalChoiceNorm statusPriorityPolicy ∧ AdditionalChoiceNorm outputPriorityPolicy

Require opposite results under the additional choice norm: status fails, output passes.

L244/- Changing the actual priority reasons changes choice compliance while the accurate audit remains identical. -/

Document the intended scope of policyIndependenceExample. The corresponding declaration concerns: Constructs both independent policy objects and combines actual audit accuracy with status rejection and output justification. This comment is explanatory, not a proof premise.

L245theorem policyIndependenceExample : PolicyIndependenceExample := by

State the checked result policyIndependenceExample. Constructs both independent policy objects and combines actual audit accuracy with status rejection and output justification. The following tactic block proves this explicit type.

L246  have articulated : Articulated priorityArticulation :=

Construct one shared nonempty articulation of the actual status-priority question for both policies.

L247    ⟨by simp [priorityArticulation], by simp [priorityArticulation]⟩

Construct one shared nonempty articulation of the actual status-priority question for both policies.

L248  refine ⟨rfl,rfl,rfl,rfl,rfl,statusFactsModel,?_,

Fix identical selected candidate, audit, premises, question and false report; retain actual fact models and leave the difference in reason lists.

L249    ⟨articulated,rfl,statusPriorityAuditAccurate⟩,

Show the status-only policy completed that exact articulated audit with its mathematically accurate report.

L250    ⟨articulated,rfl,statusPriorityAuditAccurate⟩,?_,?_⟩

Supply the identical fulfilled audit for the output policy, leaving the two separate additional-choice-norm results.

L251  · decide

Compute that status-only and output-based priority reason lists are distinct despite their shared selected candidate and audit.

L252  · exact statusOnlyFails identityRequirements identityImpl .standing

Apply statusOnlyFails to the actual status policy’s priority reason, proving failure of AdditionalChoiceNorm.

L253  · exact identityJustified

Use identityJustified for the output policy’s actual relevant output reason, proving its AdditionalChoiceNorm.

L255/- A correctly articulated, completed negative assessment does not enforce the additional selection rule.

Document the intended scope of generalGroundsNotChoice. The corresponding declaration concerns: Combines the factual non-entailment case with a separate policy-level countermodel to deriving the added choice norm from represented general assessment duties. This comment is explanatory, not a proof premise.

L256This is only independence from represented assessment procedures: keeping this unsupported priority would fail general support proportionality too. -/

Document the intended scope of generalGroundsNotChoice. The corresponding declaration concerns: Combines the factual non-entailment case with a separate policy-level countermodel to deriving the added choice norm from represented general assessment duties. This comment is explanatory, not a proof premise.

L257theorem generalGroundsNotChoice :

State the checked result generalGroundsNotChoice. Combines the factual non-entailment case with a separate policy-level countermodel to deriving the added choice norm from represented general assessment duties.

L258    (Articulated priorityArticulation ∧ AssessmentAccurate false ∧

Retain the original articulated, accurately negative status assessment as part of the registered result.

L259      (∀ selected, Models statusFacts selected) ∧

Keep the same actual status premises modeled by every candidate.

L260      priorityClaim .identity ∧ ¬ priorityClaim .successor ∧

Keep priority true for identity and false for successor.

L261      ¬ Entails statusFacts priorityClaim ∧

Keep the demonstrated status-to-priority non-entailment.

L262      ¬ JustifiedChoice identityRequirements identityImpl [.status .standing]) ∧

Keep status-only choice failure, then join it to the stronger policy-independence example.

L263    PolicyIndependenceExample :=

Include actual policy variation through PolicyIndependenceExample, rather than ending at status non-entailment.

L264  ⟨statusAssessmentNonEntailment, policyIndependenceExample⟩

Pair the preserved status non-entailment proof with policyIndependenceExample, thereby including actual independent priority-reason variation in the registered theorem.

L266end CoreReader.Choice

Close namespace CoreReader.Choice; this adds no proof or premise.