leanified/CoreReader/Logic.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 · 185 lines

LeanLine explanation

L1namespace CoreReader.Logic

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

L3/- A claim denotes the worlds in which its content holds. -/

Document the intended scope of Claim. The corresponding declaration concerns: A claim is a proposition-valued function on a supplied world type W; the world type is not restricted to a real-world interpretation. This comment is explanatory, not a proof premise.

L4abbrev Claim (W : Type) := W → Prop

Introduce the type abbreviation Claim. A claim is a proposition-valued function on a supplied world type W; the world type is not restricted to a real-world interpretation.

L5/- A theory is a collection of simultaneously held claims. -/

Document the intended scope of Theory. The corresponding declaration concerns: A theory is a predicate selecting claims, rather than a finite syntax or executable theory representation. This comment is explanatory, not a proof premise.

L6abbrev Theory (W : Type) := Claim W → Prop

Introduce the type abbreviation Theory. A theory is a predicate selecting claims, rather than a finite syntax or executable theory representation.

L7/- A model satisfies every member of the whole theory. -/

Document the intended scope of Models. The corresponding declaration concerns: A world models a theory exactly when every selected claim holds at that world. This comment is explanatory, not a proof premise.

L8def Models {W : Type} (t : Theory W) (w : W) : Prop := ∀ p, t p → p w

Define Models. A world models a theory exactly when every selected claim holds at that world.

L9/- Semantic entailment quantifies over all models. -/

Document the intended scope of Entails. The corresponding declaration concerns: Semantic entailment universally quantifies over worlds satisfying the theory. With no model it is vacuous. This comment is explanatory, not a proof premise.

L10def Entails {W : Type} (t : Theory W) (p : Claim W) : Prop := ∀ w, Models t w → p w

Define Entails. Semantic entailment universally quantifies over worlds satisfying the theory. With no model it is vacuous.

L11/- Satisfiability requires an actual witness. -/

Document the intended scope of Satisfiable. The corresponding declaration concerns: Satisfiability requires an actual witness world together with a proof that it models the theory. This comment is explanatory, not a proof premise.

L12def Satisfiable {W : Type} (t : Theory W) : Prop := ∃ w, Models t w

Define Satisfiable. Satisfiability requires an actual witness world together with a proof that it models the theory.

L13/- Assumptions, meanings and scope are distinct components; questions remain explicit. -/

Document the intended scope of Context. The corresponding declaration concerns: Packages contextual assumptions, question meanings, and a scope predicate; the interface does not validate these choices. This comment is explanatory, not a proof premise.

L14structure Context (W Q : Type) where

Declare the data interface Context. Packages contextual assumptions, question meanings, and a scope predicate; the interface does not validate these choices.

L15  assumptions : Theory W

Store the actual contextual assumption theory, separately from the held theory.

L16  meaning : Q → Claim W

Interpret each question as a proposition about each world.

L17  scope : Claim W

Store the predicate selecting the admitted application scope.

L18/- Admissible worlds satisfy held claims, assumptions and scope jointly. -/

Document the intended scope of Admissible. The corresponding declaration concerns: A world is admissible when the held theory, contextual assumptions, and scope all hold simultaneously. This comment is explanatory, not a proof premise.

L19def Admissible {W Q : Type} (t : Theory W) (c : Context W Q) (w : W) : Prop :=

Define Admissible. A world is admissible when the held theory, contextual assumptions, and scope all hold simultaneously.

L20  Models t w ∧ Models c.assumptions w ∧ c.scope w

Require this same world to model both theories and satisfy the contextual scope simultaneously.

L21/- A negative judgment denies the very same question under the same meaning. -/

Document the intended scope of Consequence. The corresponding declaration concerns: A signed consequence must hold in every admissible world: positive selects the question meaning and negative selects its negation. This comment is explanatory, not a proof premise.

L22def Consequence {W Q : Type} (t : Theory W) (c : Context W Q) (q : Q) (positive : Bool) : Prop :=

Define Consequence. A signed consequence must hold in every admissible world: positive selects the question meaning and negative selects its negation.

L23  ∀ w, Admissible t c w → if positive then c.meaning q w else ¬ c.meaning q w

Quantify over every admissible world; the sign selects either this question’s meaning or its negation.

L24/- The consistency obligation prohibits both consequences at one comparison basis. -/

Document the intended scope of Consistent. The corresponding declaration concerns: Consistency rules out simultaneously entailing a question and its negation for every question in Q. Empty Q makes this condition vacuous. This comment is explanatory, not a proof premise.

L25def Consistent {W Q : Type} (t : Theory W) (c : Context W Q) : Prop :=

Define Consistent. Consistency rules out simultaneously entailing a question and its negation for every question in Q. Empty Q makes this condition vacuous.

L26  ∀ q, ¬ (Consequence t c q true ∧ Consequence t c q false)

For every question, prohibit the conjunction of its positive and negative consequences in this same context.

L27/- An inhabited joint interpretation prevents opposite semantic consequences. -/

Document the intended scope of consequenceConsistency. The corresponding declaration concerns: Given an admissible witness, proves that no question can have both signed consequences. The witness is an explicit premise. This comment is explanatory, not a proof premise.

L28theorem consequenceConsistency {W Q : Type} (t : Theory W) (c : Context W Q)

State the checked result consequenceConsistency. Given an admissible witness, proves that no question can have both signed consequences. The witness is an explicit premise.

L29    (inhabited : ∃ w, Admissible t c w) : Consistent t c := by

Assume an admissible witness for the whole context and conclude its consistency; begin the proof.

L30  intro q h

Introduce an arbitrary question q and the hypothetical pair h of its positive and negative consequences in the same context.

L31  obtain ⟨w, hw⟩ := inhabited

Extract the common admissible world w and its entire theory/assumptions/scope proof hw from the explicit inhabited premise.

L32  exact (h.2 w hw) (h.1 w hw)

Evaluate both halves of h at the same w and hw; the negative consequence contradicts the positive consequence.

L33/- Empty and singleton theories provide concrete semantic contexts. -/

Document the intended scope of emptyTheory. The corresponding declaration concerns: Selects no claims, so every world models this theory. This comment is explanatory, not a proof premise.

L34def emptyTheory {W : Type} : Theory W := fun _ => False

Define emptyTheory. Selects no claims, so every world models this theory.

L35def singleton {W : Type} (p : Claim W) : Theory W := fun q => q = p

Define singleton. Selects exactly the claim equal to p; this uses equality of predicate functions.

L36def union {W : Type} (a b : Theory W) : Theory W := fun p => a p ∨ b p

Define union. Combines two sets of claims by disjunction of membership.

L37theorem modelsSingleton {W : Type} (p : Claim W) (w : W) : Models (singleton p) w ↔ p w := by

State the checked result modelsSingleton. Proves that modeling the singleton theory is equivalent to satisfying its sole claim. The following tactic block proves this explicit type.

L38  constructor

Split the equivalence between satisfying the singleton theory and satisfying its sole claim into two implications.

L39  · intro h; exact h p rfl

Use the assumed singleton model h on p, whose membership follows from reflexive equality.

L40  · intro h q hq; cases hq; exact h

For any selected claim q, singleton membership identifies q with p; substitute that identity and return the assumed truth h of p.

L41theorem modelsUnion {W : Type} (a b : Theory W) (w : W) :

State the checked result modelsUnion. Proves that modeling the union is equivalent to modeling both constituent theories at the same world.

L42    Models (union a b) w ↔ Models a w ∧ Models b w := by

State that the same world models the theory union exactly when it models both constituent theories.

L43  constructor

Prove the model-of-union equivalence in its forward and reverse directions.

L44  · intro h; exact ⟨fun p hp => h p (Or.inl hp), fun p hp => h p (Or.inr hp)⟩

Restrict the union model h to each theory by embedding its membership proof into the left or right disjunct.

L45  · rintro ⟨ha,hb⟩ p (hp|hp); exact ha p hp; exact hb p hp

Unpack both constituent models, split a union membership into its two alternatives, and use the corresponding model on the same claim and world.

L46/- The paired world records independent truth values for two questions. -/

Document the intended scope of premiseP. The corresponding declaration concerns: Reads the first Boolean coordinate as true. This comment is explanatory, not a proof premise.

L47def premiseP : Claim (Bool × Bool) := fun w => w.1 = true

Define premiseP. Reads the first Boolean coordinate as true.

L48def premiseRule : Claim (Bool × Bool) := fun w => w.1 = true → w.2 = true

Define premiseRule. Makes truth of the first Boolean imply truth of the second.

L49def premiseNotQ : Claim (Bool × Bool) := fun w => w.2 ≠ true

Define premiseNotQ. Requires the second Boolean not to be true.

L50def jointTheory : Theory (Bool × Bool) :=

Define jointTheory. Combines the first-coordinate fact, the implication, and the negated second-coordinate fact.

L51  union (singleton premiseP) (union (singleton premiseRule) (singleton premiseNotQ))

Hold P, the rule P implies Q, and not Q together through nested theory unions.

L52/- Each premise has a model, but their joint implication makes the union unsatisfiable. -/

Document the intended scope of jointConflict. The corresponding declaration concerns: Exhibits individual models of each of three claims, then proves their conjunction has no model. This comment is explanatory, not a proof premise.

L53theorem jointConflict :

State the checked result jointConflict. Exhibits individual models of each of three claims, then proves their conjunction has no model.

L54    Satisfiable (singleton premiseP) ∧ Satisfiable (singleton premiseRule) ∧

The first two conclusions provide separate models for P and its implication rule.

L55    Satisfiable (singleton premiseNotQ) ∧ ¬ Satisfiable jointTheory := by

Also require a separate model for not Q, but deny any model of the entire joint theory.

L56  refine ⟨⟨(true,true), (modelsSingleton _ _).2 rfl⟩,

Supply (true,true) as the model of P, using modelsSingleton to turn its first-coordinate equality into the required model proof.

L57    ⟨(false,false), (modelsSingleton _ _).2 (by intro h; cases h)⟩,

Supply (false,false) for the implication premise: assuming its false first coordinate is true is impossible.

L58    ⟨(false,false), (modelsSingleton _ _).2 (by intro h; cases h)⟩, ?_⟩

Supply (false,false) for not Q and leave the joint unsatisfiability branch to be proved.

L59  rintro ⟨w, hw⟩

Assume a joint model w with proof hw in order to refute its existence.

L60  have hp := hw premiseP (Or.inl rfl)

Extract the actual first-coordinate fact P from its left membership in the joint theory.

L61  have hr := hw premiseRule (Or.inr (Or.inl rfl))

Extract P implies Q from the nested union membership of the rule.

L62  have hn := hw premiseNotQ (Or.inr (Or.inr rfl))

Extract not Q from the other nested union branch at the same world.

L63  exact hn (hr hp)

Apply the rule to P to derive Q and contradict the extracted not Q.

L64/- A retraction replaces the old singleton, rather than retaining both at the same time. -/

Document the intended scope of revisionSlice. The corresponding declaration concerns: At time zero requires a true world; at every other natural time requires a false world. This comment is explanatory, not a proof premise.

L65def revisionSlice (time : Nat) : Theory Bool :=

Define revisionSlice. At time zero requires a true world; at every other natural time requires a false world.

L66  singleton (fun w => w = (time == 0))

Select the single claim that the world equals the Boolean result of testing time=0.

L67/- The initial and revised slices have models; keeping both would create a conflict. -/

Document the intended scope of revisionCanReverse. The corresponding declaration concerns: Exhibits satisfiable time-zero and time-one slices whose union is unsatisfiable. No temporal update mechanism is implemented. This comment is explanatory, not a proof premise.

L68theorem revisionCanReverse :

State the checked result revisionCanReverse. Exhibits satisfiable time-zero and time-one slices whose union is unsatisfiable. No temporal update mechanism is implemented.

L69    Satisfiable (revisionSlice 0) ∧ Satisfiable (revisionSlice 1) ∧

Require time slices 0 and 1 to have separate model witnesses.

L70    ¬ Satisfiable (union (revisionSlice 0) (revisionSlice 1)) := by

Deny a model of their simultaneous union; this does not deny either separate witness.

L71  refine ⟨⟨true, (modelsSingleton _ _).2 rfl⟩,

Give true as the witness for the time-zero singleton theory.

L72    ⟨false, (modelsSingleton _ _).2 rfl⟩, ?_⟩

Give false as the witness for time one, and leave the impossibility of holding both slices together.

L73  rintro ⟨w, hw⟩

Assume a world satisfies both time slices simultaneously.

L74  have hs := (modelsUnion _ _ _).1 hw

Split this union model into models of the time-zero and time-one theories at the same world.

L75  have hp := (modelsSingleton _ _).1 hs.1

Extract that the common world equals true from the time-zero singleton.

L76  have hn := (modelsSingleton _ _).1 hs.2

Extract that the same world equals false from the time-one singleton.

L77  have bad : true = false := hp.symm.trans hn

Compose the two equalities through the same world to derive the impossible equality true = false.

L78  cases bad

Eliminate the impossible equality between distinct Boolean constructors.

L79/- This basic question asks whether the represented switch is on. -/

Document the intended scope of onQuestion. The corresponding declaration concerns: The sole Unit question asks whether the Boolean world is true. This comment is explanatory, not a proof premise.

L80def onQuestion : Unit → Claim Bool := fun _ w => w = true

Define onQuestion. The sole Unit question asks whether the Boolean world is true.

L81def assumptionContext (b : Bool) : Context Bool Unit :=

Define assumptionContext. Varies the assumption selecting the world while fixing its question meaning and unrestricted scope.

L82  ⟨singleton (fun w => w = b), onQuestion, fun _ => True⟩

Select world b through assumptions, retain the same on-question, and allow every world in scope.

L83def meaningContext (b : Bool) : Context Bool Unit :=

Define meaningContext. Fixes the world assumption to true but varies whether the question means equality to true or false.

L84  ⟨singleton (fun w => w = true), (fun _ w => w = b), fun _ => True⟩

Keep the true-world assumption while changing the question to equality with b; scope remains unrestricted.

L85def scopeContext (b : Bool) : Context Bool Unit :=

Define scopeContext. Keeps assumptions empty and the question fixed while selecting the world through scope.

L86  ⟨emptyTheory, onQuestion, fun w => w = b⟩

Leave assumptions empty and the question fixed, but let scope select world b.

L87/- Distinct assumptions, meanings and scopes each admit opposite judgments without same-context conflict. -/

Document the intended scope of contextDifferences. The corresponding declaration concerns: Proves that changing any one of assumptions, meaning, or scope can reverse polarity, with explicit admissible witnesses in all displayed contexts. This comment is explanatory, not a proof premise.

L88theorem contextDifferences :

State the checked result contextDifferences. Proves that changing any one of assumptions, meaning, or scope can reverse polarity, with explicit admissible witnesses in all displayed contexts.

L89    (Consequence emptyTheory (assumptionContext true) () true ∧

Require a positive answer under true-valued assumptions.

L90      Consequence emptyTheory (assumptionContext false) () false) ∧

Require the negative answer under false-valued assumptions; the contexts differ.

L91    (Consequence emptyTheory (meaningContext true) () true ∧

Require a positive answer for the question meaning equality to true.

L92      Consequence emptyTheory (meaningContext false) () false) ∧

Require the negative answer when that question instead means equality to false.

L93    (Consequence emptyTheory (scopeContext true) () true ∧

Require the positive answer in the scope restricted to true.

L94      Consequence emptyTheory (scopeContext false) () false) ∧

Require the negative answer in the different scope restricted to false.

L95    (∀ b, ∃ w, Admissible emptyTheory (assumptionContext b) w) ∧

For either assumption selector, require an actual admissible world.

L96    (∀ b, ∃ w, Admissible emptyTheory (meaningContext b) w) ∧

For either question meaning, require an actual admissible world.

L97    (∀ b, ∃ w, Admissible emptyTheory (scopeContext b) w) := by

For either scope selector, require an actual admissible world and begin the combined proof.

L98  have empty : ∀ w : Bool, Models emptyTheory w := by intro w p hp; cases hp

Show every Boolean world satisfies emptyTheory because membership in that theory is False.

L99  refine ⟨⟨?_, ?_⟩, ⟨?_, ?_⟩, ⟨?_, ?_⟩, ?_, ?_, ?_⟩

Separate the positive/negative answer pairs for changed assumptions, meaning and scope, then the three nonempty-context witness obligations.

L100  · intro w h; change w = true; exact (modelsSingleton (fun x : Bool => x = true) w).1 h.2.1

For the true-assumption context, read w = true from the contextual singleton assumptions.

L101  · intro w h hp; have hn := (modelsSingleton _ _).1 h.2.1; cases hp.symm.trans hn

For the false-assumption context, a proposed positive answer contradicts the singleton assumption w = false.

L102  · intro w h; change w = true; exact (modelsSingleton (fun x : Bool => x = true) w).1 h.2.1

For the true meaning of the question, use the fixed true-world assumption to establish the positive answer.

L103  · intro w h hn; have hp := (modelsSingleton _ _).1 h.2.1; cases hp.symm.trans hn

For the changed false meaning, its proposed truth conflicts with the unchanged true-world assumption.

L104  · intro w h; exact h.2.2

In the true-scope context, the scope component itself states the required positive answer.

L105  · intro w h hp; cases hp.symm.trans h.2.2

In the false-scope context, a positive answer contradicts the scope component at the same world.

L106  · intro b; exact ⟨b, empty b, (modelsSingleton _ _).2 rfl, trivial⟩

For either chosen assumption b, witness world b satisfies the empty held theory, that singleton assumption and unrestricted scope.

L107  · intro b; exact ⟨true, empty true, (modelsSingleton _ _).2 rfl, trivial⟩

For either question meaning b, true remains a witness because the assumptions are fixed to true and scope is unrestricted.

L108  · intro b; exact ⟨b, empty b, empty b, rfl⟩

For either scope selector b, world b satisfies both empty theories and the selected scope by equality.

L109/- Snapshots preserve identifiable adopted-form revisions even when semantic content agrees. -/

Document the intended scope of Snapshot. The corresponding declaration concerns: Packages held claims, context and a natural-number revision identity; there is no history validation. This comment is explanatory, not a proof premise.

L110structure Snapshot (W Q : Type) where

Declare the data interface Snapshot. Packages held claims, context and a natural-number revision identity; there is no history validation.

L111  held : Theory W

Store the theory of simultaneously held claims in the snapshot.

L112  context : Context W Q

Store the snapshot’s assumptions, question meanings and scope as one Context.

L113  revisionIdentity : Nat

Store a separate natural-number revision identifier; no history validation is implied.

L114/- Semantic equivalence compares represented content, not its list ordering. -/

Document the intended scope of SameContent. The corresponding declaration concerns: Defines sameness using claim-membership equivalence, contextual-assumption membership equivalence, pointwise meaning equivalence, and pointwise scope equivalence. This comment is explanatory, not a proof premise.

L115def SameContent {W Q : Type} (a b : Snapshot W Q) : Prop :=

Define SameContent. Defines sameness using claim-membership equivalence, contextual-assumption membership equivalence, pointwise meaning equivalence, and pointwise scope equivalence.

L116  (∀ p, a.held p ↔ b.held p) ∧

Require identical held-claim membership for every claim in both snapshots.

L117  (∀ p, a.context.assumptions p ↔ b.context.assumptions p) ∧

Require identical membership for every contextual assumption.

L118  (∀ q w, a.context.meaning q w ↔ b.context.meaning q w) ∧

Require equivalent question meanings for every question at every world.

L119  (∀ w, a.context.scope w ↔ b.context.scope w)

Require equivalent scope predicates at every world.

L120/- The reporting norm covers both semantic change and independently identified revisions. -/

Document the intended scope of TruthfulReport. The corresponding declaration concerns: Requires a true report if semantic content or revision identity differs. It allows a true report when neither differs and implements no detector. This comment is explanatory, not a proof premise.

L121def TruthfulReport {W Q : Type} (a b : Snapshot W Q) (reported : Bool) : Prop :=

Define TruthfulReport. Requires a true report if semantic content or revision identity differs. It allows a true report when neither differs and implements no detector.

L122  (¬ SameContent a b ∨ a.revisionIdentity ≠ b.revisionIdentity) → reported = true

Define truthful reporting as a positive flag whenever content differs or the independent revision identifiers differ.

L123/- A real represented change and compliance entail an acknowledged change. -/

Document the intended scope of semanticChangeMustBeReported. The corresponding declaration concerns: Instantiates the reporting interface with a supplied change proof; it cannot discover changes on its own. This comment is explanatory, not a proof premise.

L124theorem semanticChangeMustBeReported {W Q : Type} (a b : Snapshot W Q) (reported : Bool)

State the checked result semanticChangeMustBeReported. Instantiates the reporting interface with a supplied change proof; it cannot discover changes on its own.

L125    (changed : ¬ SameContent a b ∨ a.revisionIdentity ≠ b.revisionIdentity)

Assume an actual change: either content differs or the revision identifiers differ.

L126    (h : TruthfulReport a b reported) : reported = true := h changed

Assume the reporting obligation and apply it to the preceding change premise to obtain reported=true.

L127/- Reordering a two-claim presentation preserves the held theory extension. -/

Document the intended scope of representationOrderIrrelevant. The corresponding declaration concerns: Proves swapping the order of two singleton components leaves theory membership unchanged. This comment is explanatory, not a proof premise.

L128theorem representationOrderIrrelevant {W : Type} (p q : Claim W) :

State the checked result representationOrderIrrelevant. Proves swapping the order of two singleton components leaves theory membership unchanged.

L129    ∀ r, union (singleton p) (singleton q) r ↔ union (singleton q) (singleton p) r := by

For any claim r, swapping p and q preserves membership in their singleton-theory union.

L130  intro r; exact or_comm

For an arbitrary candidate claim r, use commutativity of disjunction to preserve union membership after reordering p and q.

L131def contextSnapshot (c : Context Bool Unit) (revision : Nat := 0) : Snapshot Bool Unit :=

Define contextSnapshot. Wraps a Boolean/Unit context in a snapshot with empty held theory and a default revision of zero.

L132  ⟨emptyTheory, c, revision⟩

Construct a snapshot with no held claims, the supplied context, and the supplied revision identifier.

L133/- Hiding each kind of contextual change violates the reporting interface; reporting alone supplies no truth guarantee. -/

Document the intended scope of hiddenContextChangeRejected. The corresponding declaration concerns: Rejects false reports for three concrete context changes and a revision-only change; also shows reporting true does not make an incompatible assumption hold. This comment is explanatory, not a proof premise.

L134theorem hiddenContextChangeRejected :

State the checked result hiddenContextChangeRejected. Rejects false reports for three concrete context changes and a revision-only change; also shows reporting true does not make an incompatible assumption hold.

L135    ¬ TruthfulReport (contextSnapshot (assumptionContext true)) (contextSnapshot (assumptionContext false)) false ∧

Reject a false report when actual contextual assumptions change from true to false.

L136    ¬ TruthfulReport (contextSnapshot (meaningContext true)) (contextSnapshot (meaningContext false)) false ∧

Reject a false report when the question’s actual meaning changes.

L137    ¬ TruthfulReport (contextSnapshot (scopeContext true)) (contextSnapshot (scopeContext false)) false ∧

Reject a false report when the actual application scope changes.

L138    ¬ TruthfulReport (contextSnapshot (scopeContext true) 0) (contextSnapshot (scopeContext true) 1) false ∧

Reject a false report when revision identity changes from 0 to 1 despite unchanged context.

L139    (TruthfulReport (contextSnapshot (assumptionContext true)) (contextSnapshot (assumptionContext false)) true ∧

Permit truthful acknowledgement of the changed assumptions with a true report.

L140      ¬ Models (assumptionContext false).assumptions true) := by

Nevertheless deny that those revised false-world assumptions hold at actual true.

L141  have neq : (fun w : Bool => w = true) ≠ (fun w : Bool => w = false) := by

Prepare a semantic inequality: the predicates selecting true and selecting false are distinct functions.

L142    intro h; have k := congrFun h true; have z : true = false := k.mp rfl; cases z

Evaluate any alleged predicate equality at true; it would turn reflexive truth into true = false.

L143  refine ⟨?_, ?_, ?_, ?_, ?_⟩

Split the four rejected hidden changes from the final acknowledged-but-false-assumption example.

L144  · intro h

Assume the hidden assumption change with report=false satisfied TruthfulReport, in order to refute that claim.

L145    have bad := h (Or.inl (by intro s; exact neq ((s.2.1 _).mp rfl)))

A claimed SameContent would equate the changed assumption predicates; their established inequality activates TruthfulReport and forces the false flag to be true.

L146    cases bad

Close this hidden-change branch because the required true report contradicts the specified false flag.

L147  · intro h

Assume the changed question meaning could be truthfully reported as unchanged.

L148    have bad := h (Or.inl (by intro s; have z := (s.2.2.1 () true).mp rfl; cases z))

At the sole question and world true, the changed meaning contradicts SameContent; the reporting obligation then forces a positive report.

L149    cases bad

Close this hidden-change branch because the required true report contradicts the specified false flag.

L150  · intro h

Assume the changed application scope could satisfy the reporting rule with a false change flag.

L151    have bad := h (Or.inl (by intro s; have z := (s.2.2.2 true).mp rfl; cases z))

Compare the two scopes at true to refute SameContent, then apply the reporting obligation to this real scope change.

L152    cases bad

Close this hidden-change branch because the required true report contradicts the specified false flag.

L153  · intro h; have bad := h (Or.inr (by decide)); cases bad

The distinct revision identities alone activate the reporting rule, contradicting the false report even without a content change.

L154  · refine ⟨fun _ => rfl, ?_⟩

Construct an always-positive truthful report, while leaving the separate truth of the revised assumption to be refuted.

L155    intro h; have z := (modelsSingleton _ _).1 h; cases z

Extract the revised false-world assumption at actual true; its impossible equality shows acknowledgement did not make it true.

L156/- Two nonidentical resource objectives can share a feasible allocation. -/

Document the intended scope of tensionWithoutContradiction. The corresponding declaration concerns: Exhibits overlapping lower/upper budget bounds while proving that the two predicates differ. This is a concrete compatible-constraints example. This comment is explanatory, not a proof premise.

L157theorem tensionWithoutContradiction :

State the checked result tensionWithoutContradiction. Exhibits overlapping lower/upper budget bounds while proving that the two predicates differ. This is a concrete compatible-constraints example.

L158    (∃ budget : Nat, 4 ≤ budget ∧ budget ≤ 6) ∧

Ask for a natural-number budget satisfying both lower bound 4 and upper bound 6.

L159    ¬ ((fun n : Nat => 4 ≤ n) = (fun n : Nat => n ≤ 6)) := by

Also assert that the two bound predicates are not identical, even though jointly satisfiable.

L160  refine ⟨⟨5, by decide, by decide⟩, ?_⟩

Choose budget 5, check both numeric bounds, and leave the inequality of the two objective predicates.

L161  intro h; have k := congrFun h 0; have bad : 4 ≤ 0 := k.mpr (by decide); cases bad

At budget 0, the upper bound holds but the lower bound cannot; therefore the objective predicates cannot be equal.

L162/- Conflicting conclusions cannot be retained under the same consistency obligation. -/

Document the intended scope of conflictRequiresChange. The corresponding declaration concerns: Given both signed consequences for one question, proves inconsistency as defined. It does not construct a repair or establish which premise should change. This comment is explanatory, not a proof premise.

L163theorem conflictRequiresChange {W Q : Type} (t : Theory W) (c : Context W Q) (q : Q)

State the checked result conflictRequiresChange. Given both signed consequences for one question, proves inconsistency as defined. It does not construct a repair or establish which premise should change.

L164    (positive : Consequence t c q true) (negative : Consequence t c q false) :

Assume both opposed consequences for exactly the same theory, context and question.

L165    ¬ Consistent t c := fun h => h q ⟨positive,negative⟩

Any Consistent proof would forbid that given pair; apply it to refute consistency, without constructing a revision.

L166/- A satisfiable theory can have a false assumption at a specified actual world. -/

Document the intended scope of consistentFalse. The corresponding declaration concerns: Exhibits a satisfiable Boolean singleton theory that fails at the separately chosen world false; satisfiability is not truth at every world. This comment is explanatory, not a proof premise.

L167theorem consistentFalse : Satisfiable (singleton (fun w : Bool => w = true)) ∧

State the checked result consistentFalse. Exhibits a satisfiable Boolean singleton theory that fails at the separately chosen world false; satisfiability is not truth at every world.

L168    ¬ Models (singleton (fun w : Bool => w = true)) false := by

Deny that actual false models the theory whose sole claim is world=true.

L169  refine ⟨⟨true, (modelsSingleton _ _).2 rfl⟩, ?_⟩

Provide true as a model of the singleton theory and separately refute modeling it at actual false.

L170  intro h; have bad := (modelsSingleton _ _).1 h; cases bad

Singleton modeling at false would force false = true, an impossible Boolean equality.

L171/- The explicitly asked on/off question is undecided by the empty but inhabited theory. -/

Document the intended scope of consistentIncomplete. The corresponding declaration concerns: Shows the empty Boolean theory is satisfiable while entailing neither the true-world claim nor its negation. This comment is explanatory, not a proof premise.

L172theorem consistentIncomplete : Satisfiable (emptyTheory : Theory Bool) ∧

State the checked result consistentIncomplete. Shows the empty Boolean theory is satisfiable while entailing neither the true-world claim nor its negation.

L173    ¬ Entails emptyTheory (fun w : Bool => w = true) ∧

The inhabited empty theory does not entail the positive true-world answer.

L174    ¬ Entails emptyTheory (fun w : Bool => w ≠ true) := by

It also does not entail the negative true-world answer; prove these two failures separately.

L175  have empty : ∀ w : Bool, Models emptyTheory w := by intro w p hp; cases hp

Show every Boolean world satisfies emptyTheory because membership in that theory is False.

L176  refine ⟨⟨true, empty true⟩, ?_, ?_⟩

Provide an inhabited empty theory and leave both positive and negative entailments to be refuted.

L177  · intro h; have bad := h false (empty false); cases bad

A purported entailment of world=true fails at the empty theory model false.

L178  · intro h; exact h true (empty true) rfl

A purported entailment of world≠true fails at the empty theory model true.

L179/- A claim can share a model with a theory without following in every model. -/

Document the intended scope of compatibilityNotEntailment. The corresponding declaration concerns: Shows that adding a claim can remain satisfiable even though the original empty theory did not entail that claim. This comment is explanatory, not a proof premise.

L180theorem compatibilityNotEntailment :

State the checked result compatibilityNotEntailment. Shows that adding a claim can remain satisfiable even though the original empty theory did not entail that claim.

L181    Satisfiable (union emptyTheory (singleton (fun w : Bool => w = true))) ∧

Require a model where emptyTheory and the positive singleton claim hold together.

L182    ¬ Entails emptyTheory (fun w : Bool => w = true) := by

Still deny that emptyTheory by itself entails that positive claim.

L183  refine ⟨⟨true, (modelsUnion _ _ _).2 ⟨?_, (modelsSingleton _ _).2 rfl⟩⟩,

Use world true to witness compatibility of the empty theory with the positive singleton claim.

L184    consistentIncomplete.2.1⟩

Reuse the previously proved failure of positive entailment from the empty theory.

L185  intro p hp; cases hp

Finish the model witness: no claim can actually belong to emptyTheory.

L187end CoreReader.Logic

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