leanified/CoreReader/Evidence.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 · 721 lines

LeanLine explanation

L1import CoreReader.Logic

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

L2import CoreReader.Agency

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

L4namespace CoreReader.Evidence

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

L5open CoreReader.Logic

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

L6open CoreReader.Agency

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

L8/- An observation records the outcome of a specified test on the represented world. -/

Document the intended scope of Record. The corresponding declaration concerns: A record packages a supplied Boolean test and its supplied observed result; provenance and measurement reliability are not fields. This comment is explanatory, not a proof premise.

L9structure Record (W : Type) where

Declare the data interface Record. A record packages a supplied Boolean test and its supplied observed result; provenance and measurement reliability are not fields.

L10  test : W → Bool

Store a specified Boolean test that reads the actual represented world.

L11  observed : Bool

Store the observed Boolean outcome to which that test will be compared.

L12/- Compatible worlds reproduce the actual contents of every recorded observation. -/

Document the intended scope of Compatible. The corresponding declaration concerns: A world is compatible when every listed test yields its recorded result. The empty record list admits every world. This comment is explanatory, not a proof premise.

L13def Compatible {W : Type} (records : List (Record W)) (w : W) : Prop :=

Define Compatible. A world is compatible when every listed test yields its recorded result. The empty record list admits every world.

L14  ∀ r, r ∈ records → r.test w = r.observed

Require every listed record’s actual test at w to equal that record’s observed outcome.

L15/- Inferential support requires the same claim in every evidence-compatible world. -/

Document the intended scope of Supports. The corresponding declaration concerns: Support means that the claim holds in every compatible modeled world. It is semantic entailment from records, not a statistical confidence measure. This comment is explanatory, not a proof premise.

L16def Supports {W : Type} (records : List (Record W)) (claim : Claim W) : Prop :=

Define Supports. Support means that the claim holds in every compatible modeled world. It is semantic entailment from records, not a statistical confidence measure.

L17  ∀ w, Compatible records w → claim w

Require the very claim to hold in every world compatible with all records; absent compatible worlds this implication alone can be vacuous.

L18/- Articulation identifies concepts, premises, reason contents and an application limit. -/

Document the intended scope of Articulation. The corresponding declaration concerns: Packages concept strings, an assumption theory, a list of reason claims, and a scope/limits claim. This comment is explanatory, not a proof premise.

L19structure Articulation (W : Type) where

Declare the data interface Articulation. Packages concept strings, an assumption theory, a list of reason claims, and a scope/limits claim.

L20  concepts : List String

Store identifiable concept names; strings alone do not establish semantic adequacy.

L21  assumptions : Theory W

Store the actual theory stated as the articulation’s assumptions.

L22  reasons : List (Claim W)

Store reason contents as propositions about the same world type.

L23  limits : Claim W

Store the actual application-limit predicate for those reasons.

L24/- Nonempty identifiable concepts and reasons are procedural articulation requirements. -/

Document the intended scope of Articulated. The corresponding declaration concerns: Checks only that concept and reason lists are nonempty; it does not establish truth, relevance, or a relation to the target claim. This comment is explanatory, not a proof premise.

L25def Articulated {W : Type} (a : Articulation W) : Prop :=

Define Articulated. Checks only that concept and reason lists are nonempty; it does not establish truth, relevance, or a relation to the target claim.

L26  a.concepts ≠ [] ∧ a.reasons ≠ []

Require nonempty concept and reason lists only; this procedural condition is weaker than matching, discharged Grounds.

L27/- This application model interprets an adopted option through its actual outcomes and stated goals/constraints. -/

Document the intended scope of ValuePosition. The corresponding declaration concerns: Represents an adopted option, selected option, option-indexed outcomes/reasons, objectives, constraints, starting theory, scope and criticism response; this is a disclosed application adapter. This comment is explanatory, not a proof premise.

L28structure ValuePosition (W : Type) where

Declare the data interface ValuePosition. Represents an adopted option, selected option, option-indexed outcomes/reasons, objectives, constraints, starting theory, scope and criticism response; this is a disclosed application adapter.

L29  Position : Type

Supply the type of options among which this value position adopts one.

L30  Outcome : Type

Supply the outcome type used to interpret the effects of each option.

L31  adopted : Position

Specify which option is adopted, separately from which option a world actually selects.

L32  selected : W → Position

Read the actually selected option from each world.

L33  outcome : W → Position → Outcome

Interpret the actual outcome of each option at each world, rather than storing an arbitrary support label.

L34  objective : Outcome → Prop

State the adopted objective as a predicate on outcomes; its value authority is not proved by this field.

L35  constraints : W → Position → Prop

State the world- and option-specific constraints checked alongside the objective.

L36  starting : Theory W

Store the starting theory; JointAdoption will require it to share a real model with adoption and reasons.

L37  reasons : List (W → Position → Prop)

Store reasons parameterized by both world and option, so switching the adopted option changes the assessed reasons.

L38  limits : Claim W

Specify the scope within which this value-assessment procedure claims its conclusions.

L39  relevantCriticism : Claim W

Identify which worlds present relevant criticism; this is an explicit application predicate.

L40  response : W → Option String

Store an optional textual response at each world; its presence does not prove that the criticism is answered adequately.

L41/- The adopted position's claim is derived from the same selected option used by the outcome interpretation. -/

Document the intended scope of ValuePosition.commitment. The corresponding declaration concerns: The commitment claim says the world selects this position's adopted option; it is no longer a freely relabeled separate claim field. This comment is explanatory, not a proof premise.

L42def ValuePosition.commitment {W : Type} (v : ValuePosition W) : Claim W :=

Define ValuePosition.commitment. The commitment claim says the world selects this position's adopted option; it is no longer a freely relabeled separate claim field.

L43  fun w => v.selected w = v.adopted

Derive the commitment claim by equating actual selection with this very adopted option.

L44/- Assessed consequences concern this adopted option's actual outcome, objective and constraints. -/

Document the intended scope of ValuePosition.consequence. The corresponding declaration concerns: Checks this adopted option's modeled outcome against its objective and constraints. This comment is explanatory, not a proof premise.

L45def ValuePosition.consequence {W : Type} (v : ValuePosition W) : Claim W :=

Define ValuePosition.consequence. Checks this adopted option's modeled outcome against its objective and constraints.

L46  fun w => v.objective (v.outcome w v.adopted) ∧ v.constraints w v.adopted

Derive the assessed consequence from this adopted option’s actual outcome satisfying the objective and its actual constraints.

L47/- Articulated reasons specialize the actual option-indexed premises to the adopted option. -/

Document the intended scope of ValuePosition.activeReasons. The corresponding declaration concerns: Specializes every option-indexed reason to the adopted option for articulation. This comment is explanatory, not a proof premise.

L48def ValuePosition.activeReasons {W : Type} (v : ValuePosition W) : List (Claim W) :=

Define ValuePosition.activeReasons. Specializes every option-indexed reason to the adopted option for articulation.

L49  v.reasons.map (fun reason w => reason w v.adopted)

Specialize each option-indexed reason to the adopted option to produce its actual articulated world predicate.

L50/- A joint witness excludes inconsistent starts and impossible adoption states. -/

Document the intended scope of JointAdoption. The corresponding declaration concerns: Requires one world jointly modeling the starting theory, scope, actual adoption and all adopted-option reasons. This comment is explanatory, not a proof premise.

L51def JointAdoption {W : Type} (v : ValuePosition W) : Prop :=

Define JointAdoption. Requires one world jointly modeling the starting theory, scope, actual adoption and all adopted-option reasons.

L52  ∃ w, Models v.starting w ∧ v.limits w ∧ v.commitment w ∧

Require one common world for starting assumptions, application limits and actual adoption.

L53    ∀ reason, reason ∈ v.reasons → reason w v.adopted

At that same witness, require every listed reason for that adopted option to hold together.

L54/- This declared option/outcome adapter checks joint reasons for an assessed consequence; it is not a necessary deductive form for all value justification. -/

Document the intended scope of ValueProcedure. The corresponding declaration concerns: Requires nonempty reasons, a joint adoption witness, joint reasons supporting the option's consequence within starting assumptions/scope, and nonempty criticism responses. It does not prove ultimate value correctness. This comment is explanatory, not a proof premise.

L55def ValueProcedure {W : Type} (v : ValuePosition W) : Prop :=

Define ValueProcedure. Requires nonempty reasons, a joint adoption witness, joint reasons supporting the option's consequence within starting assumptions/scope, and nonempty criticism responses. It does not prove ultimate value correctness.

L56  v.reasons ≠ [] ∧ JointAdoption v ∧

Begin ValueProcedure with nonempty reasons and the complete joint adoption witness.

L57  (∀ w, Models v.starting w → v.limits w →

For every world satisfying the actual starting theory and limits, impose the following conditional consequence requirement.

L58    (∀ reason, reason ∈ v.reasons → reason w v.adopted) → v.consequence w) ∧

Use the conjunction of all reasons for the adopted option to imply its actual consequence; no individual-reason sufficiency requirement is imposed.

L59  (∀ w, v.limits w → v.relevantCriticism w → ∃ answer, v.response w = some answer ∧ answer ≠ "")

Within limits, every relevant criticism must receive a specified nonempty response; this checks recorded response, not persuasiveness.

L60/- A facet carries its specific contents; several different facets can have the same conclusion. -/

Document the intended scope of Facet. The corresponding declaration concerns: Defines three distinct facet kinds with different discharge conditions. This comment is explanatory, not a proof premise.

L61inductive Facet (W : Type) where

Declare the alternatives Facet. Defines three distinct facet kinds with different discharge conditions.

L62  | empirical (records : List (Record W)) (scope conclusion uncertainty : Claim W)

An empirical facet stores actual test records together with its scope, conclusion and stated uncertainty predicate.

L63  | inferential (assumptions : Theory W) (conclusion : Claim W)

An inferential facet stores its actual premise theory and the conclusion to be entailed from it.

L64  | value (position : ValuePosition W)

A value facet stores the entire option/outcome position, including its starting theory, reasons, limits and criticism response.

L65/- The claim referred to by each assessment facet is explicit. -/

Document the intended scope of Facet.claim. The corresponding declaration concerns: Extracts the target claim of a facet, using the commitment rather than consequence for a value facet. This comment is explanatory, not a proof premise.

L66def Facet.claim {W : Type} : Facet W → Claim W

Define Facet.claim. Extracts the target claim of a facet, using the commitment rather than consequence for a value facet.

L67  | .empirical _ _ p _ => p

Read the empirical facet’s own conclusion p as its claim; records, scope and uncertainty remain assessment inputs.

L68  | .inferential _ p => p

Read the inferential facet’s own conclusion p as its claim, separately from its premise theory.

L69  | .value v => v.commitment

The value facet’s claim is actual selection equaling its own adopted option, derived through v.commitment.

L70/- These disclosed semantic adapters implement selected nature-specific checks; passing them does not establish all real empirical or value adequacy. -/

Document the intended scope of FacetDischarged. The corresponding declaration concerns: Dispatches to a different check for each facet kind; these checks have different truth guarantees. This comment is explanatory, not a proof premise.

L71def FacetDischarged {W : Type} : Facet W → Prop

Define FacetDischarged. Dispatches to a different check for each facet kind; these checks have different truth guarantees.

L72  | .empirical records scope p uncertainty =>

Enter the empirical discharge case with this facet’s actual records, scope, conclusion p and uncertainty predicate.

L73      (∃ w, Compatible records w ∧ scope w) ∧

For an empirical facet, require a world compatible with its records and inside its scope, excluding an empty empirical domain.

L74      Supports records (fun w => scope w → p w) ∧ Supports records uncertainty

Require the records to support the scoped conclusion and the explicitly stated uncertainty predicate.

L75  | .inferential assumptions p => Satisfiable assumptions ∧ Entails assumptions p

Inferential discharge requires a nonempty model of the actual assumptions and semantic entailment of p from those same assumptions.

L76  | .value v => ValueProcedure v

Value discharge is exactly the declared ValueProcedure for that same position, not a proof of ultimate value adequacy.

L77/- This model's semantic adapter identifies the actual assumptions, reason content and limit of a facet. -/

Document the intended scope of FacetArticulated. The corresponding declaration concerns: Requires articulation fields to match the facet's own assumptions, reasons and limits; concept strings are not constrained here. This comment is explanatory, not a proof premise.

L78def FacetArticulated {W : Type} (a : Articulation W) : Facet W → Prop

Define FacetArticulated. Requires articulation fields to match the facet's own assumptions, reasons and limits; concept strings are not constrained here.

L79  | .empirical records scope _ _ =>

In the empirical articulation case, read the actual records and scope whose assumptions/reasons/limits must match.

L80      a.assumptions = singleton (Compatible records) ∧ a.reasons = [Compatible records] ∧ a.limits = scope

This empirical adapter equates articulated assumptions and reasons with actual record compatibility, and articulated limits with the empirical scope.

L81  | .inferential assumptions _ =>

In the inferential case, use this facet’s actual assumption theory as the articulation’s reference.

L82      a.assumptions = assumptions ∧ a.reasons = [Models assumptions] ∧ a.limits = (fun _ => True)

This inferential adapter retains the exact premise theory, articulates its model condition as the reason, and uses unrestricted additional limits.

L83  | .value v => a.assumptions = v.starting ∧ a.reasons = v.activeReasons ∧ a.limits = v.limits

Require value articulation to use exactly this position’s starting theory, adopted-option active reasons and limits.

L84/- A canonical articulation exposes this adapter; the source does not mandate this particular representation of grounds. -/

Document the intended scope of canonicalArticulation. The corresponding declaration concerns: Constructs field-aligned articulations by pattern matching; the fixed concept strings are descriptive labels. This comment is explanatory, not a proof premise.

L85def canonicalArticulation {W : Type} : Facet W → Articulation W

Define canonicalArticulation. Constructs field-aligned articulations by pattern matching; the fixed concept strings are descriptive labels.

L86  | .empirical records scope _ _ =>

Construct the empirical canonical articulation from the actual record list and scope of the selected facet.

L87      ⟨["recorded test outcomes", "observation conditions"], singleton (Compatible records), [Compatible records], scope⟩

Construct empirical articulation naming test outcomes and conditions, using the actual compatibility claim as its premise/reason and the original scope as its limit.

L88  | .inferential assumptions _ =>

Construct inferential canonical articulation from this facet’s actual premise theory.

L89      ⟨["stated assumptions", "semantic consequence"], assumptions, [Models assumptions], fun _ => True⟩

Construct inferential articulation from the same theory and its actual model predicate, with no extra limit.

L90  | .value v =>

Construct the value articulation using the same complete position v.

L91      ⟨["adopted position", "reasons and consequences"], v.starting, v.activeReasons, v.limits⟩

Construct value articulation from the actual starting theory, adopted-option reasons and original limits.

L92/- Canonical articulation is connected to the very facet whose grounds it identifies. -/

Document the intended scope of canonicalFacetArticulated. The corresponding declaration concerns: Proves all canonical articulations have the required field alignment; no discharge hypothesis is needed for equality by construction. This comment is explanatory, not a proof premise.

L93theorem canonicalFacetArticulated {W : Type} (f : Facet W) :

State the checked result canonicalFacetArticulated. Proves all canonical articulations have the required field alignment; no discharge hypothesis is needed for equality by construction.

L94    FacetArticulated (canonicalArticulation f) f := by

Assert that canonical articulation is semantically connected to this very facet; the proof checks each facet constructor.

L95  cases f <;> exact ⟨rfl, rfl, rfl⟩

Split the three facet constructors; each canonical articulation has exactly the assumptions, reasons and limits required by its matching branch, so all three equalities are reflexive.

L96/- A discharged facet has nonempty canonical reason articulation, including the value procedure's reason requirement. -/

Document the intended scope of canonicalArticulated. The corresponding declaration concerns: Given a discharged facet, proves its canonical concept/reason lists are nonempty. The value case uses the discharge premise's reason nonemptiness. This comment is explanatory, not a proof premise.

L97theorem canonicalArticulated {W : Type} (f : Facet W) (h : FacetDischarged f) :

State the checked result canonicalArticulated. Given a discharged facet, proves its canonical concept/reason lists are nonempty. The value case uses the discharge premise's reason nonemptiness.

L98    Articulated (canonicalArticulation f) := by

Given this facet’s discharge, require its canonical concepts and reasons to be nonempty.

L99  cases f with

Check canonical articulation separately for empirical, inferential and value facets.

L100  | empirical records scope p uncertainty => simp [Articulated, canonicalArticulation]

In this empirical or inferential branch, the canonical concept and reason lists are explicitly nonempty; simplification verifies both articulation requirements.

L101  | inferential assumptions p => simp [Articulated, canonicalArticulation]

In this empirical or inferential branch, the canonical concept and reason lists are explicitly nonempty; simplification verifies both articulation requirements.

L102  | value v =>

For the value branch, the premise h is ValueProcedure v; its nonempty reasons must establish nonempty canonical active reasons.

L103      refine ⟨by simp [canonicalArticulation], ?_⟩

For a value facet, supply nonempty canonical concepts and leave the nonempty active-reason obligation.

L104      simpa [canonicalArticulation, ValuePosition.activeReasons] using h.1

Use the discharged value procedure’s nonempty reasons; specializing them to the adopted option preserves nonemptiness.

L105/- This model of the Grounds obligation binds each actual facet to its claim and articulation. Its disclosed FacetDischarged adapters do not replace all source-level assessment responsibilities or prove real adequacy. -/

Document the intended scope of Grounds. The corresponding declaration concerns: Grounds packages a nonempty facet list, coverage of a supplied applicability predicate, common claim identity, articulation presence/alignment, and every listed facet's discharge. It is not uniformly a truth certificate for the claim. This comment is explanatory, not a proof premise.

L106def Grounds {W : Type} (claim : Claim W) (articulations : Facet W → Articulation W)

Define Grounds. Grounds packages a nonempty facet list, coverage of a supplied applicability predicate, common claim identity, articulation presence/alignment, and every listed facet's discharge. It is not uniformly a truth certificate for the claim.

L107    (actualApplicable : Facet W → Prop) (facets : List (Facet W)) : Prop :=

Take actualApplicable independently of the finite list, so coverage is an explicit obligation rather than inferred from list membership.

L108  facets ≠ [] ∧ (∀ facet, actualApplicable facet → facet ∈ facets) ∧

Require a nonempty facet list and inclusion of every facet satisfying actualApplicable.

L109  ∀ facet, facet ∈ facets → facet.claim = claim ∧ Articulated (articulations facet) ∧

For every listed facet, require the exact claim and a nonempty articulation belonging to that facet.

L110    FacetArticulated (articulations facet) facet ∧ FacetDischarged facet

Also require semantic matching to its actual premises/reasons/limits and discharge by its declared adapter.

L111/- The achievement obligation requires grounds for this very claim, without making observation a universal prerequisite. -/

Document the intended scope of AchievementAccountability. The corresponding declaration concerns: Defines achievement accountability as exactly the same Grounds predicate, with no additional execution or achievement proof. This comment is explanatory, not a proof premise.

L112def AchievementAccountability {W : Type} (achievement : Claim W) (articulations : Facet W → Articulation W)

Define AchievementAccountability. Defines achievement accountability as exactly the same Grounds predicate, with no additional execution or achievement proof.

L113    (actualApplicable : Facet W → Prop) (facets : List (Facet W)) : Prop :=

Achievement accountability accepts the same actual-applicability predicate and facet list as Grounds.

L114  Grounds achievement articulations actualApplicable facets

Define accountability directly by Grounds for the very achievement claim; no extra universal observation requirement is added.

L115/- The concrete achievement claim refers to each transition's own before/after states. -/

Document the intended scope of transitionAchievement. The corresponding declaration concerns: Defines achievement as understanding/construction expansion between the same modeled transition's before and after states. This comment is explanatory, not a proof premise.

L116def transitionAchievement : Claim TransitionCase :=

Define transitionAchievement. Defines achievement as understanding/construction expansion between the same modeled transition's before and after states.

L117  fun transition => Expanded (transitionBefore transition) (transitionAfter transition)

The achievement claim is actual expansion between the selected transition’s own before and after states.

L118/- This observation inspects an actually constructed successor and its output under that transition's input condition. -/

Document the intended scope of transitionPerformanceRecord. The corresponding declaration concerns: Tests whether that after-state contains successor actually returning one at the transition input, within the two-transition model. This comment is explanatory, not a proof premise.

L119def transitionPerformanceRecord : Record TransitionCase :=

Define transitionPerformanceRecord. Tests whether that after-state contains successor actually returning one at the transition input, within the two-transition model.

L120  ⟨fun transition => (transitionAfter transition).constructed.any

The performance test inspects operations actually constructed in this transition’s after-state.

L121    (fun operation => operation == .successor && decide (operation.run (transitionInput transition) = 1)), true⟩

It records true only when successor is present and actually sends the shared transition input to 1.

L122/- The positive report test reads its asserted operation, input and output; it does not verify their presence in the after-state. -/

Document the intended scope of transitionReportRecord. The corresponding declaration concerns: Records only the report's announced operation/input/output, not its actual achievement. This comment is explanatory, not a proof premise.

L123def transitionReportRecord : Record TransitionCase :=

Define transitionReportRecord. Records only the report's announced operation/input/output, not its actual achievement.

L124  ⟨fun transition =>

Begin a record whose test reads the actual transition’s announcement.

L125    let report := transitionAnnouncement transition

Bind report to the announcement generated for this same transition.

L126    report.reportedNewOperation == .successor && report.input == 0 && report.expectedOutput == 1, true⟩

Test its stated successor, input 0 and expected output 1, recording a positive announcement independently of whether the operation exists.

L127/- Only the genuine extension matches the operation/performance observation in this two-transition model. -/

Document the intended scope of transitionPerformanceCompatible. The corresponding declaration concerns: Exhausts inflate/extend to show the actual performance record identifies extension. This comment is explanatory, not a proof premise.

L128theorem transitionPerformanceCompatible :

State the checked result transitionPerformanceCompatible. Exhausts inflate/extend to show the actual performance record identifies extension.

L129    ∀ transition, Compatible [transitionPerformanceRecord] transition ↔ transition = .extend := by

Claim that matching the actual positive performance record is equivalent to selecting extend.

L130  intro transition

Fix an arbitrary actual transition, either inflate or extend, for the record-compatibility equivalence.

L131  constructor

Prove both directions: performance compatibility implies extend, and extend supplies compatibility.

L132  · intro h

Assume this transition matches the actual positive performance record.

L133    have observed := h transitionPerformanceRecord (List.mem_singleton.mpr rfl)

Apply compatibility to the actual singleton performance record to obtain its observed test result for this transition.

L134    cases transition

Split the actual transition into inflate and extend, whose after-states have different operation content.

L135    · cases observed

The inflate state lacks successor, so its performance test cannot equal the recorded true outcome.

L136    · rfl

The extend case has the required transition identity by reflexivity.

L137  · intro h; cases h

For the reverse implication, substitute the assumption that the transition is extend.

L138    intro record hr; have hr' := List.mem_singleton.mp hr; subst record

Membership in the singleton record list identifies the arbitrary record with this exact transition record; substitute it before checking its test.

L139    rfl

Evaluate the actual extend performance record; its successor-at-zero test equals the recorded true outcome.

L140/- A compatible performance observation establishes the same transition's report content and hence its represented expansion. -/

Document the intended scope of transitionSupported. The corresponding declaration concerns: Uses performance identification, the concrete new operation and report claim to establish transition expansion in every compatible case. This comment is explanatory, not a proof premise.

L141theorem transitionSupported : Supports [transitionPerformanceRecord] transitionAchievement := by

State the checked result transitionSupported. Uses performance identification, the concrete new operation and report claim to establish transition expansion in every compatible case. The following tactic block proves this explicit type.

L142  intro transition compatible

Take an arbitrary transition and its compatibility with the actual performance record; prove expansion for that same transition.

L143  have h := (transitionPerformanceCompatible transition).1 compatible

Use transitionPerformanceCompatible to identify every performance-compatible transition as extend.

L144  subst transition

Substitute extend for the transition, so the remaining achievement claim concerns its real extended after-state.

L145  have reportTrue : (transitionAnnouncement .extend).claim := by

Check the same system-generated extend report against its actual before/after states: successor is newly constructed and sends input 0 to output 1.

L146    simp [transitionAnnouncement, transitionAfter, transitionInput,

Check the same system-generated extend report against its actual before/after states: successor is newly constructed and sends input 0 to output 1.

L147      Announcement.claim, GeneratingSystem.report, generatingSystem, extendedState, baseState, Operation.run]

Check the same system-generated extend report against its actual before/after states: successor is newly constructed and sends input 0 to output 1.

L148  exact announcementClaimImpliesExpansion _ reportTrue

Apply announcementClaimImpliesExpansion to the verified report content to obtain the same transition’s Expanded claim.

L149/- The actual scope is the shared input-zero condition, with no probabilistic inference introduced. -/

Document the intended scope of transitionFacet. The corresponding declaration concerns: Packages the performance record, input-zero scope and exact expansion claim as an empirical facet. This comment is explanatory, not a proof premise.

L150def transitionFacet : Facet TransitionCase :=

Define transitionFacet. Packages the performance record, input-zero scope and exact expansion claim as an empirical facet.

L151  .empirical [transitionPerformanceRecord] (fun transition => transitionInput transition = 0)

Build an empirical facet from the performance record with the exact input-0 transition scope.

L152    transitionAchievement (fun _ => True)

Its conclusion is the same transition’s achievement; its uncertainty predicate is explicitly True.

L153/- The empirical assessment has a real compatible witness and supports this scoped achievement. -/

Document the intended scope of transitionFacetDischarged. The corresponding declaration concerns: Supplies extension as a nonempty witness, actual support and trivial uncertainty. This comment is explanatory, not a proof premise.

L154theorem transitionFacetDischarged : FacetDischarged transitionFacet := by

State the checked result transitionFacetDischarged. Supplies extension as a nonempty witness, actual support and trivial uncertainty. The following tactic block proves this explicit type.

L155  refine ⟨⟨.extend, (transitionPerformanceCompatible _).2 rfl, rfl⟩, ?_, ?_⟩

Provide extend as the nonempty empirical witness with compatible performance evidence and the shared input-0 scope; leave scoped support and uncertainty checks.

L156  · intro transition compatible _; exact transitionSupported transition compatible

The already proved transition support supplies the achievement at any compatible transition, hence within the chosen scope.

L157  · intro _ _; trivial

The explicitly unrestricted uncertainty predicate is True, so this adapter component is immediate; no quantitative uncertainty bound is inferred.

L158/- Every applicable facet of this specified achievement has matching articulation and actual discharged evidence. -/

Document the intended scope of transitionAccountable. The corresponding declaration concerns: Builds achievement Grounds with matching claim, scope, canonical articulation and discharged facet. This comment is explanatory, not a proof premise.

L159theorem transitionAccountable :

State the checked result transitionAccountable. Builds achievement Grounds with matching claim, scope, canonical articulation and discharged facet.

L160    AchievementAccountability transitionAchievement canonicalArticulation

State accountability for the actual transition-achievement predicate with canonical articulation.

L161      (fun facet => facet = transitionFacet) [transitionFacet] := by

Declare transitionFacet the only applicable facet and use precisely that singleton evidence package.

L162  refine ⟨by simp, ?_, ?_⟩

Split accountability into nonempty facets, coverage of actual applicability, and matching articulated discharge for each included facet.

L163  · intro facet hf; subst facet; exact List.mem_singleton.mpr rfl

The applicability assumption identifies the facet with the one prescribed facet, which belongs to the singleton list.

L164  · intro facet hf; have hf' := List.mem_singleton.mp hf; subst facet

Singleton membership identifies the current facet with the prescribed one; substitute it to check its exact claim and grounds.

L165    exact ⟨rfl, canonicalArticulated _ transitionFacetDischarged,

Assemble identical claim, nonempty canonical articulation, its semantic connection to this facet, and transitionFacetDischarged.

L166      canonicalFacetArticulated _, transitionFacetDischarged⟩

Assemble identical claim, nonempty canonical articulation, its semantic connection to this facet, and transitionFacetDischarged.

L167/- Both actual transitions issue the same positive report about their own identified state pair. -/

Document the intended scope of transitionReportCompatible. The corresponding declaration concerns: Shows both transition cases produce the same announced operation/input/output record. This comment is explanatory, not a proof premise.

L168theorem transitionReportCompatible (transition : TransitionCase) :

State the checked result transitionReportCompatible. Shows both transition cases produce the same announced operation/input/output record.

L169    Compatible [transitionReportRecord] transition := by

State that this transition’s positive report record is compatible with the transition itself, including inflate.

L170  intro record hr; have hr' := List.mem_singleton.mp hr; subst record

Membership in the singleton record list identifies the arbitrary record with this exact transition record; substitute it before checking its test.

L171  rfl

The report test only checks the actual positive announcement contents, which evaluate identically for either transition.

L172/- Inflation is a concrete report-compatible counterworld, so the positive report alone does not support the same achievement claim. -/

Document the intended scope of transitionReportDoesNotSupport. The corresponding declaration concerns: Uses the inflated transition as a report-compatible non-achievement countermodel. This comment is explanatory, not a proof premise.

L173theorem transitionReportDoesNotSupport :

State the checked result transitionReportDoesNotSupport. Uses the inflated transition as a report-compatible non-achievement countermodel.

L174    Compatible [transitionReportRecord] .inflate ∧ ¬ transitionAchievement .inflate ∧

Require inflate to match the report while failing the same achievement predicate.

L175    ¬ Supports [transitionReportRecord] transitionAchievement := by

Conclude that the positive report records therefore do not support the achievement over all compatible transitions.

L176  have noExpansion : ¬ transitionAchievement .inflate := by

Unfold the inflate transition: both understood and constructed operation sets are unchanged, so no new-operation witness for Expanded exists.

L177    simp [transitionAchievement, transitionBefore, transitionAfter, Expanded, baseState, inflatedState]

Unfold the inflate transition: both understood and constructed operation sets are unchanged, so no new-operation witness for Expanded exists.

L178  exact ⟨transitionReportCompatible _, noExpansion, fun h => noExpansion (h _ (transitionReportCompatible _))⟩

Combine positive-report compatibility with the false expansion claim at inflate; any claimed support applied there gives a contradiction.

L179/- These concrete obligations, positive evidence and negative report case all refer to the same state-pair and input semantics. -/

Document the intended scope of ConcreteAchievementExample. The corresponding declaration concerns: Combines same-object achievement accountability and supported extension with an unsupported inflation report, preserving before/after/input identities. This comment is explanatory, not a proof premise.

L180def ConcreteAchievementExample : Prop :=

Define ConcreteAchievementExample. Combines same-object achievement accountability and supported extension with an unsupported inflation report, preserving before/after/input identities.

L181  AchievementAccountability transitionAchievement canonicalArticulation

The concrete example includes actual accountability for the transition achievement.

L182    (fun facet => facet = transitionFacet) [transitionFacet] ∧

Its actual-applicability predicate and list identify the same single transition facet.

L183  Compatible [transitionPerformanceRecord] .extend ∧

Require extend to satisfy the actual performance observation.

L184  Supports [transitionPerformanceRecord] transitionAchievement ∧ transitionAchievement .extend ∧

Require semantic support for the achievement and its truth at extend.

L185  (Compatible [transitionReportRecord] .inflate ∧ ¬ transitionAchievement .inflate ∧

Also retain the report-compatible inflate world in which this achievement is false.

L186    ¬ Supports [transitionReportRecord] transitionAchievement) ∧

State the resulting failure of support from reports alone.

L187  (∀ transition, (transitionAnnouncement transition).before = transitionBefore transition ∧

For every transition, bind the report’s before state to the actual transition-before state.

L188    (transitionAnnouncement transition).after = transitionAfter transition ∧

Bind its after state to that same transition’s actual after state.

L189    (transitionAnnouncement transition).input = transitionInput transition ∧ transitionInput transition = 0)

Bind the report input to the actual transition input and explicitly fix that condition to 0.

L190/- The concrete example jointly inhabits accountability, evidence compatibility, actual gain, and the report-only countermodel. -/

Document the intended scope of concreteAchievementExample. The corresponding declaration concerns: Assembles the concrete performance support, reporting countermodel and exact state/input links. This comment is explanatory, not a proof premise.

L191theorem concreteAchievementExample : ConcreteAchievementExample := by

State the checked result concreteAchievementExample. Assembles the concrete performance support, reporting countermodel and exact state/input links. The following tactic block proves this explicit type.

L192  refine ⟨transitionAccountable, (transitionPerformanceCompatible _).2 rfl, transitionSupported,

Assemble the actual achievement’s accountability, extend performance compatibility and semantic support in the concrete example.

L193    transitionSupported .extend ((transitionPerformanceCompatible _).2 rfl),

Apply that same support to the extend witness to establish actual expansion there.

L194    transitionReportDoesNotSupport, ?_⟩

Include the report-compatible inflate counterexample and leave the same-before/after/input relationships.

L195  intro transition; exact ⟨rfl,rfl,rfl,rfl⟩

For either transition, all report-to-state and input-0 links hold by the definitions themselves.

L196/- Semantic evidence yields truth only at a world that actually satisfies those evidence conditions. -/

Document the intended scope of achievementNeedsSupport. The corresponding declaration concerns: Applies supplied compatible-world support to the arbitrary actual claim and separately includes the checked concrete transition example. This comment is explanatory, not a proof premise.

L197theorem achievementNeedsSupport {W : Type} (achievement : Claim W) (records : List (Record W))

State the checked result achievementNeedsSupport. Applies supplied compatible-world support to the arbitrary actual claim and separately includes the checked concrete transition example.

L198    (actual : W) (reliableHere : Compatible records actual) (support : Supports records achievement) :

Assume the chosen actual world matches all records and those records already support the achievement.

L199    achievement actual ∧ ConcreteAchievementExample :=

Conclude truth of the achievement at that actual world, together with the separately constructed concrete achievement example.

L200  ⟨support actual reliableHere, concreteAchievementExample⟩

Apply the assumed support to the actual evidence-compatible world, and pair that local truth with the separately proved concrete achievement example.

L201/- Weakening a conclusion preserves support; this makes no claim about weakening the evidence. -/

Document the intended scope of supportWeakening. The corresponding declaration concerns: Preserves support when a supported claim implies a weaker claim at every world; it does not weaken the record set. This comment is explanatory, not a proof premise.

L202theorem supportWeakening {W : Type} (records : List (Record W)) (p q : Claim W)

State the checked result supportWeakening. Preserves support when a supported claim implies a weaker claim at every world; it does not weaken the record set.

L203    (support : Supports records p) (weaker : ∀ w, p w → q w) : Supports records q :=

Assume support for p and a world-by-world implication from p to q; conclude support for q using the same records.

L204  fun w hw => weaker w (support w hw)

At each compatible world w, first derive p using the unchanged records, then apply the supplied implication weaker to obtain q.

L205/- Discarding the only informative observation loses support for the unchanged switch claim. -/

Document the intended scope of evidenceWeakeningCanLoseSupport. The corresponding declaration concerns: Provides a true Boolean observation supporting equality to true and shows deleting that record loses this support. This comment is explanatory, not a proof premise.

L206theorem evidenceWeakeningCanLoseSupport :

State the checked result evidenceWeakeningCanLoseSupport. Provides a true Boolean observation supporting equality to true and shows deleting that record loses this support.

L207    Supports ([⟨id, true⟩] : List (Record Bool)) (fun w => w = true) ∧

The single identity observation supports that the Boolean world is true.

L208    ¬ Supports ([] : List (Record Bool)) (fun w => w = true) := by

Deleting that observation leaves empty records, which do not support the unchanged claim.

L209  refine ⟨?_, ?_⟩

Split the supported one-record claim from the failure of the same claim after deleting that record.

L210  · intro w hw; exact hw ⟨id,true⟩ (by simp)

Read the informative identity test from compatibility; it directly states that the Boolean world is true.

L211  · intro h; have bad := h false (by intro r hr; cases hr); cases bad

With no records, false is compatible; evaluating purported support there refutes the unchanged true-world claim.

L212/- Restricting the quantified application domain preserves a supported universal conclusion. -/

Document the intended scope of scopeRestriction. The corresponding declaration concerns: Restricts a universally supported property from a wider input domain to an included narrower domain, for arbitrary world and input types. This comment is explanatory, not a proof premise.

L213theorem scopeRestriction {W X : Type} (records : List (Record W)) (p : W → X → Prop)

State the checked result scopeRestriction. Restricts a universally supported property from a wider input domain to an included narrower domain, for arbitrary world and input types.

L214    (wide narrow : X → Prop) (included : ∀ x, narrow x → wide x)

Take broad and narrow application domains and assume every narrow-domain input is in the broad domain.

L215    (support : Supports records (fun w => ∀ x, wide x → p w x)) :

Assume the same records support p at every input in the broad domain.

L216    Supports records (fun w => ∀ x, narrow x → p w x) :=

Conclude support at every input in the narrower domain; neither the evidence nor predicate p changes.

L217  fun w hw x hx => support w hw x (included x hx)

For a compatible world and narrow-domain input x, included converts narrow membership to broad membership; apply the original broad support there.

L218/- Actual applicability, rather than an optional classifier label, determines facet responsibility. -/

Document the intended scope of Duties. The corresponding declaration concerns: Requires every facet satisfying the supplied applicability predicate to be discharged. This comment is explanatory, not a proof premise.

L219def Duties {W : Type} (applicable : Facet W → Prop) : Prop :=

Define Duties. Requires every facet satisfying the supplied applicability predicate to be discharged.

L220  ∀ f, applicable f → FacetDischarged f

Require every actually applicable facet to pass its own discharge condition.

L221def LabeledDuties {W : Type} (_labels : List String) (applicable : Facet W → Prop) : Prop :=

Define LabeledDuties. Defines labeled duties by ignoring all labels and keeping only the applicability-based duties.

L222  Duties applicable

Define labeled duties by exactly the original applicability duties; the labels supply no waiver.

L223/- Combining applicable facets requires both sets of substantive duties. -/

Document the intended scope of assessmentUnion. The corresponding declaration concerns: Proves that discharging the union of two applicability predicates is equivalent to discharging each separately. This comment is explanatory, not a proof premise.

L224theorem assessmentUnion {W : Type} (a b : Facet W → Prop) :

State the checked result assessmentUnion. Proves that discharging the union of two applicability predicates is equivalent to discharging each separately.

L225    Duties (fun f => a f ∨ b f) ↔ Duties a ∧ Duties b := by

Equate duties for the union of two applicability predicates with fulfillment of both sets of duties.

L226  constructor

Prove both directions between duty on the union applicability predicate and simultaneous duties on its two components.

L227  · intro h; exact ⟨fun f hf => h f (Or.inl hf), fun f hf => h f (Or.inr hf)⟩

Restrict the union duty to each applicable-facet predicate using the matching disjunction injection.

L228  · rintro ⟨ha,hb⟩ f (hf|hf); exact ha f hf; exact hb f hf

Unpack both duty sets, split actual applicability into its left/right case, and discharge that very facet using the corresponding duty.

L229/- Omitting or changing labels does not remove an applicable duty. -/

Document the intended scope of labelsCannotWaive. The corresponding declaration concerns: Proves changing labels cannot change duties because labels were ignored by definition; no external classification mechanism is analyzed. This comment is explanatory, not a proof premise.

L230theorem labelsCannotWaive {W : Type} (xs ys : List String) (a : Facet W → Prop) :

State the checked result labelsCannotWaive. Proves changing labels cannot change duties because labels were ignored by definition; no external classification mechanism is analyzed.

L231    LabeledDuties xs a ↔ LabeledDuties ys a := Iff.rfl

Changing only the label lists leaves the same duty proposition; the equivalence is reflexive.

L232/- The observed switch is the outcome itself, not a record identifier. -/

Document the intended scope of switchRecord. The corresponding declaration concerns: Records the identity Boolean test with observed value true. This comment is explanatory, not a proof premise.

L233def switchRecord : Record Bool := ⟨id, true⟩

Define switchRecord. Records the identity Boolean test with observed value true.

L234theorem switchCompatible (w : Bool) : Compatible [switchRecord] w ↔ w = true := by

State the checked result switchCompatible. Proves compatibility with the single switch record is exactly equality of the world with true. The following tactic block proves this explicit type.

L235  constructor

Prove that compatibility with the singleton switch record is equivalent to the actual Boolean world being true.

L236  · intro h; exact h switchRecord (by simp)

Apply record compatibility to the sole named test to recover its actual observed equality.

L237  · intro hw r hr; simp only [List.mem_singleton] at hr; cases hr; exact hw

Conversely, singleton membership identifies any listed record with this test, whose equality is the supplied observation premise.

L238theorem switchSupported : Supports [switchRecord] (fun w : Bool => w = true) :=

State the checked result switchSupported. Supports equality to true by extracting the previously proved compatibility equivalence. The supplied proof term uses the displayed constructed witnesses or earlier lemmas, rather than adding an axiom.

L239  fun w hw => (switchCompatible w).1 hw

Use switchCompatible’s forward implication to extract world=true from the same world’s actual record compatibility.

L240/- The candidate action has specific benefit and cost outcomes; its inactive alternative has neither. -/

Document the intended scope of optionBenefit. The corresponding declaration concerns: Assigns benefit 4 to selected=true and 0 otherwise. This comment is explanatory, not a proof premise.

L241def optionBenefit (selected : Bool) : Nat := if selected then 4 else 0

Define optionBenefit. Assigns benefit 4 to selected=true and 0 otherwise.

L242def optionCost (selected : Bool) : Nat := if selected then 3 else 0

Define optionCost. Assigns cost 3 to selected=true and 0 otherwise.

L243/- The report describes each option's actual cost and benefit; it does not itself assert which option ought to be selected. -/

Document the intended scope of optionReport. The corresponding declaration concerns: States option-specific cost and benefit facts rather than an unconnected reason flag. This comment is explanatory, not a proof premise.

L244def optionReport (selected : Bool) : Prop :=

Define optionReport. States option-specific cost and benefit facts rather than an unconnected reason flag.

L245  optionCost selected ≤ 3 ∧ optionBenefit selected = (if selected then 4 else 0)

The option report asserts actual cost at most 3 and the option-specific benefit of 4 for on or 0 for off.

L246/- The on position connects its own selected option to that option's benefit/cost outcome. -/

Document the intended scope of switchPosition. The corresponding declaration concerns: Adopts true with actual option cost/benefit outcomes, cost-below-benefit objective, budget constraint and a scoped criticism response. This comment is explanatory, not a proof premise.

L247def switchPosition : ValuePosition Bool where

Define switchPosition. Adopts true with actual option cost/benefit outcomes, cost-below-benefit objective, budget constraint and a scoped criticism response.

L248  Position := Bool

Use Boolean options for on/off.

L249  Outcome := Nat × Nat

Represent each outcome as actual benefit and cost in a natural-number pair.

L250  adopted := true

Adopt the on option explicitly; adoption itself is not derived from arithmetic.

L251  selected := id

Read the actual selected option directly from the Boolean world.

L252  outcome := fun _ option => (optionBenefit option, optionCost option)

Compute benefit and cost from this same actual option.

L253  objective := fun result => result.2 < result.1

Adopt the objective that actual benefit strictly exceeds actual cost.

L254  constraints := fun _ option => optionCost option ≤ 3

Check the actual option cost against the fixed budget 3.

L255  starting := singleton (fun w => w = true)

Assume the actual Boolean selection is on; do not insert the assessed benefit conclusion into the starting theory.

L256  reasons := [fun _ option => optionReport option]

Use the option-indexed actual cost/benefit report as the sole reason.

L257  limits := fun _ => True

Use an unrestricted world scope in this example; starting assumptions and reason content still constrain the procedure.

L258  relevantCriticism := fun w => w = false

Mark the off-selected world as a relevant criticism case.

L259  response := fun w => if w then some "benefit exceeds cost within budget" else some "reconsider if the budget no longer permits this cost"

Provide distinct nonempty messages for the two worlds, including budget reconsideration in the criticism case.

L260theorem switchValueProcedure : ValueProcedure switchPosition := by

State the checked result switchValueProcedure. Provides a consistent adoption witness and derives the adopted option's objective/constraint from its actual cost-benefit reason; both Boolean responses are checked. The following tactic block proves this explicit type.

L261  refine ⟨by simp [switchPosition], ?_, ?_, ?_⟩

Separate nonempty reasons, a joint adoption witness, consequence support by all reasons, and response to criticism for switchPosition.

L262  · refine ⟨true, (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

Choose world true, satisfying the starting selection, unrestricted limit and adopted option, and leave its actual reason to check.

L263    intro reason hr

Take any reason in switchPosition’s list; the next step identifies its actual optionReport content at the adopted on witness.

L264    have hr' : reason = (fun (_ : Bool) (option : Bool) => optionReport option) := List.mem_singleton.mp hr

Singleton membership identifies the arbitrary reason with optionReport specialized to this position’s adopted option; substitute that actual reason.

L265    subst reason

Singleton membership identifies the arbitrary reason with optionReport specialized to this position’s adopted option; substitute that actual reason.

L266    exact ⟨by decide, rfl⟩

Check that the adopted on option meets its recorded cost bound and its stated benefit value.

L267  · intro w _ _ allReasons

For an arbitrary world in the stated starting/limit conditions, assume the entire active-reason conjunction.

L268    have evidence := allReasons (fun (_ : Bool) (option : Bool) => optionReport option) (List.mem_singleton.mpr rfl)

Extract the actual optionReport reason from that conjunction, rather than introducing an independent support label.

L269    change optionReport true at evidence

Unfold which option is adopted: this evidence concerns the on option.

L270    have benefitAboveBudget : 3 < optionBenefit true := by rw [evidence.2]; decide

Use the reported benefit equality to prove the on option’s benefit exceeds 3.

L271    exact ⟨Nat.lt_of_le_of_lt evidence.1 benefitAboveBudget, evidence.1⟩

Combine cost ≤ 3 with benefit > 3 to prove cost < benefit, and retain the same cost bound as the constraint.

L272  · intro w _ _; cases w <;> simp [switchPosition]

Check both Boolean worlds to provide the recorded nonempty criticism response where required.

L273/- Adopting the other option updates the adopted starting state too, so rejection cannot be blamed on an inconsistent start. -/

Document the intended scope of oppositePosition. The corresponding declaration concerns: Changes the adopted option to false and updates its starting selection while retaining the same outcome model and objective. This comment is explanatory, not a proof premise.

L274def oppositePosition : ValuePosition Bool :=

Define oppositePosition. Changes the adopted option to false and updates its starting selection while retaining the same outcome model and objective.

L275  { switchPosition with adopted := false, starting := singleton (fun w => w = false) }

Change both adopted option and starting selection to off while retaining the same actual outcome/reason interpretation.

L276/- The alternative has a joint adoption witness but its actual zero benefit/cost fails the adopted strict-benefit objective. -/

Document the intended scope of oppositePositionRejected. The corresponding declaration concerns: Shows false can be jointly adopted but fails the unchanged cost-below-benefit objective, so its value procedure is rejected. This comment is explanatory, not a proof premise.

L277theorem oppositePositionRejected : JointAdoption oppositePosition ∧ ¬ ValueProcedure oppositePosition := by

State the checked result oppositePositionRejected. Shows false can be jointly adopted but fails the unchanged cost-below-benefit objective, so its value procedure is rejected. The following tactic block proves this explicit type.

L278  have witness : JointAdoption oppositePosition := by

Construct an actual joint adoption witness for the opposite off position at world false; the rejection will therefore not rely on an empty domain.

L279    refine ⟨false, (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

Construct an actual joint adoption witness for the opposite off position at world false; the rejection will therefore not rely on an empty domain.

L280    intro reason hr

For the opposite position’s false-world witness, take any listed reason before checking that off option’s actual report.

L281    have hr' : reason = (fun (_ : Bool) (option : Bool) => optionReport option) := List.mem_singleton.mp hr

Singleton membership identifies the arbitrary reason with optionReport specialized to this position’s adopted option; substitute that actual reason.

L282    subst reason

Singleton membership identifies the arbitrary reason with optionReport specialized to this position’s adopted option; substitute that actual reason.

L283    exact ⟨by decide, rfl⟩

The off option’s own report is true: its zero cost is within the bound and its zero benefit matches the stated report.

L284  refine ⟨witness, ?_⟩

Retain the nonempty joint witness and separately refute fulfillment of the opposite value procedure.

L285  intro h

Assume the opposite off position satisfies its entire ValueProcedure, to derive a contradiction with its zero-benefit outcome.

L286  have allReasons : ∀ reason, reason ∈ oppositePosition.reasons → reason false oppositePosition.adopted := by

Assemble all of the opposite position’s reasons at its actual false-world witness before applying any consequence requirement.

L287    intro reason hr

Take any actual reason of the opposite position to assemble all reasons at its inhabited false-world counterexample.

L288    have hr' : reason = (fun (_ : Bool) (option : Bool) => optionReport option) := List.mem_singleton.mp hr

Singleton membership identifies the arbitrary reason with optionReport specialized to this position’s adopted option; substitute that actual reason.

L289    subst reason

Singleton membership identifies the arbitrary reason with optionReport specialized to this position’s adopted option; substitute that actual reason.

L290    exact ⟨by decide, rfl⟩

The off option’s own report is true: its zero cost is within the bound and its zero benefit matches the stated report.

L291  have bad := h.2.2.1 false ((modelsSingleton _ _).2 rfl) trivial allReasons

Apply the assumed opposite procedure’s joint-reason consequence clause to that same starting/limit witness and all its actual reasons.

L292  exact Nat.lt_irrefl 0 bad.1

Its purported objective would require the off option’s zero cost to be strictly less than its zero benefit, contradicting irreflexivity.

L293/- Contradictory starting assumptions and an impossible selected/adopted equality are separate inadmissible variants. -/

Document the intended scope of contradictoryStartingPosition. The corresponding declaration concerns: Replaces the starting theory with a false singleton, eliminating every joint adoption witness. This comment is explanatory, not a proof premise.

L294def contradictoryStartingPosition : ValuePosition Bool :=

Define contradictoryStartingPosition. Replaces the starting theory with a false singleton, eliminating every joint adoption witness.

L295  { switchPosition with starting := singleton (fun _ => False) }

Replace the starting theory with the impossible singleton claim False.

L296def impossibleAdoptionPosition : ValuePosition Bool :=

Define impossibleAdoptionPosition. Always selects false while retaining adoption of true, making joint adoption impossible.

L297  { switchPosition with selected := fun _ => false }

Keep the adopted on option but make every actual selection off, making joint adoption impossible.

L298/- The common-world witness rejects both contradiction and an impossible commitment instead of proving them vacuously. -/

Document the intended scope of inadmissibleValuePositionsRejected. The corresponding declaration concerns: Rejects both inconsistent starting theory and impossible adoption via the required witness. This comment is explanatory, not a proof premise.

L299theorem inadmissibleValuePositionsRejected :

State the checked result inadmissibleValuePositionsRejected. Rejects both inconsistent starting theory and impossible adoption via the required witness.

L300    ¬ ValueProcedure contradictoryStartingPosition ∧ ¬ ValueProcedure impossibleAdoptionPosition := by

Reject the procedures for contradictory starting assumptions and impossible actual adoption separately.

L301  constructor

Separate rejection of the contradictory starting theory from rejection of the impossible selected/adopted combination.

L302  · intro h; obtain ⟨w,hw,_,_,_⟩ := h.2.1

Extract a joint adoption witness from the alleged procedure for the contradictory starting position.

L303    exact (modelsSingleton _ _).1 hw

The singleton starting theory requires False at that witness, directly contradicting its model proof.

L304  · intro h; obtain ⟨w,_,_,hw,_⟩ := h.2.1

Extract the adoption equality from the alleged joint witness for the impossible selected/adopted combination.

L305    cases hw

The required adoption equality equates distinct Boolean options, so this witness cannot exist.

L306/- Removing the reasons leaves only a position and assertion, which fails this value procedure. -/

Document the intended scope of unsupportedPosition. The corresponding declaration concerns: Copies the switch value position but deletes its reasons, guaranteeing procedural failure. This comment is explanatory, not a proof premise.

L307def unsupportedPosition : ValuePosition Bool := { switchPosition with reasons := [] }

Define unsupportedPosition. Copies the switch value position but deletes its reasons, guaranteeing procedural failure.

L308def switchEmpirical : Facet Bool :=

Define switchEmpirical. Builds an empirical facet concluding the Boolean world is true from the switch record, with unrestricted scope and trivially true uncertainty.

L309  .empirical [switchRecord] (fun _ => True) (fun w => w = true) (fun _ => True)

Use the actual switch observation, unrestricted scope and same selected-on claim; uncertainty is explicitly True.

L310theorem switchEmpiricalDischarged : FacetDischarged switchEmpirical := by

State the checked result switchEmpiricalDischarged. Discharges that empirical facet with a true-world witness, semantic support, and trivial uncertainty. The following tactic block proves this explicit type.

L311  refine ⟨⟨true, (switchCompatible true).2 rfl, trivial⟩, ?_, ?_⟩

Use true as a nonempty world compatible with the switch record and unrestricted empirical scope.

L312  · intro w hw _; exact switchSupported w hw

The same switch record’s semantic support proves the scoped switch claim at each compatible world.

L313  · intro w _; trivial

Discharge the explicitly trivial uncertainty predicate, without adding an empirical confidence claim.

L314/- A mixed empirical/value position has actual empirical evidence but still lacks its value-reason duty. -/

Document the intended scope of mixedMissingResponsibility. The corresponding declaration concerns: Shows a discharged empirical facet does not discharge a union of applicable facets when an included value facet has no reasons. This comment is explanatory, not a proof premise.

L315theorem mixedMissingResponsibility :

State the checked result mixedMissingResponsibility. Shows a discharged empirical facet does not discharge a union of applicable facets when an included value facet has no reasons.

L316    FacetDischarged switchEmpirical ∧

Retain successful discharge of the actual empirical switch facet.

L317    ¬ LabeledDuties [] (fun f : Facet Bool => f = switchEmpirical ∨ f = .value unsupportedPosition) := by

Deny all mixed duties even with empty labels, because the actual value facet also applies and lacks recorded reasons.

L318  refine ⟨switchEmpiricalDischarged, ?_⟩

Keep the valid empirical switch facet and separately refute completion of all mixed duties.

L319  intro h

Assume every actual mixed facet is discharged, including the value facet whose recorded reason list is empty.

L320  have bad := (h (.value unsupportedPosition) (Or.inr rfl)).1

Select the value facet from the actual applicability union and extract its required nonempty reason-list condition.

L321  exact bad rfl

Its reason list is definitionally empty, contradicting only that recorded procedural requirement.

L322/- A fully identified argument may still fail to entail the stated conclusion. -/

Document the intended scope of uninformativeArgument. The corresponding declaration concerns: Constructs a nonempty articulation with no assumptions and a tautological reason; it carries no information about the switch conclusion. This comment is explanatory, not a proof premise.

L323def uninformativeArgument : Articulation Bool :=

Define uninformativeArgument. Constructs a nonempty articulation with no assumptions and a tautological reason; it carries no information about the switch conclusion.

L324  ⟨["switch state"], emptyTheory, [fun _ => True], fun _ => True⟩

Articulate a switch concept with empty assumptions and a True reason; these nonempty words do not constrain the switch world.

L325theorem articulationNotSupport : Articulated uninformativeArgument ∧

State the checked result articulationNotSupport. Proves this articulation passes the nonemptiness check while its assumptions do not entail that the world is true.

L326    ¬ Entails uninformativeArgument.assumptions (fun w : Bool => w = true) := by

The uninformative articulation’s actual assumptions do not entail that the world is true.

L327  exact ⟨⟨by simp [uninformativeArgument], by simp [uninformativeArgument]⟩,

Pair nonempty but uninformative concepts/reasons with the empty theory’s established failure to entail the switch claim.

L328    consistentIncomplete.2.1⟩

Pair nonempty but uninformative concepts/reasons with the empty theory’s established failure to entail the switch claim.

L329/- Identifiable but unrelated argument fields cannot replace the actual observation grounds under the connected adapter. -/

Document the intended scope of unrelatedArticulationRejected. The corresponding declaration concerns: Shows that a nonempty unrelated articulation and a discharged empirical facet need not align, and rejects this concrete pairing. This comment is explanatory, not a proof premise.

L330theorem unrelatedArticulationRejected :

State the checked result unrelatedArticulationRejected. Shows that a nonempty unrelated articulation and a discharged empirical facet need not align, and rejects this concrete pairing.

L331    Articulated uninformativeArgument ∧ FacetDischarged switchEmpirical ∧

Keep the unrelated articulation procedurally present and the switch facet actually discharged.

L332    ¬ FacetArticulated uninformativeArgument switchEmpirical := by

Still reject semantic matching between that unrelated articulation and this empirical facet.

L333  refine ⟨articulationNotSupport.1, switchEmpiricalDischarged, ?_⟩

Retain articulation and valid switch evidence, then separately test whether this unrelated articulation actually matches the facet.

L334  intro h

Assume the uninformative articulation semantically matches switchEmpirical, despite its empty premise theory.

L335  have relation := congrFun h.1 (Compatible [switchRecord])

Evaluate the alleged equality of articulation assumptions and empirical compatibility assumptions on the compatibility claim itself.

L336  have bad : False := relation.mpr rfl

The empirical singleton contains that compatibility claim, while the unrelated empty theory cannot; the alleged equality yields False.

L337  exact bad

Close this component of unrelatedArticulationRejected using the displayed local evidence or previously proved lemma; the component belongs to the following fixed result: Shows that a nonempty unrelated articulation and a discharged empirical facet need not align, and rejects this concrete pairing.

L338/- Repetition of the same unrelated temperature observation leaves the switch state undetermined. -/

Document the intended scope of temperatureRecord. The corresponding declaration concerns: Records only the first coordinate of a Boolean pair, observed as true; the second coordinate is unmeasured. This comment is explanatory, not a proof premise.

L339def temperatureRecord : Record (Bool × Bool) := ⟨Prod.fst, true⟩

Define temperatureRecord. Records only the first coordinate of a Boolean pair, observed as true; the second coordinate is unmeasured.

L340theorem temperatureCompatible (b : Bool) :

State the checked result temperatureCompatible. Shows duplicating that record remains compatible with either second-coordinate value when the first is true.

L341    Compatible [temperatureRecord, temperatureRecord] (true,b) := by

For any output coordinate b, repeated temperature records remain compatible with (true,b).

L342  intro r hr

For either output coordinate b, singleton-style membership in the repeated list selects the same temperature test; its observed first coordinate is true and leaves b unconstrained.

L343  simp at hr

For either output coordinate b, singleton-style membership in the repeated list selects the same temperature test; its observed first coordinate is true and leaves b unconstrained.

L344  cases hr

For either output coordinate b, singleton-style membership in the repeated list selects the same temperature test; its observed first coordinate is true and leaves b unconstrained.

L345  rfl

For either output coordinate b, singleton-style membership in the repeated list selects the same temperature test; its observed first coordinate is true and leaves b unconstrained.

L346/- The world identifies a selected action and its budget; the action costs three units. -/

Document the intended scope of BudgetWorld. The corresponding declaration concerns: Uses a Boolean action coordinate and natural-number budget as the world type. This comment is explanatory, not a proof premise.

L347abbrev BudgetWorld := Bool × Nat

Introduce the type abbreviation BudgetWorld. Uses a Boolean action coordinate and natural-number budget as the world type.

L348/- A real issued announcement asserts the selected action, but says nothing about affordability. -/

Document the intended scope of announcement. The corresponding declaration concerns: Defines a fixed declaration string; its content is not linked to budget. This comment is explanatory, not a proof premise.

L349def announcement : String := "activate"

Define announcement. Defines a fixed declaration string; its content is not linked to budget.

L350def announcementPosition : ValuePosition BudgetWorld where

Define announcementPosition. Uses an action announcement as the sole option-indexed reason while requiring actual benefit/cost and available budget.

L351  Position := Bool

Use Boolean options for on/off.

L352  Outcome := Nat × Nat

Represent each outcome as actual benefit and cost in a natural-number pair.

L353  adopted := true

Adopt the on option explicitly; adoption itself is not derived from arithmetic.

L354  selected := Prod.fst

Read actual selection from the first coordinate while leaving budget independently variable.

L355  outcome := fun _ option => (optionBenefit option, optionCost option)

Compute benefit and cost from this same actual option.

L356  objective := fun result => result.2 < result.1

Adopt the objective that actual benefit strictly exceeds actual cost.

L357  constraints := fun w option => optionCost option ≤ w.2

Compare the adopted option’s actual cost with this world’s independently supplied budget.

L358  starting := singleton (fun w => w.1 = true)

Fix selection to on without any affordability or budget assumption.

L359  reasons := [fun _ option => announcement = (if option then "activate" else "disable")]

Use the actual option-specific announcement text as the reason; it says nothing about available budget.

L360  limits := fun _ => True

Use an unrestricted world scope in this example; starting assumptions and reason content still constrain the procedure.

L361  relevantCriticism := fun w => w.2 < 3

Treat budget below 3 as relevant criticism of this cost-3 action.

L362  response := fun _ => some "reconsider the action when its cost exceeds budget"

Record a nonempty message about reconsidering the action when cost exceeds budget.

L363/- The zero-budget counterworld satisfies the stated starts, adoption and all announced reasons jointly. -/

Document the intended scope of announcementHasJointAdoption. The corresponding declaration concerns: Constructs an action-true budget-zero world where the announcement reason holds; failure later is substantive, not absent adoption. This comment is explanatory, not a proof premise.

L364theorem announcementHasJointAdoption : JointAdoption announcementPosition := by

State the checked result announcementHasJointAdoption. Constructs an action-true budget-zero world where the announcement reason holds; failure later is substantive, not absent adoption. The following tactic block proves this explicit type.

L365  refine ⟨(true,0), (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

Choose selected-on with budget 0 as a joint adoption witness; the starting theory fixes selection but does not assume affordability.

L366  intro reason hr

Take an arbitrary announcement reason at the selected-on, zero-budget joint witness.

L367  have hr' : reason = (fun (_ : BudgetWorld) (option : Bool) => announcement = (if option then "activate" else "disable")) :=

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L368    List.mem_singleton.mp hr

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L369  subst reason

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L370  rfl

The actual announcement equals the on option’s activation text; this proves the announcement reason, not the budget constraint.

L371/- A nonempty announcement remains true in a jointly admissible zero-budget world but cannot support the action's affordability. -/

Document the intended scope of announcementNotBudgetReason. The corresponding declaration concerns: At budget zero, the adopted action and true nonempty announcement reasons fail the real budget consequence, refuting the procedure. This comment is explanatory, not a proof premise.

L372theorem announcementNotBudgetReason :

State the checked result announcementNotBudgetReason. At budget zero, the adopted action and true nonempty announcement reasons fail the real budget consequence, refuting the procedure.

L373    announcementPosition.reasons ≠ [] ∧ announcementPosition.commitment (true,0) ∧

Require nonempty announcement reasons and actual adoption at selected-on with budget 0.

L374    (∀ reason, reason ∈ announcementPosition.reasons → reason (true,0) announcementPosition.adopted) ∧

At that same zero-budget world, all actual announcement reasons hold.

L375    ¬ announcementPosition.consequence (true,0) ∧ ¬ ValueProcedure announcementPosition := by

Nevertheless reject the actual consequence and the whole value procedure.

L376  refine ⟨by simp [announcementPosition], rfl, ?_, (by intro h; cases h.2), ?_⟩

Assemble nonempty announcement reasons and the true announcement; refute the zero-budget consequence and leave failure of the whole procedure.

L377  · intro reason hr

For the claimed conjunction of reasons at budget 0, take any member of the actual announcement reason list.

L378    have hr' : reason = (fun (_ : BudgetWorld) (option : Bool) => announcement = (if option then "activate" else "disable")) := List.mem_singleton.mp hr

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L379    subst reason

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L380    rfl

The actual announcement equals the on option’s activation text; this proves the announcement reason, not the budget constraint.

L381  · intro h

Assume the announcement position satisfies ValueProcedure, to test its consequence clause at budget 0.

L382    have allReasons : ∀ reason, reason ∈ announcementPosition.reasons → reason (true,0) announcementPosition.adopted := by

Collect every announcement reason at the same selected-on, zero-budget world.

L383      intro reason hr

To supply all reasons to that clause, take any announcement reason at the same zero-budget world.

L384      have hr' : reason = (fun (_ : BudgetWorld) (option : Bool) => announcement = (if option then "activate" else "disable")) := List.mem_singleton.mp hr

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L385      subst reason

Use membership to identify the actual reason as the option-indexed announcement text, then specialize it to the adopted on option.

L386      rfl

The actual announcement equals the on option’s activation text; this proves the announcement reason, not the budget constraint.

L387    have bad := h.2.2.1 (true,0) ((modelsSingleton _ _).2 rfl) trivial allReasons

Apply a hypothetical procedure to that inhabited zero-budget starting/limit case and its actual announcement reason.

L388    cases bad.2

The resulting cost constraint would require cost 3 within budget 0, which is impossible.

L389/- A repeated actual selection observation contains no budget information. -/

Document the intended scope of actionRecord. The corresponding declaration concerns: Records only the action Boolean, leaving budget completely unconstrained. This comment is explanatory, not a proof premise.

L390def actionRecord : Record BudgetWorld := ⟨Prod.fst, true⟩

Define actionRecord. Records only the action Boolean, leaving budget completely unconstrained.

L391theorem actionCompatible (budget : Nat) : Compatible [actionRecord, actionRecord] (true,budget) := by

State the checked result actionCompatible. Shows two copies of the action record accept every budget when action=true. The following tactic block proves this explicit type.

L392  intro r hr; simp at hr; cases hr; rfl

Every action record in the repeated list tests only the actual selected-on coordinate, so any supplied budget remains compatible.

L393/- Single and repeated irrelevant observations cannot establish the other outcome or the same action's budget adequacy. -/

Document the intended scope of measurementRepeatNotSupport. The corresponding declaration concerns: Combines explicit countermodels showing that repeated measurement of one coordinate does not support an unmeasured coordinate or a budget consequence, and does not fix the announcement value procedure. This comment is explanatory, not a proof premise.

L394theorem measurementRepeatNotSupport :

State the checked result measurementRepeatNotSupport. Combines explicit countermodels showing that repeated measurement of one coordinate does not support an unmeasured coordinate or a budget consequence, and does not fix the announcement value procedure.

L395    temperatureRecord.test (true,false) = true ∧

The actual temperature test returns true even when the independent output coordinate is false.

L396    Compatible [temperatureRecord,temperatureRecord] (true,false) ∧

Retain this false-output world under repeated temperature observations.

L397    Compatible [temperatureRecord,temperatureRecord] (true,true) ∧

Also retain a true-output world under those same repeated observations.

L398    ¬ Supports [temperatureRecord] (fun w : Bool × Bool => w.2 = true) ∧

A single temperature record does not support the other output being true.

L399    ¬ Supports [temperatureRecord,temperatureRecord] (fun w : Bool × Bool => w.2 = true) ∧

Repeating that temperature record still does not support the other output being true.

L400    Compatible [actionRecord,actionRecord] (true,0) ∧

Repeated observed activation is compatible with selected-on and budget 0.

L401    Compatible [actionRecord,actionRecord] (true,3) ∧

The same repeated records are also compatible with budget 3.

L402    ¬ Supports [actionRecord] announcementPosition.consequence ∧

A single activation record does not support the option’s actual objective-and-budget consequence.

L403    ¬ Supports [actionRecord,actionRecord] announcementPosition.consequence ∧

Repeating activation records does not repair that lack of consequence support.

L404    ¬ ValueProcedure announcementPosition := by

The announcement-based value procedure also fails for that actual option and constraint.

L405  refine ⟨rfl, temperatureCompatible false, temperatureCompatible true, ?_, ?_,

Record the observation’s actual true value and both temperature-compatible output alternatives; leave the unsupported output claims to refute.

L406    actionCompatible 0, actionCompatible 3, ?_, ?_, announcementNotBudgetReason.2.2.2.2⟩

Keep both budget-0 and budget-3 action-compatible worlds and the established announcement-procedure failure; leave affordability support claims to refute.

L407  · intro h

Assume a single temperature observation supports the independently represented second output being true.

L408    have bad := h (true,false) (by intro r hr; simp only [List.mem_singleton] at hr; cases hr; rfl)

Apply purported one-record output support to (true,false), whose temperature observation is true but whose other output claim is false.

L409    cases bad

Apply purported one-record output support to (true,false), whose temperature observation is true but whose other output claim is false.

L410  · intro h; have bad := h (true,false) (temperatureCompatible false); cases bad

The same (true,false) counterworld remains compatible with repeated temperature records, defeating repeated-data output support.

L411  · intro h

Assume a single action observation supports the adopted option’s benefit-and-budget consequence.

L412    have bad := h (true,0) (by intro r hr; simp only [List.mem_singleton] at hr; cases hr; rfl)

A single observed activation is compatible with budget 0; purported consequence support there would force the impossible cost constraint.

L413    cases bad.2

A single observed activation is compatible with budget 0; purported consequence support there would force the impossible cost constraint.

L414  · intro h; have bad := h (true,0) (actionCompatible 0); cases bad.2

Repeating activation records retains the same zero-budget counterworld, so it still does not support the actual affordability consequence.

L415/- Missing reason records fail a procedure; independently, a present announcement fails the explicit budget-support criterion. -/

Document the intended scope of selfAssertionNotReason. The corresponding declaration concerns: Combines empty-reason and nonempty-but-budget-irrelevant self-assertion failures, with a joint adoption witness for the latter. This comment is explanatory, not a proof premise.

L416theorem selfAssertionNotReason :

State the checked result selfAssertionNotReason. Combines empty-reason and nonempty-but-budget-irrelevant self-assertion failures, with a joint adoption witness for the latter.

L417    (unsupportedPosition.commitment true ∧ ¬ ValueProcedure unsupportedPosition) ∧

The missing-reason position can be actually adopted yet fail its recorded procedure.

L418    (announcementPosition.reasons ≠ [] ∧ announcementPosition.commitment (true,0) ∧

The stronger announcement example has nonempty reasons and actual adoption at budget 0.

L419      ¬ announcementPosition.consequence (true,0) ∧ ¬ ValueProcedure announcementPosition) ∧

Its actual consequence and its procedure still fail because the same adopted option exceeds budget.

L420    JointAdoption announcementPosition :=

Retain an actual joint adoption witness, excluding an empty-starting-domain explanation of this failure.

L421  ⟨⟨rfl, fun h => h.1 rfl⟩,

Prove unsupportedPosition.commitment true by reduction; a supposed ValueProcedure contradicts its empty reason list through its nonemptiness requirement.

L422    ⟨announcementNotBudgetReason.1, announcementNotBudgetReason.2.1,

Reuse the nonempty actual announcement reasons and adoption equality from announcementNotBudgetReason.

L423      announcementNotBudgetReason.2.2.2.1, announcementNotBudgetReason.2.2.2.2⟩,

Also reuse failure of the same zero-budget consequence and of the entire announcement procedure.

L424    announcementHasJointAdoption⟩

Retain announcementHasJointAdoption so this failure is not explained by an empty or inconsistent starting domain.

L425/- The value procedure is satisfiable although the adopted starting commitment is not entailed by empty facts. -/

Document the intended scope of valueWithoutSelfProof. The corresponding declaration concerns: Exhibits a coherent reasoned position not derivable from empty assumptions, and rejects opposite-option, inconsistent-start and impossible-adoption variants. This comment is explanatory, not a proof premise.

L426theorem valueWithoutSelfProof : ValueProcedure switchPosition ∧

State the checked result valueWithoutSelfProof. Exhibits a coherent reasoned position not derivable from empty assumptions, and rejects opposite-option, inconsistent-start and impossible-adoption variants.

L427    Satisfiable switchPosition.starting ∧

Require the switch position’s actual starting theory to have a model.

L428    ¬ Entails (emptyTheory : Theory Bool) switchPosition.commitment ∧

Deny derivation of its adopted commitment from the empty Boolean theory.

L429    (JointAdoption oppositePosition ∧ ¬ ValueProcedure oppositePosition) ∧

The opposite position has a joint witness but fails consequence assessment.

L430    (¬ ValueProcedure contradictoryStartingPosition ∧ ¬ ValueProcedure impossibleAdoptionPosition) :=

Also reject contradictory starting and impossible adoption variants, distinguishing non-self-derived from inconsistent starts.

L431  ⟨switchValueProcedure, ⟨true, (modelsSingleton _ _).2 rfl⟩, consistentIncomplete.2.1,

Combine the actual switch procedure, world true as its starting model, and non-entailment of the adopted claim from emptyTheory.

L432    oppositePositionRejected, inadmissibleValuePositionsRejected⟩

Add rejection of the inhabited opposite option and the separate contradictory-start and impossible-adoption variants.

L433/- The world records the selected option and its actual benefit/cost outcomes. -/

Document the intended scope of BenefitCostWorld. The corresponding declaration concerns: Stores a selected Boolean option together with variable benefit and cost values. This comment is explanatory, not a proof premise.

L434abbrev BenefitCostWorld := Bool × (Nat × Nat)

Introduce the type abbreviation BenefitCostWorld. Stores a selected Boolean option together with variable benefit and cost values.

L435def measuredOutcome (world : BenefitCostWorld) (option : Bool) : Nat × Nat :=

Define measuredOutcome. For true, returns the world's benefit/cost pair; false has outcome zero/zero.

L436  if option then world.2 else (0,0)

The on option reads the world’s actual benefit/cost pair; the off option yields (0,0).

L437def benefitReason (world : BenefitCostWorld) (option : Bool) : Prop :=

Define benefitReason. Requires the same option's measured benefit to equal four.

L438  (measuredOutcome world option).1 = 4

The benefit reason requires the actual option’s measured benefit to equal 4.

L439def costReason (world : BenefitCostWorld) (option : Bool) : Prop :=

Define costReason. Requires that option's measured cost to be at most three.

L440  (measuredOutcome world option).2 ≤ 3

The cost reason requires the same option’s measured cost to be at most 3.

L441/- Neither recorded benefit nor recorded cost alone establishes the selected option's joint consequence. -/

Document the intended scope of jointReasonPosition. The corresponding declaration concerns: Uses two separate option-specific benefit and cost reasons jointly for the adopted option's objective and budget. This comment is explanatory, not a proof premise.

L442def jointReasonPosition : ValuePosition BenefitCostWorld where

Define jointReasonPosition. Uses two separate option-specific benefit and cost reasons jointly for the adopted option's objective and budget.

L443  Position := Bool

Use Boolean options for on/off.

L444  Outcome := Nat × Nat

Represent each outcome as actual benefit and cost in a natural-number pair.

L445  adopted := true

Adopt the on option explicitly; adoption itself is not derived from arithmetic.

L446  selected := Prod.fst

Read selection from the world’s first coordinate, separately from measured benefit and cost.

L447  outcome := measuredOutcome

Use measuredOutcome so the assessed option’s actual benefit and cost come from this world.

L448  objective := fun result => result.2 < result.1

Adopt the objective that actual benefit strictly exceeds actual cost.

L449  constraints := fun world option => (measuredOutcome world option).2 ≤ 3

Require this option’s measured cost to be at most 3.

L450  starting := singleton (fun world => world.1 = true)

Assume the selected option is on, without assuming benefit or cost conclusions.

L451  reasons := [benefitReason, costReason]

List benefitReason and costReason together; the procedure will use their conjunction.

L452  limits := fun _ => True

Use an unrestricted world scope in this example; starting assumptions and reason content still constrain the procedure.

L453  relevantCriticism := fun world => 3 < world.2.2

Identify an actual measured cost above 3 as relevant criticism.

L454  response := fun _ => some "reassess the option when its cost exceeds the budget"

Record the nonempty response to reassess this option when its actual cost exceeds budget.

L455/- These two content constraints jointly establish the consequence in a nonempty adopted world. -/

Document the intended scope of jointReasonProcedure. The corresponding declaration concerns: Builds a joint witness at benefit four/cost three and combines both reasons to prove cost below benefit and within budget. This comment is explanatory, not a proof premise.

L456theorem jointReasonProcedure : ValueProcedure jointReasonPosition := by

State the checked result jointReasonProcedure. Builds a joint witness at benefit four/cost three and combines both reasons to prove cost below benefit and within budget. The following tactic block proves this explicit type.

L457  refine ⟨by simp [jointReasonPosition], ?_, ?_, ?_⟩

Separate the joint-reason position’s nonempty reasons, joint witness, conjunction-based consequence and criticism response.

L458  · refine ⟨(true,(4,3)), (modelsSingleton _ _).2 rfl, trivial, rfl, ?_⟩

Use selected-on with benefit 4 and cost 3 as the common starting/limit/adoption witness.

L459    intro reason hr

Take any of the two reasons at the actual (true,(4,3)) witness, then split membership to check each distinct reason.

L460    change reason ∈ [benefitReason,costReason] at hr

Expose the actual two-element reason list: benefitReason and costReason.

L461    rcases List.mem_cons.mp hr with hr | hr

Split reason membership into the benefit reason or the remaining singleton cost reason.

L462    · subst reason; rfl

Substitute the benefit reason and check that the witness’s measured benefit is exactly 4.

L463    · have hr' := List.mem_singleton.mp hr

Identify the remaining reason with costReason and substitute it.

L464      subst reason

Identify the remaining reason with costReason and substitute it.

L465      change 3 ≤ 3; exact Nat.le_refl 3

Check the witness’s cost bound 3 ≤ 3 by reflexivity of the natural-number order.

L466  · intro world _ _ reasons

For an arbitrary admitted world, assume all active reasons together rather than requiring either reason alone to suffice.

L467    have benefit := reasons benefitReason (by change benefitReason ∈ [benefitReason,costReason]; simp)

Extract the actual benefitReason from the reason conjunction at this world and adopted option.

L468    have cost := reasons costReason (by change costReason ∈ [benefitReason,costReason]; simp)

Extract costReason from the same conjunction at the same world and option.

L469    change (measuredOutcome world true).1 = 4 at benefit

Unfold benefitReason: the adopted on option’s measured benefit equals 4.

L470    change (measuredOutcome world true).2 ≤ 3 at cost

Unfold costReason: that same option’s measured cost is at most 3.

L471    refine ⟨?_, cost⟩

Retain the actual cost constraint and leave only the strict benefit-over-cost objective.

L472    have bigger : 3 < (measuredOutcome world true).1 := by rw [benefit]; decide

Rewrite the measured benefit to 4 and check that it exceeds 3.

L473    exact Nat.lt_of_le_of_lt cost bigger

Compose cost ≤ 3 with 3 < benefit to establish cost < benefit using both reasons.

L474  · intro world _ _

For a world within limits where criticism is relevant, construct the required response about this option’s excessive cost.

L475    exact ⟨"reassess the option when its cost exceeds the budget", rfl, by decide⟩

Provide the explicit nonempty response about reassessing the option when its cost exceeds the budget; this records a response, not its persuasive adequacy.

L476/- Each separate reason has a concrete same-start/limit/adoption counterworld; their conjunction is sufficient. -/

Document the intended scope of JointReasonsExample. The corresponding declaration concerns: States that the joint procedure passes while either reason alone can hold at a world failing the consequence. This comment is explanatory, not a proof premise.

L477def JointReasonsExample : Prop :=

Define JointReasonsExample. States that the joint procedure passes while either reason alone can hold at a world failing the consequence.

L478  ValueProcedure jointReasonPosition ∧

Require the two-reason position to satisfy its complete ValueProcedure.

L479  (Models jointReasonPosition.starting (true,(4,5)) ∧ jointReasonPosition.limits (true,(4,5)) ∧

Fix a benefit-only counterworld (true,(4,5)) satisfying the same starting assumptions and limits.

L480    jointReasonPosition.commitment (true,(4,5)) ∧ benefitReason (true,(4,5)) true ∧

At that world, actual adoption and the benefit reason both hold.

L481    ¬ jointReasonPosition.consequence (true,(4,5))) ∧

Deny the assessed consequence there, because its actual cost is too high.

L482  (Models jointReasonPosition.starting (true,(0,3)) ∧ jointReasonPosition.limits (true,(0,3)) ∧

Fix a cost-only counterworld (true,(0,3)) under the same starting assumptions and limits.

L483    jointReasonPosition.commitment (true,(0,3)) ∧ costReason (true,(0,3)) true ∧

At this world, actual adoption and the cost reason hold.

L484    ¬ jointReasonPosition.consequence (true,(0,3)))

Deny its assessed consequence because zero benefit does not exceed cost 3.

L485theorem jointReasonsExample : JointReasonsExample := by

State the checked result jointReasonsExample. Uses benefit four/cost five and benefit zero/cost three as counterexamples to individual-reason sufficiency. The following tactic block proves this explicit type.

L486  refine ⟨jointReasonProcedure,

Begin the combined example with the already checked two-reason procedure.

L487    ⟨(modelsSingleton _ _).2 rfl, trivial, rfl, rfl, ?_⟩,

Supply the benefit-only counterworld with benefit 4 and cost 5, satisfying the same starting, limit and adoption conditions.

L488    ⟨(modelsSingleton _ _).2 rfl, trivial, rfl, Nat.le_refl 3, ?_⟩⟩

Supply the cost-only counterworld with benefit 0 and cost 3 under the same conditions.

L489  · intro h; have bad : 5 ≤ 3 := h.2; omega

The benefit-only world violates the cost constraint 5 ≤ 3; natural-number arithmetic closes the contradiction.

L490  · intro h; have bad : 3 < 0 := h.1; omega

The cost-only world cannot satisfy the strict objective 3 < 0; arithmetic closes this counterexample.

L491/- Empirical observations, semantic inference and criticism-responsive reasons coexist without a scalar score. -/

Document the intended scope of heterogeneousReasons. The corresponding declaration concerns: Combines empirical, inferential and value examples with a genuine two-reason combination that neither reason alone establishes. This comment is explanatory, not a proof premise.

L492theorem heterogeneousReasons :

State the checked result heterogeneousReasons. Combines empirical, inferential and value examples with a genuine two-reason combination that neither reason alone establishes.

L493    FacetDischarged switchEmpirical ∧

Include the actually discharged empirical switch facet.

L494    FacetDischarged (Facet.inferential (singleton (fun w : Bool => w = true)) (fun w => w = true)) ∧

Include an inferential facet whose satisfiable true-world premise entails the same true-world claim.

L495    FacetDischarged (Facet.value switchPosition) ∧ JointReasonsExample := by

Include the actual switch value procedure and the two-joint-reasons example in this registered theorem.

L496  refine ⟨switchEmpiricalDischarged, ⟨⟨true, (modelsSingleton _ _).2 rfl⟩, ?_⟩, switchValueProcedure, jointReasonsExample⟩

Combine the checked empirical facet, an inhabited inferential singleton, the value procedure and the joint-reason counterexamples.

L497  intro w hw; exact (modelsSingleton (fun x : Bool => x = true) w).1 hw

For the inferential facet, its singleton premise directly yields the same true-world claim at any model.

L499/- This local observation checks the actual output on input zero. -/

Document the intended scope of zeroRecord. The corresponding declaration concerns: Records only a function's Boolean output at natural-number input zero. This comment is explanatory, not a proof premise.

L500def zeroRecord : Record (Nat → Bool) := ⟨fun f => f 0, true⟩

Define zeroRecord. Records only a function's Boolean output at natural-number input zero.

L501def localGenerator (seed : Nat) : Nat → Bool := fun n => n == seed

Define localGenerator. Produces a function returning true exactly at its natural-number seed.

L502/- All outputs being true is a stronger, explicitly quantified capability claim. -/

Document the intended scope of allTrue. The corresponding declaration concerns: Requires a Boolean-valued function to return true at every natural number. This comment is explanatory, not a proof premise.

L503def allTrue : Claim (Nat → Bool) := fun f => ∀ n, f n = true

Define allTrue. Requires a Boolean-valued function to return true at every natural number.

L504theorem zeroCompatible (f : Nat → Bool) : Compatible [zeroRecord] f ↔ f 0 = true := by

State the checked result zeroCompatible. Proves one zero-input record constrains exactly the function's value at zero. The following tactic block proves this explicit type.

L505  constructor

Prove both directions between matching zeroRecord and the actual function returning true at input 0.

L506  · intro h; exact h zeroRecord (by simp)

Apply record compatibility to the sole named test to recover its actual observed equality.

L507  · intro hf r hr; simp only [List.mem_singleton] at hr; cases hr; exact hf

Conversely, singleton membership identifies any listed record with this test, whose equality is the supplied observation premise.

L508/- A generating subject owns an earlier predicate and a seed used to revise that actual predicate. -/

Document the intended scope of GeneratingProcess. The corresponding declaration concerns: Stores producer identity, the actual earlier predicate and the seed used by its revision algorithm. This comment is explanatory, not a proof premise.

L509structure GeneratingProcess where

Declare the data interface GeneratingProcess. Stores producer identity, the actual earlier predicate and the seed used by its revision algorithm.

L510  owner : Nat

Store the actual generating process owner identifier.

L511  prior : Nat → Bool

Store the prior Boolean-valued function before this process generates its revision.

L512  generateSeed : Nat

Store the seed input used by this process’s actual local generator.

L513/- The revision preserves prior successes and adds the seed-selected case through the actual generator. -/

Document the intended scope of GeneratingProcess.outputRevision. The corresponding declaration concerns: Preserves prior successes and adds the seed-selected input through the actual local generator. This comment is explanatory, not a proof premise.

L514def GeneratingProcess.outputRevision (process : GeneratingProcess) : Nat → Bool :=

Define GeneratingProcess.outputRevision. Preserves prior successes and adds the seed-selected input through the actual local generator.

L515  fun input => process.prior input || localGenerator process.generateSeed input

The revised function preserves each true prior output or adds truth at the actual generated seed input.

L516/- A produced revision retains its producer and exact old/new objects. -/

Document the intended scope of ProducedRevision. The corresponding declaration concerns: Stores producer plus exact before and after predicate objects. This comment is explanatory, not a proof premise.

L517structure ProducedRevision where

Declare the data interface ProducedRevision. Stores producer plus exact before and after predicate objects.

L518  producer : Nat

Identify which owner produced this concrete revision object.

L519  before : Nat → Bool

Store the actual before-function of the revision.

L520  after : Nat → Bool

Store the actual after-function of the revision.

L521/- The subject itself constructs the owned before/after revision object. -/

Document the intended scope of GeneratingProcess.produce. The corresponding declaration concerns: Constructs this process's own revision with its owner and actual prior/output functions. This comment is explanatory, not a proof premise.

L522def GeneratingProcess.produce (process : GeneratingProcess) : ProducedRevision :=

Define GeneratingProcess.produce. Constructs this process's own revision with its owner and actual prior/output functions.

L523  ⟨process.owner, process.prior, process.outputRevision⟩

Construct the revision directly from this process’s owner, prior function and computed output revision.

L524def sampleGeneratingProcess : GeneratingProcess := ⟨17, fun _ => false, 0⟩

Define sampleGeneratingProcess. Uses owner seventeen, an always-false prior predicate and seed zero.

L525/- This same-owner revision actually changes input zero, while its produced predicate still fails at input one. -/

Document the intended scope of OwnedRevisionExample. The corresponding declaration concerns: Binds self-origin and exact before/after functions to a real zero-input change whose global claim lacks support. This comment is explanatory, not a proof premise.

L526def OwnedRevisionExample : Prop :=

Define OwnedRevisionExample. Binds self-origin and exact before/after functions to a real zero-input change whose global claim lacks support.

L527  sampleGeneratingProcess.produce.producer = sampleGeneratingProcess.owner ∧

Bind the revision’s producer identifier to the actual generating process owner.

L528  sampleGeneratingProcess.produce.before = sampleGeneratingProcess.prior ∧

Bind its before-function to this process’s actual prior function.

L529  sampleGeneratingProcess.produce.after = sampleGeneratingProcess.outputRevision ∧

Bind its after-function to this process’s actual outputRevision.

L530  sampleGeneratingProcess.produce.before 0 = false ∧ sampleGeneratingProcess.produce.after 0 = true ∧

Require actual change at input 0 from false before to true after.

L531  sampleGeneratingProcess.produce.after 1 = false ∧

Retain an actual false output at input 1 after that revision.

L532  Compatible [zeroRecord] sampleGeneratingProcess.produce.after ∧

The actual produced after-function matches the input-0 observation.

L533  ¬ Supports [zeroRecord] allTrue

That record still does not support the all-input truth claim.

L534/- Actual producer/old/new links and the compatible failing revision witness the insufficiency of self-origin. -/

Document the intended scope of ownedRevisionExample. The corresponding declaration concerns: Computes ownership/object links and uses the produced function's failure at one to refute universal support. This comment is explanatory, not a proof premise.

L535theorem ownedRevisionExample : OwnedRevisionExample := by

State the checked result ownedRevisionExample. Computes ownership/object links and uses the produced function's failure at one to refute universal support. The following tactic block proves this explicit type.

L536  refine ⟨rfl,rfl,rfl,rfl,rfl,rfl,(zeroCompatible _).2 rfl, ?_⟩

Check producer identity, prior/output revision relationships and actual sample values by computation; retain zero-record compatibility and leave universal support to refute.

L537  intro h

Assume zeroRecord supports allTrue, to refute it using this owner’s actual produced revision.

L538  have bad := h sampleGeneratingProcess.produce.after ((zeroCompatible _).2 rfl) 1

Apply purported support to this owner’s actual produced after-function at input 1, where its revision still returns false.

L539  cases bad

Eliminate the resulting false=true equality; the actual revision is an evidence-compatible counterexample.

L540/- The generator's own sample succeeds, but its generated revision has a concrete unsupported global claim. -/

Document the intended scope of selfOriginDoesNotSupport. The corresponding declaration concerns: Retains the local observation countermodel and adds an actual owned before/after revision with the same unsupported global claim. This comment is explanatory, not a proof premise.

L541theorem selfOriginDoesNotSupport :

State the checked result selfOriginDoesNotSupport. Retains the local observation countermodel and adds an actual owned before/after revision with the same unsupported global claim.

L542    localGenerator 0 0 = true ∧ localGenerator 0 1 = false ∧

Compute localGenerator 0 as true at 0 and false at 1.

L543    Compatible [zeroRecord] (localGenerator 0) ∧

Require this generated function to match the same input-0 record.

L544    ¬ Supports [zeroRecord] allTrue ∧ OwnedRevisionExample := by

State failure of all-input support and include the concrete owner/prior/revision relationship example.

L545  refine ⟨rfl, rfl, (zeroCompatible _).2 rfl, ?_, ownedRevisionExample⟩

Compute the generated function’s values at 0 and 1, give its zero-record compatibility, and include the owned revision relationship example.

L546  intro h

Assume the local zero observation entails true output at every input of every compatible function.

L547  have bad := h (localGenerator 0) ((zeroCompatible _).2 rfl) 1

Instantiate alleged universal support with localGenerator 0 and then input 1; compatibility at 0 did not constrain this failing input.

L548  cases bad

Eliminate the resulting false=true equality; the actual revision is an evidence-compatible counterexample.

L549/- A proper local observation allows both a universally successful and a failing extension. -/

Document the intended scope of localNotUniversal. The corresponding declaration concerns: Exhibits both a universally true function and a zero-only true function compatible with the same observation, with an explicit outside input; therefore the observation does not support universal truth. This comment is explanatory, not a proof premise.

L550theorem localNotUniversal :

State the checked result localNotUniversal. Exhibits both a universally true function and a zero-only true function compatible with the same observation, with an explicit outside input; therefore the observation does not support universal truth.

L551    (∃ outside : Nat, outside ≠ 0) ∧

Require at least one natural-number input outside the observed singleton scope.

L552    Compatible [zeroRecord] (fun _ => true) ∧

The constant-true function matches the zero observation.

L553    Compatible [zeroRecord] (localGenerator 0) ∧

The local generator also matches that same observation.

L554    allTrue (fun _ => true) ∧ ¬ allTrue (localGenerator 0) ∧

The first function is universally true while the second is not.

L555    ¬ Supports [zeroRecord] allTrue := by

Therefore the shared observation does not support universal truth.

L556  refine ⟨⟨1, by decide⟩, (zeroCompatible _).2 rfl, (zeroCompatible _).2 rfl,

Provide an input outside the observed scope and show both the constant-true function and local generator satisfy the same zero observation.

L557    (fun _ => rfl), ?_, selfOriginDoesNotSupport.2.2.2.1⟩

The constant function is universally true; retain the known support counterexample and leave the local generator’s universal claim to refute.

L558  intro h; have bad := h 1; cases bad

Evaluate any proposed all-input truth of the local generator at 1, where its actual result is false.

L559/- Two implementations agree on the actual observed input and differ on a specified relevant omitted input. -/

Document the intended scope of hiddenDifference. The corresponding declaration concerns: Shows the two functions agree on the domain restricted to zero and disagree at one; local agreement does not establish global equality. This comment is explanatory, not a proof premise.

L560theorem hiddenDifference :

State the checked result hiddenDifference. Shows the two functions agree on the domain restricted to zero and disagree at one; local agreement does not establish global equality.

L561    (∀ n : Nat, n = 0 → (fun _ : Nat => true) n = localGenerator 0 n) ∧

State equality of both functions only for inputs satisfying n=0.

L562    (fun _ : Nat => true) 1 ≠ localGenerator 0 1 := by

State their concrete output inequality at input 1.

L563  refine ⟨?_, by decide⟩

Separate agreement on the input-0 scope from the concrete output difference at input 1.

L564  intro n hn; cases hn; rfl

Substitute n=0 from the scope premise; both functions then compute to true.

L565/- One observation supplies only its actual input-specific consequence, without repetition. -/

Document the intended scope of singleObservation. The corresponding declaration concerns: A single zero-input observation is nonvacuously compatible and supports its local result but does not support the all-input claim. This comment is explanatory, not a proof premise.

L566theorem singleObservation : [zeroRecord].length = 1 ∧

State the checked result singleObservation. A single zero-input observation is nonvacuously compatible and supports its local result but does not support the all-input claim.

L567    (∃ f, Compatible [zeroRecord] f) ∧

Require an actual function compatible with the single observation, preventing empty evidence semantics.

L568    Supports [zeroRecord] (fun f => f 0 = true) ∧

That single record supports its actual input-0 claim.

L569    ¬ Supports [zeroRecord] allTrue :=

It does not support the stronger all-input claim.

L570  ⟨rfl, ⟨localGenerator 0, (zeroCompatible _).2 rfl⟩,

Compute the record count as one and provide localGenerator 0 as an actual compatible witness.

L571    (fun f hf => (zeroCompatible f).1 hf), selfOriginDoesNotSupport.2.2.2.1⟩

Extract the supported input-0 fact directly from compatibility and reuse the established failure of allTrue support.

L572/- This inferential assessment derives a successor value from its explicit numeric premise without observation. -/

Document the intended scope of arithmeticFacet. The corresponding declaration concerns: Defines an inferential facet with assumption n=2 and conclusion n+1=3. This comment is explanatory, not a proof premise.

L573def arithmeticFacet : Facet Nat := .inferential (singleton (fun n => n = 2)) (fun n => n + 1 = 3)

Define arithmeticFacet. Defines an inferential facet with assumption n=2 and conclusion n+1=3.

L574def usesObservation {W : Type} : Facet W → Bool

Define usesObservation. Returns true only for empirical facet tags; this is a classification test, not an analysis of computational executability.

L575  | .empirical _ _ _ _ => true

Classify an empirical facet as using observation because it carries actual test records.

L576  | _ => false

Classify inferential and value facets as not using observation in this represented method classifier.

L577/- An actual valid inferential assessment refutes a mandatory measurement/repetition/framework chain. -/

Document the intended scope of noUniversalChain. The corresponding declaration concerns: Discharges the arithmetic implication with a model n=2 while its observation tag is false. This is an example of nonempirical discharge, not a universal account of knowledge. This comment is explanatory, not a proof premise.

L578theorem noUniversalChain : FacetDischarged arithmeticFacet ∧ usesObservation arithmeticFacet = false := by

State the checked result noUniversalChain. Discharges the arithmetic implication with a model n=2 while its observation tag is false. This is an example of nonempirical discharge, not a universal account of knowledge. The following tactic block proves this explicit type.

L579  refine ⟨⟨⟨2, (modelsSingleton _ _).2 rfl⟩, ?_⟩, rfl⟩

Provide n=2 as the inferential theory’s nonempty witness and note that its facet constructor uses no observation.

L580  intro n hn

Take any natural-number world n satisfying the arithmetic facet’s actual premise theory.

L581  have premise := (modelsSingleton (fun x : Nat => x = 2) n).1 hn

Extract n=2 from the actual singleton premise, rather than assuming the desired successor conclusion.

L582  change n + 1 = 3

Expose the arithmetic conclusion n+1=3 as the remaining goal.

L583  rw [premise]

Rewrite n to 2 using the premise; the required arithmetic equality reduces by computation.

L584/- A trial has a reproducible setting, an actual outcome and a separately recorded outcome. -/

Document the intended scope of Trial. The corresponding declaration concerns: Stores setting, actual outcome and recorded outcome as independent natural-number fields, with no measurement mechanism. This comment is explanatory, not a proof premise.

L585structure Trial where

Declare the data interface Trial. Stores setting, actual outcome and recorded outcome as independent natural-number fields, with no measurement mechanism.

L586  setting : Nat

Store the trial’s setting separately from its outcomes.

L587  actualOutcome : Nat

Store the trial’s actual outcome, whether accurately recorded or not.

L588  recordedOutcome : Nat

Store the separately recorded outcome to allow accuracy comparisons.

L589/- Verifying a record, reproducing settings and retaining a conclusion are separate predicates. -/

Document the intended scope of Verified. The corresponding declaration concerns: Verification means exact equality of the two supplied outcome fields. This comment is explanatory, not a proof premise.

L590def Verified (t : Trial) : Prop := t.recordedOutcome = t.actualOutcome

Define Verified. Verification means exact equality of the two supplied outcome fields.

L591def Reproduced (a b : Trial) : Prop := a.setting = b.setting

Define Reproduced. Reproduction means only equality of two setting fields; it does not require matching outcomes or histories.

L592def Bounded (t : Trial) : Prop := t.actualOutcome ≤ 2

Define Bounded. The bound property is actualOutcome≤2, a fixed threshold rather than a general stability theory.

L593/- Same-setting possible trials can differ while preserving the chosen bound; no probability semantics is claimed. -/

Document the intended scope of variableOutcomesStableBound. The corresponding declaration concerns: Exhibits matching settings with different actual outcomes that both satisfy the fixed upper bound. This comment is explanatory, not a proof premise.

L594theorem variableOutcomesStableBound :

State the checked result variableOutcomesStableBound. Exhibits matching settings with different actual outcomes that both satisfy the fixed upper bound.

L595    let a : Trial := ⟨0,1,1⟩

Fix the first trial at setting 0 with actual and recorded outcome 1.

L596    let b : Trial := ⟨0,2,2⟩

Fix the second trial at the same setting with actual and recorded outcome 2.

L597    Reproduced a b ∧ a.actualOutcome ≠ b.actualOutcome ∧ Bounded a ∧ Bounded b := by

Require the two explicitly fixed trials to share settings, differ in actual outcomes and both satisfy actualOutcome ≤ 2.

L598  simp [Reproduced, Bounded]

Evaluate the two same-setting trials: actual outcomes 1 and 2 differ, but each satisfies actualOutcome ≤ 2.

L599/- Concrete records distinguish record accuracy, condition reproduction and conclusion stability. -/

Document the intended scope of verificationReproductionStability. The corresponding declaration concerns: Uses explicit numeric trials to separate recorded/actual agreement, equal settings, and the fixed outcome bound. This comment is explanatory, not a proof premise.

L600theorem verificationReproductionStability :

State the checked result verificationReproductionStability. Uses explicit numeric trials to separate recorded/actual agreement, equal settings, and the fixed outcome bound.

L601    (Verified ⟨0,1,1⟩ ∧ Verified ⟨1,1,1⟩ ∧ ¬ Reproduced ⟨0,1,1⟩ ⟨1,1,1⟩) ∧

Require two accurately recorded trials whose settings nevertheless differ.

L602    (Reproduced ⟨0,1,1⟩ ⟨0,3,2⟩ ∧ ¬ Verified ⟨0,3,2⟩ ∧ ¬ Bounded ⟨0,3,2⟩) ∧

Require repeated settings alongside an inaccurate second record and an actual result exceeding the bound.

L603    (Bounded ⟨0,1,1⟩ ∧ Bounded ⟨0,2,0⟩ ∧ ¬ Verified ⟨0,2,0⟩) := by

Require preserved bounds even though one recorded outcome is inaccurate.

L604  simp [Verified, Reproduced, Bounded]

Compute each concrete trial predicate separately, exhibiting changed settings, inaccurate recording and failure or preservation of the bound without conflating them.

L605/- Explanation certificates are executable syntax for this same arithmetic process. -/

Document the intended scope of Program. The corresponding declaration concerns: Defines a tiny program language with doubling and natural-number constants only. This comment is explanatory, not a proof premise.

L606inductive Program where

Declare the alternatives Program. Defines a tiny program language with doubling and natural-number constants only.

L607  | doubleInput

Provide syntax for the explanation program that doubles its actual input.

L608  | constant (value : Nat)

Provide syntax for a constant-output explanation program carrying its returned natural number.

L609def Program.eval : Program → Nat → Nat

Define Program.eval. Defines the executable meaning of the two program constructors.

L610  | .doubleInput, n => n + n

Evaluate the doubleInput explanation program at n by actual addition n+n.

L611  | .constant value, _ => value

Evaluate a constant program by returning its stored value, independently of the input.

L612/- A process exposes outputs and an explanation response, whose certificate can be checked against those outputs. -/

Document the intended scope of Process. The corresponding declaration concerns: A process consists of an arbitrary natural-number function and an optional tiny-language explanation program. This comment is explanatory, not a proof premise.

L613structure Process where

Declare the data interface Process. A process consists of an arbitrary natural-number function and an optional tiny-language explanation program.

L614  output : Nat → Nat

Store the same process’s actual output function over natural-number inputs.

L615  explanation : Option Program

Store the process’s optional supplied explanation program, separately from its output function.

L616/- The output-only application contract checks every relevant input. -/

Document the intended scope of OutputContract. The corresponding declaration concerns: Requires the output function to double every natural-number input. This comment is explanatory, not a proof premise.

L617def OutputContract (p : Process) : Prop := ∀ n, p.output n = n + n

Define OutputContract. Requires the output function to double every natural-number input.

L618/- The explanation application contract requires a provided certificate faithful to this very process. -/

Document the intended scope of ExplanationContract. The corresponding declaration concerns: Requires an attached program whose evaluated outputs equal the process output on every input; this is extensional agreement, not causal or human explanatory adequacy. This comment is explanatory, not a proof premise.

L619def ExplanationContract (p : Process) : Prop :=

Define ExplanationContract. Requires an attached program whose evaluated outputs equal the process output on every input; this is extensional agreement, not causal or human explanatory adequacy.

L620  ∃ program, p.explanation = some program ∧ ∀ n, program.eval n = p.output n

Require an actually supplied program whose evaluation equals this process’s output at every natural input.

L621/- This process produces doubled values but returns no explanatory certificate. -/

Document the intended scope of outputOnlyProcess. The corresponding declaration concerns: Constructs the correct doubling function without any attached explanation program. This comment is explanatory, not a proof premise.

L622def outputOnlyProcess : Process := ⟨fun n => n + n, none⟩

Define outputOnlyProcess. Constructs the correct doubling function without any attached explanation program.

L623def explainedProcess : Process := ⟨fun n => n + n, some .doubleInput⟩

Define explainedProcess. Constructs the same output function with the doubling program attached.

L624/- Object scope fixes the very process whose contract is assessed; contract inputs themselves still range over all naturals. -/

Document the intended scope of processScope. The corresponding declaration concerns: Restricts modeled candidates to the exact assessed process, without restricting the contract's input quantifier. This comment is explanatory, not a proof premise.

L625def processScope (assessed : Process) : Theory Process :=

Define processScope. Restricts modeled candidates to the exact assessed process, without restricting the contract's input quantifier.

L626  singleton (fun candidate => candidate = assessed)

Restrict theory models by the actual equality candidate=assessed, not by assuming the desired contract.

L627/- This inferential facet checks an explicit contract under exact process-identity assumptions. -/

Document the intended scope of processContractFacet. The corresponding declaration concerns: Builds an inferential contract facet under the exact assessed-process identity assumption. This comment is explanatory, not a proof premise.

L628def processContractFacet (assessed : Process) (contract : Claim Process) : Facet Process :=

Define processContractFacet. Builds an inferential contract facet under the exact assessed-process identity assumption.

L629  .inferential (processScope assessed) contract

Build an inferential facet with that exact object-identity scope and the supplied contract conclusion.

L630/- The scope's compatible interpretations are exactly this assessed process, not an unrelated substitute. -/

Document the intended scope of processScopeModels. The corresponding declaration concerns: Proves that modeling the identity scope is exactly equality to the assessed process. This comment is explanatory, not a proof premise.

L631theorem processScopeModels (assessed candidate : Process) :

State the checked result processScopeModels. Proves that modeling the identity scope is exactly equality to the assessed process.

L632    Models (processScope assessed) candidate ↔ candidate = assessed :=

State that modeling this scope is exactly equality to the assessed process.

L633  modelsSingleton (fun process => process = assessed) candidate

Instantiate modelsSingleton with equality to the actual assessed Process, proving exactly which candidates satisfy processScope.

L634/- A concrete contract proof supplies the facet's consequence for its scoped object. -/

Document the intended scope of processContractDischarged. The corresponding declaration concerns: Uses a supplied proof of the actual process contract and scope equality to discharge the corresponding inferential facet. This comment is explanatory, not a proof premise.

L635theorem processContractDischarged (assessed : Process) (contract : Claim Process) (proof : contract assessed) :

State the checked result processContractDischarged. Uses a supplied proof of the actual process contract and scope equality to discharge the corresponding inferential facet.

L636    FacetDischarged (processContractFacet assessed contract) := by

Conclude discharge for that same object’s contract facet using the explicit contract-proof premise.

L637  refine ⟨⟨assessed,(processScopeModels _ _).2 rfl⟩, ?_⟩

Use the assessed process itself as a model of its identity scope; leave semantic entailment of its contract.

L638  intro candidate hc

Take a candidate and proof hc that it lies in the actual assessed process’s identity scope.

L639  have same := (processScopeModels _ _).1 hc

From the scope model hc, recover that the candidate is exactly the assessed process.

L640  subst candidate

Substitute that process identity so the contract goal is about the actual assessed object.

L641  exact proof

Use the explicit premise proof of this object’s contract; the generic helper does not create contract correctness without that premise.

L642/- Scoped capability grounds include exact claim, object-specific assumptions, canonical articulation and actual assessment. -/

Document the intended scope of ProcessGrounds. The corresponding declaration concerns: Requires canonical Grounds for this exact process/contract facet and its singleton applicability. This comment is explanatory, not a proof premise.

L643def ProcessGrounds (assessed : Process) (contract : Claim Process) : Prop :=

Define ProcessGrounds. Requires canonical Grounds for this exact process/contract facet and its singleton applicability.

L644  Grounds contract canonicalArticulation (fun facet => facet = processContractFacet assessed contract)

Require Grounds for the supplied contract using canonical articulation and the exact assessed-process facet as applicable.

L645    [processContractFacet assessed contract]

The listed evidence package contains precisely that same process-contract facet.

L646theorem processGrounds (assessed : Process) (contract : Claim Process) (proof : contract assessed) :

State the checked result processGrounds. Constructs matching contract Grounds from an actual proof for that same assessed process.

L647    ProcessGrounds assessed contract := by

Conclude these same-object ProcessGrounds from the explicit proof of the contract at the assessed process.

L648  have discharged := processContractDischarged assessed contract proof

Apply the contract-discharge helper to the explicit proof for this same assessed process.

L649  refine ⟨by simp, ?_, ?_⟩

Separate nonempty facets, exact applicability coverage and each facet’s claim/articulation/discharge obligations.

L650  · intro facet hf; subst facet; exact List.mem_singleton.mpr rfl

The applicability assumption identifies the facet with the one prescribed facet, which belongs to the singleton list.

L651  · intro facet hf; have hf' := List.mem_singleton.mp hf; subst facet

Singleton membership identifies the current facet with the prescribed one; substitute it to check its exact claim and grounds.

L652    exact ⟨rfl,canonicalArticulated _ discharged,canonicalFacetArticulated _,discharged⟩

Assemble the same contract claim, nonempty canonical articulation, semantic connection to the object scope and the established discharge.

L653/- Universal output correctness here comes from the concrete program definition, not from an assumed capability label. -/

Document the intended scope of outputCorrectByEvaluation. The corresponding declaration concerns: Proves all-input doubling directly from the concrete output function, not an assumed success flag. This comment is explanatory, not a proof premise.

L654theorem outputCorrectByEvaluation : OutputContract outputOnlyProcess := fun _ => rfl

State the checked result outputCorrectByEvaluation. Proves all-input doubling directly from the concrete output function, not an assumed success flag. The supplied proof term uses the displayed constructed witnesses or earlier lemmas, rather than adding an axiom.

L655/- This same process actually returns no explanation certificate. -/

Document the intended scope of outputOnlyNoExplanation. The corresponding declaration concerns: Rejects an attached explanation witness because the same process stores none. This comment is explanatory, not a proof premise.

L656theorem outputOnlyNoExplanation : ¬ ExplanationContract outputOnlyProcess := by

State the checked result outputOnlyNoExplanation. Rejects an attached explanation witness because the same process stores none. The following tactic block proves this explicit type.

L657  rintro ⟨program,h,_⟩; cases h

Any explanation contract would supply a program whose some value equals the process’s actual none response; distinct option constructors make that impossible.

L658/- The full application contract requires outputs and an explanation of that same process. -/

Document the intended scope of FullProcessContract. The corresponding declaration concerns: Conjoins output correctness with an attached output-faithful explanation for the same process. This comment is explanatory, not a proof premise.

L659def FullProcessContract (assessed : Process) : Prop := OutputContract assessed ∧ ExplanationContract assessed

Define FullProcessContract. Conjoins output correctness with an attached output-faithful explanation for the same process.

L660/- Output-only grounds have the assessed process itself as a counterworld to the stronger contract. -/

Document the intended scope of OutputContractEvidence. The corresponding declaration concerns: Combines grounded output and a nonempty exact-process scope whose model refutes the stronger full contract. This comment is explanatory, not a proof premise.

L661def OutputContractEvidence : Prop :=

Define OutputContractEvidence. Combines grounded output and a nonempty exact-process scope whose model refutes the stronger full contract.

L662  ProcessGrounds outputOnlyProcess OutputContract ∧

Require grounded output correctness for the actual output-only process.

L663  Models (processScope outputOnlyProcess) outputOnlyProcess ∧

Keep that process itself as an inhabitant of the exact assessment scope.

L664  ¬ Entails (processScope outputOnlyProcess) FullProcessContract

Deny that this same scope entails the stronger output-plus-explanation contract.

L665/- Existing output evidence does not supply the absent explanation for the same object and scope. -/

Document the intended scope of outputContractEvidence. The corresponding declaration concerns: Builds output Grounds by evaluation and uses the missing explanation at the same process to refute full-contract entailment. This comment is explanatory, not a proof premise.

L666theorem outputContractEvidence : OutputContractEvidence := by

State the checked result outputContractEvidence. Builds output Grounds by evaluation and uses the missing explanation at the same process to refute full-contract entailment. The following tactic block proves this explicit type.

L667  refine ⟨processGrounds _ _ outputCorrectByEvaluation, (processScopeModels _ _).2 rfl, ?_⟩

Supply the actual output contract’s grounds and the process’s own scope witness, then refute the stronger contract under that very scope.

L668  intro stronger

Assume that this exact process scope entails the stronger output-plus-explanation contract.

L669  exact outputOnlyNoExplanation (stronger outputOnlyProcess ((processScopeModels _ _).2 rfl)).2

Instantiate alleged full-contract entailment at outputOnlyProcess itself; its explanation component contradicts the proven absent explanation.

L670/- Both actual application contracts have grounds and explicit object scopes; neither scope is empty. -/

Document the intended scope of ScopedApplicationEvidence. The corresponding declaration concerns: Requires both different application contracts to have Grounds and nonempty exact-process scopes. This comment is explanatory, not a proof premise.

L671def ScopedApplicationEvidence : Prop :=

Define ScopedApplicationEvidence. Requires both different application contracts to have Grounds and nonempty exact-process scopes.

L672  ProcessGrounds outputOnlyProcess OutputContract ∧

Include grounded output correctness for outputOnlyProcess.

L673  ProcessGrounds explainedProcess FullProcessContract ∧

Include grounded output and explanation together for explainedProcess.

L674  (∀ candidate, Models (processScope outputOnlyProcess) candidate ↔ candidate = outputOnlyProcess) ∧

Make the first scope’s exact identity with outputOnlyProcess explicit for every candidate.

L675  (∀ candidate, Models (processScope explainedProcess) candidate ↔ candidate = explainedProcess) ∧

Likewise make the second scope’s exact identity with explainedProcess explicit.

L676  Satisfiable (processScope outputOnlyProcess) ∧ Satisfiable (processScope explainedProcess)

Require both actual process-identity theories to be satisfiable.

L677/- Concrete evaluation and a faithful double-input certificate establish the two differently scoped contracts. -/

Document the intended scope of scopedApplicationEvidence. The corresponding declaration concerns: Supplies actual all-input output proofs and the doubling explanation program for the stronger contract. This comment is explanatory, not a proof premise.

L678theorem scopedApplicationEvidence : ScopedApplicationEvidence := by

State the checked result scopedApplicationEvidence. Supplies actual all-input output proofs and the doubling explanation program for the stronger contract. The following tactic block proves this explicit type.

L679  refine ⟨processGrounds _ _ outputCorrectByEvaluation, processGrounds _ _ ?_,

Construct output-only grounds by evaluation and reserve the explained process’s stronger contract proof.

L680    processScopeModels _,processScopeModels _,⟨_,(processScopeModels _ _).2 rfl⟩,

Provide exact process-identity scope equivalences and each process itself as a nonempty scope witness.

L681    ⟨_,(processScopeModels _ _).2 rfl⟩⟩

Provide exact process-identity scope equivalences and each process itself as a nonempty scope witness.

L682  exact ⟨fun _ => rfl,⟨.doubleInput,rfl,fun _ => rfl⟩⟩

For explainedProcess, prove every doubled output by reflexivity and supply doubleInput as an actual provided, extensionally faithful explanation program.

L683/- Universal output correctness does not entail the explanation-requiring contract for the same process. -/

Document the intended scope of outputNotExplanation. The corresponding declaration concerns: Proves output correctness with no attached explanation and includes the corresponding same-object Grounds/countermodel evidence. This comment is explanatory, not a proof premise.

L684theorem outputNotExplanation : OutputContract outputOnlyProcess ∧

State the checked result outputNotExplanation. Proves output correctness with no attached explanation and includes the corresponding same-object Grounds/countermodel evidence.

L685    ¬ ExplanationContract outputOnlyProcess ∧ OutputContractEvidence :=

Retain absence of this process’s explanation contract together with its scoped output evidence.

L686  ⟨outputCorrectByEvaluation, outputOnlyNoExplanation, outputContractEvidence⟩

Combine actual output correctness, the same process’s absence of an explanation, and its matched scoped output evidence.

L687/- Applications may use distinct contracts, and a faithful certificate can satisfy the stronger one. -/

Document the intended scope of applicationContractsDiffer. The corresponding declaration concerns: Shows output-only evidence fails the stronger contract, while the explained process satisfies both; both applications carry their own Grounds. This comment is explanatory, not a proof premise.

L688theorem applicationContractsDiffer :

State the checked result applicationContractsDiffer. Shows output-only evidence fails the stronger contract, while the explained process satisfies both; both applications carry their own Grounds.

L689    (OutputContract outputOnlyProcess ∧ ¬ (OutputContract outputOnlyProcess ∧ ExplanationContract outputOnlyProcess)) ∧

The output-only process meets output correctness but fails the combined output-and-explanation contract.

L690    (OutputContract explainedProcess ∧ ExplanationContract explainedProcess) ∧

The explained process meets both actual contracts.

L691    ScopedApplicationEvidence :=

Include the explicit scoped grounds and nonempty witnesses for both application contracts.

L692  ⟨⟨outputCorrectByEvaluation, fun h => outputOnlyNoExplanation h.2⟩,

For outputOnlyProcess, supply actual output correctness and refute any joint contract by projecting its impossible explanation component.

L693    ⟨(fun _ => rfl), ⟨.doubleInput, rfl, fun _ => rfl⟩⟩, scopedApplicationEvidence⟩

For explainedProcess, compute all doubled outputs, supply faithful doubleInput syntax, and include both contracts’ matched scoped grounds.

L694/- The assessor supplies a mathematical certificate; the process's own explanation response is unnecessary. -/

Document the intended scope of ExternalCertificate. The corresponding declaration concerns: Binds output-correctness proof to the exact process and distinct assessor/assessed identifiers; it is a mathematical role model, not authenticated real provenance. This comment is explanatory, not a proof premise.

L695structure ExternalCertificate (p : Process) where

Declare the data interface ExternalCertificate. Binds output-correctness proof to the exact process and distinct assessor/assessed identifiers; it is a mathematical role model, not authenticated real provenance.

L696  assessorId : Nat

Store the external assessor’s identifier.

L697  assessedId : Nat

Store the assessed participant’s identifier; the certificate type already fixes the assessed Process.

L698  distinctParticipants : assessorId ≠ assessedId

Require distinct participant identifiers as an explicit certificate field.

L699  outputCorrect : ∀ n, p.output n = n + n

Require a proof of this very process’s doubled output for every input; a generic certificate assumes this field, while the concrete certificate constructs it.

L700/- The external assessor 42 evaluates the specified process 7; the full output proof is constructed by evaluation. -/

Document the intended scope of externalOutputCertificate. The corresponding declaration concerns: Constructs assessor forty-two's proof for assessed object seven by actual output evaluation. This comment is explanatory, not a proof premise.

L701def externalOutputCertificate : ExternalCertificate outputOnlyProcess :=

Define externalOutputCertificate. Constructs assessor forty-two's proof for assessed object seven by actual output evaluation.

L702  ⟨42,7,by decide,fun _ => rfl⟩

Construct participants 42 and 7, compute their inequality, and prove every doubled output by reflexivity of the actual program.

L703/- An external certificate establishes the output contract without producing an internal explanation. -/

Document the intended scope of externalAssessment. The corresponding declaration concerns: Uses a distinct-participant certificate to supply matching output Grounds while the assessed process still returns no explanation. This comment is explanatory, not a proof premise.

L704theorem externalAssessment :

State the checked result externalAssessment. Uses a distinct-participant certificate to supply matching output Grounds while the assessed process still returns no explanation.

L705    (∃ certificate : ExternalCertificate outputOnlyProcess,

Require an actual external certificate indexed by outputOnlyProcess.

L706      certificate.assessorId = 42 ∧ certificate.assessedId = 7 ∧

Identify its assessor as 42 and assessed participant as 7.

L707      certificate.assessorId ≠ certificate.assessedId ∧ OutputContract outputOnlyProcess) ∧

Require their distinction and actual output correctness of the same process.

L708    ProcessGrounds outputOnlyProcess OutputContract ∧

Also retain matched ProcessGrounds for that same output contract.

L709    ¬ ExplanationContract outputOnlyProcess :=

Still deny an internal explanation contract for that actual process.

L710  ⟨⟨externalOutputCertificate,rfl,rfl,externalOutputCertificate.distinctParticipants,

Use the actual externalOutputCertificate with fixed participants 42 and 7 and its proved participant distinction.

L711    externalOutputCertificate.outputCorrect⟩,

Take universal output correctness from that concrete certificate, whose proof was constructed from the actual program.

L712    processGrounds outputOnlyProcess OutputContract externalOutputCertificate.outputCorrect,

Build matching ProcessGrounds for the very outputOnlyProcess using that same concrete output proof.

L713    outputOnlyNoExplanation⟩

Retain outputOnlyNoExplanation, so the external certificate does not assert an internal explanation exists.

L714/- This argument records concepts and actual premises for a semantic inference, separately from executable tests. -/

Document the intended scope of arithmeticArticulation. The corresponding declaration concerns: Names the canonical articulation of the arithmetic inferential facet. This comment is explanatory, not a proof premise.

L715def arithmeticArticulation : Articulation Nat := canonicalArticulation arithmeticFacet

Define arithmeticArticulation. Names the canonical articulation of the arithmetic inferential facet.

L716/- A reasoned inferential assessment needs no observation method, while applicable empirical assessment retains observations. -/

Document the intended scope of nonExecutableAssessment. The corresponding declaration concerns: Constructs Grounds for the arithmetic conditional facet and distinguishes its nonempirical tag from a discharged empirical switch facet. The tag does not establish noncomputability. This comment is explanatory, not a proof premise.

L717theorem nonExecutableAssessment :

State the checked result nonExecutableAssessment. Constructs Grounds for the arithmetic conditional facet and distinguishes its nonempirical tag from a discharged empirical switch facet. The tag does not establish noncomputability.

L718    Grounds (fun n : Nat => n + 1 = 3) canonicalArticulation (fun f => f = arithmeticFacet) [arithmeticFacet] ∧

Require matched canonical Grounds for n+1=3 using precisely arithmeticFacet.

L719    usesObservation arithmeticFacet = false ∧

Specify that this inferential facet uses no observation.

L720    FacetDischarged switchEmpirical ∧ usesObservation switchEmpirical = true := by

At the same time, include an actually discharged empirical facet that does use observation.

L721  refine ⟨⟨by simp, (by intro f hf; cases hf; simp), ?_⟩, rfl, switchEmpiricalDischarged, rfl⟩

Build the arithmetic claim’s nonempty, applicability-covered Grounds, retain its no-observation classification, and include the valid observed switch facet.

L722  intro f hf; simp only [List.mem_singleton] at hf; cases hf

Singleton membership fixes the assessed facet to arithmeticFacet, so its specific assumptions and conclusion must be checked.

L723  exact ⟨rfl, canonicalArticulated _ noUniversalChain.1, canonicalFacetArticulated _, noUniversalChain.1⟩

Use the same arithmetic facet’s proven discharge with canonical nonempty articulation and its exact semantic connection.

L725end CoreReader.Evidence

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