leanified/CoreReader/Integration.lean

Back to claims · Declarations and proofs

Philosophy 0.1.4 · considered Core 0.1.4. This view uses the repository’s public target catalog, readers and Lean files. Presentation does not change their judgments.

Expand Lean and line explanations · 522 lines

LeanLine explanation

L1import CoreReader.Agency

Imports CoreReader.Agency and its dependencies into this module.

L2import CoreReader.Choice

Imports CoreReader.Choice and its dependencies into this module.

L4namespace CoreReader.Integration

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

L5open CoreReader.Logic CoreReader.Evidence CoreReader.Agency CoreReader.Choice

Makes the listed namespaces available for unqualified references.

L7/- Canonical articulation preserves the actual assessment contents of each facet. -/

Documents the following definition or result: Builds Grounds from a nonempty list of discharged facets all targeting one claim, using canonical articulations and list membership itself as applicability.

L8theorem canonicalGrounds {W : Type} (claim : Claim W) (facets : List (Facet W))

Builds Grounds from a nonempty list of discharged facets all targeting one claim, using canonical articulations and list membership itself as applicability.

L9    (hne : facets ≠ []) (checked : ∀ f ∈ facets, f.claim = claim ∧ FacetDischarged f) :

Assumes a nonempty facet list, with each facet targeting claim and already discharged.

L10    Grounds claim canonicalArticulation (fun f => f ∈ facets) facets := by

Builds Grounds using each facet's own constructed articulation and list membership as the applicability predicate.

L11  exact ⟨hne, fun _ h => h, fun f hf =>

Supplies nonemptiness and tautological membership coverage, then checks each listed facet.

L12    ⟨(checked f hf).1, canonicalArticulated f (checked f hf).2,

For each facet, uses checked to establish the same claim and derive a nonempty articulation from its discharge.

L13      canonicalFacetArticulated f, (checked f hf).2⟩⟩

Adds that articulation's exact content correspondence and the supplied discharge proof.

L15theorem canonicalGroundsForSingleton {W : Type} (f : Facet W) (checked : FacetDischarged f) :

Builds Grounds for one discharged facet with applicability exactly equality to that facet.

L16    Grounds f.claim canonicalArticulation (fun g => g = f) [f] := by

For a single discharged facet, makes exactly that facet applicable to its own claim.

L17  refine ⟨by simp, (by intro g hg; cases hg; simp), ?_⟩

Proves the singleton is nonempty and every facet equal to f occurs in it; leaves per-facet content checks.

L18  intro g hg

Takes any facet g known to belong to the singleton list [f].

L19  simp only [List.mem_singleton] at hg

Singleton membership turns hg into the equality g=f.

L20  subst g

Replaces g by the same discharged facet f.

L21  exact ⟨rfl, canonicalArticulated f checked, canonicalFacetArticulated f, checked⟩

Uses identical claim, constructed articulability, exact facet-content match and checked discharge to finish its Grounds fields.

L23/- A mode selects whether a system applies or waives the modeled governance rule. -/

Documents the following definition or result: Separates applying the modeled standards from waiving them; the two modes drive actual policy decisions.

L24inductive Mode | apply | waive

Separates applying the modeled standards from waiving them; the two modes drive actual policy decisions.

L25  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L27/- The four hypotheses vary algorithm and governance independently for the same assessed system. -/

Documents the following definition or result: A world pairs one of two candidate implementations with one of two governance modes; it is a closed four-world model.

L28abbrev World := Candidate × Mode

A world pairs one of two candidate implementations with one of two governance modes; it is a closed four-world model.

L30def actual : World := (.identity, .apply)

Chooses identity implementation under applying governance as the concrete actual world.

L32/- A method's form and its possible executable realizations belong to one object. -/

Documents the following definition or result: Binds a revisable form identity to a world-dependent implementation.

L33structure Method where

Binds a method form kind/version to its world-dependent implementation; this structure alone does not prove the form is revisable.

L34  form : Form

Stores the form kind and version of this method.

L35  realize : World → Implementation

Assigns an actual implementation to every candidate/governance world for this same method.

L37/- System fields identify the owner, its method, its current principle form, policy and work. -/

Documents the following definition or result: Binds owner, method, principle form, governance selection and application requirements.

L38structure System where

Binds owner, method, principle form, governance selection and application requirements.

L39  owner : Nat

Identifies the owner whose principles and work are used for this system.

L40  method : Method

Stores the system's method form together with its world-dependent implementation.

L41  principleForm : Form

Stores the current form of the system's own principle.

L42  governance : World → Mode

Selects whether this system applies or waives governance in each world.

L43  requirements : Requirements

Fixes the actual input, output, budget and value requirements used to assess this system's implementation.

L45def policyFor : Mode → Policy

Applying governance selects the open policy; waiving selects the policy without expansion valuation.

L46  | .apply => openPolicy

Applying governance selects openPolicy, which values expansion and permits revision.

L47  | .waive => neutralPolicy

Waiving governance selects neutralPolicy, which lacks the required expansion valuation.

L49def workFor (owner : Nat) : Mode → List WorkRecord

Applying governance supplies content-checked own-work records; waiving supplies none.

L50  | .apply => completeOwnWork owner

Applying governance gives this owner the complete contentful work log.

L51  | .waive => []

Waiving governance gives the same owner an empty work log.

L53def System.policy (s : System) (w : World) : Policy := policyFor (s.governance w)

Uses this same system's governance choice to select its policy.

L54def System.rules (s : System) (_w : World) : List Principle := ownRules s.owner

Uses the registered generation/assessment rules for this system's owner.

L55def System.work (s : System) (w : World) : List WorkRecord := workFor s.owner (s.governance w)

Uses this owner's governance mode to select the actual work-record list.

L57def actualSystem : System where

Constructs owner zero with version-zero method/principle forms, candidate-dependent implementation, world-selected governance and identity requirements.

L58  owner := 0

Assigns owner zero to the shared actual system.

L59  method := ⟨⟨.method, 0⟩, fun w => implementation w.1⟩

Uses a version-zero method form whose realization is selected by the world's candidate component.

L60  principleForm := ⟨.principle, 0⟩

Sets this system's current principle form to principle version zero.

L61  governance := Prod.snd

Reads governance from the world's second component, independently of the implementation candidate.

L62  requirements := identityRequirements

Assesses the same method against identityRequirements.

L64def systemCapability (s : System) : Claim World :=

For this system's requested inputs, requires its realized method to match its own expected output.

L65  fun w => ∀ n, s.requirements.inputs n → (s.method.realize w).run n = s.requirements.expected n

Claims that this system's realized method meets its specified output on every required input.

L67def systemBudget (s : System) : Claim World :=

Checks the same realized implementation's cost against the system's budget.

L68  fun w => (s.method.realize w).cost ≤ s.requirements.budget

Claims that the same realized method's cost fits this system's own budget.

L70def systemObservation (s : System) : Record World :=

Records whether the system's actual implementation meets its expected output at input zero.

L71  ⟨fun w => decide ((s.method.realize w).run 0 = s.requirements.expected 0), true⟩

Records true for the test that this same method's output at zero equals its required output there.

L73def systemHeld (s : System) : Theory World :=

Holds this same system's capability and budget claims together.

L74  union (singleton (systemCapability s)) (singleton (systemBudget s))

The system simultaneously holds its actual output-capability claim and its budget claim.

L76inductive Question | correctOutput | affordable

Defines the output-correctness and affordability questions used by the context.

L77  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L79def systemContext (s : System) : Context World Question :=

Uses the same system's observation as assumption and its capability/budget as meanings; scope requires domain membership at zero and applying governance.

L80  ⟨singleton (Compatible [systemObservation s]),

The context assumes compatibility with this system's actual zero-input observation.

L81    (fun q => match q with | .correctOutput => systemCapability s | .affordable => systemBudget s),

Interprets correctOutput as this system's capability and affordable as its budget compliance.

L82    fun w => (s.method.realize w).domain 0 ∧ w.2 = .apply⟩

Restricts admissible scope to implementations whose domain includes zero and worlds with governance applied.

L84abbrev capability := systemCapability actualSystem

Abbreviates the actual system's parameterized output capability claim.

L85abbrev observation := systemObservation actualSystem

Abbreviates the actual system's input-zero observation record.

L86abbrev held := systemHeld actualSystem

Abbreviates the actual system's simultaneously held capability/budget theory.

L87abbrev context := systemContext actualSystem

Abbreviates the actual system's question/assumption/scope context.

L89/- The output observation identifies the algorithm, without identifying its independently varied governance mode. -/

Documents the following definition or result: Computes that the zero observation identifies the identity candidate while leaving governance mode unconstrained.

L90theorem observationIdentifies (w : World) : Compatible [observation] w ↔ w.1 = .identity := by

Computes that the zero observation identifies the identity candidate while leaving governance mode unconstrained.

L91  rcases w with ⟨candidate, mode⟩

Separates the candidate algorithm from the independently varied governance mode.

L92  cases candidate <;> simp [Compatible, observation, systemObservation, actualSystem,

Checks each of the two actual candidates against the observation's true zero-output test.

L93    implementation, identityRequirements, identityImpl, successorImpl]

Identity returns required zero while successor returns one, so only identity matches, regardless of governance.

L95theorem capabilityActual : capability actual := fun _ _ => rfl

Proves the actual identity implementation meets every requested identity output by reduction.

L97theorem observedCapability : Supports [observation] capability := by

Uses candidate identification and known identity behavior to obtain universal requested-input capability within the closed model.

L98  intro w hw

Takes an arbitrary world compatible with the same observation.

L99  have hid := (observationIdentifies w).1 hw

Uses observationIdentifies to infer that this world's algorithm candidate is identity.

L100  rcases w with ⟨candidate, mode⟩

Separates the world's algorithm and governance components for substitution.

L101  change candidate = .identity at hid

Restates the inferred identity equality directly on the candidate variable.

L102  subst candidate

Replaces the candidate algorithm with identity while retaining its governance mode.

L103  exact fun _ _ => rfl

Identity's run equals the required output at every input by definition, proving capability in this world.

L105def capabilityFacet : Facet World := .empirical [observation] (fun _ => True) capability (fun _ => True)

Packages the actual observation and capability claim in an empirical facet with unrestricted scope and trivial uncertainty.

L107theorem capabilityFacetChecked : FacetDischarged capabilityFacet := by

Supplies an actual compatible witness, the closed-model support proof and trivial uncertainty.

L108  exact ⟨⟨actual, (observationIdentifies actual).2 rfl, trivial⟩,

Supplies actual as a compatible world in the facet's unrestricted scope, avoiding an empty-world discharge.

L109    (fun w hw _ => observedCapability w hw), fun _ _ => trivial⟩

Uses observedCapability for support in every compatible world; the stated uncertainty condition is trivial.

L111theorem capabilityGrounds : Grounds capability canonicalArticulation

Builds canonical Grounds for this exact capability facet.

L112    (fun f => f = capabilityFacet) [capabilityFacet] :=

Makes only the actual output capability facet applicable, with its own singleton evidence package.

L113  canonicalGroundsForSingleton capabilityFacet capabilityFacetChecked

Applies the singleton Grounds constructor to the already discharged capability facet.

L115theorem actualAdmissible : Admissible held context actual := by

Proves actual identity/apply jointly satisfies capability, budget, observation assumptions and governance/domain scope.

L116  refine ⟨(modelsUnion _ _ _).2 ⟨(modelsSingleton _ _).2 capabilityActual,

Builds an admissible actual-world witness, first proving both jointly held claims; capability uses capabilityActual.

L117    (modelsSingleton _ _).2 (by change 1 ≤ 1; decide)⟩,

The held budget claim computes to actual cost 1 within budget 1.

L118    (modelsSingleton _ _).2 ((observationIdentifies actual).2 rfl), trivial, rfl⟩

Adds compatibility with the zero observation, domain membership at zero, and actual's apply mode.

L120theorem jointConsistent : Consistent held context :=

Derives consistency from the explicitly established actual admissible world.

L121  consequenceConsistency held context ⟨actual, actualAdmissible⟩

Applies semantic consequence consistency using actual and its admissibility proof as the required nonempty witness.

L123/- The current method/principle forms, judgments, rules and own work are read from this very system and world. -/

Documents the following definition or result: Conjoins this system's generation policy, contextual consistency, full content-valid reflexivity and current method/principle form membership.

L124def Charter (s : System) (w : World) : Prop :=

Conjoins this system's generation policy, contextual consistency, full content-valid reflexivity and current method/principle form membership.

L125  Generative (s.policy w) ∧ Consistent (systemHeld s) (systemContext s) ∧

The Charter requires this system's actual policy to be Generative and its jointly held judgments contextually consistent.

L126  Reflexive s.owner (s.rules w) (s.work w) ∧

It also requires full owned-rule reflexivity for this system's actual work log.

L127  (s.policy w).current s.method.form ∧ (s.policy w).current s.principleForm

Both the method form and principle form must be current under that same policy.

L129theorem charterChecked : Charter actualSystem actual :=

Combines evaluated open-policy facts, actual consistency and the content-validated own-work model.

L130  ⟨⟨Or.inl rfl, fun _ _ => trivial⟩, jointConsistent, completeOwnWork_reflexive 0, rfl, rfl⟩

Combines openPolicy's valuation/revisability, jointConsistent, the complete owned log and both version-zero current forms.

L132/- Revision adds a supported input-specific assertion about the same system's realized method. -/

Documents the following definition or result: Adds the system's zero-input output fact to its existing held theory.

L133def revisedHeld : Theory World := union held

Adds the system's zero-input output fact to its existing held theory.

L134  (singleton (fun w => (actualSystem.method.realize w).run 0 = actualSystem.requirements.expected 0))

Adds the specific assertion that this same method meets its required output at input zero.

L136def initialSnapshot : Snapshot World Question := ⟨held, context, 0⟩

Stores the actual held theory/context with revision identity zero.

L137def revisedSnapshot : Snapshot World Question := ⟨revisedHeld, context, 1⟩

Stores the extended held theory with the same context and revision identity one.

L139/-- organon-map CoreReader.Integration.revisionKeepsConsistency

Opens provenance metadata binding CoreReader.Integration.revisionKeepsConsistency to the following source references; this metadata is not a proof premise.

L140organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

Records source reference organon.relationships.roles#p1 with content digest 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e; matching a digest establishes source identity, not semantic fidelity.

L141organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

Records source reference organon.relationships.roles#p2 with content digest 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e; matching a digest establishes source identity, not semantic fidelity.

L142organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

Records source reference organon.relationships.roles#p3 with content digest 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e; matching a digest establishes source identity, not semantic fidelity.

L143-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L144theorem revisionKeepsConsistency :

Keeps the same charter and an admissible model after the added fact, then accepts true and rejects false revision reporting.

L145    Charter actualSystem actual ∧ Consistent revisedHeld context ∧

The actual system retains its Charter, and adding that supported assertion leaves revisedHeld consistent.

L146    TruthfulReport initialSnapshot revisedSnapshot true ∧

Reporting the identified revision as true satisfies the one-way change-report condition.

L147    ¬ TruthfulReport initialSnapshot revisedSnapshot false := by

Reporting that same revision as false violates the condition.

L148  refine ⟨charterChecked, consequenceConsistency revisedHeld context ⟨actual,

Keeps charterChecked and proves revised consistency with actual as a concrete admissible witness.

L149    (modelsUnion _ _ _).2 ⟨actualAdmissible.1, (modelsSingleton _ _).2 rfl⟩,

Actual satisfies old held claims plus the newly added zero-input output assertion.

L150    actualAdmissible.2⟩, (fun _ => rfl), ?_⟩

Retains actual's existing context/scope proof and verifies a true report; only rejection of a false report remains.

L151  intro h

Assumes the changed snapshots could satisfy TruthfulReport with report=false.

L152  have bad := h (Or.inr (by decide))

The revision identifiers 0 and 1 differ, so that assumed obligation forces false=true.

L153  cases bad

Eliminates that impossible Boolean equality, rejecting the concealed revision.

L155/- A claim about this system's method is assessed as its owner's system claim. -/

Documents the following definition or result: Requires this system's assessment record and matching Grounds for its own capability claim.

L156def OwnCapabilityDuty (s : System) (w : World) (facets : List (Facet World)) : Prop :=

Requires this system's assessment record and matching Grounds for its own capability claim.

L157  Performed (s.work w) (.system s.owner) .assessment ∧

OwnCapabilityDuty first requires an actual assessment record targeting this system's owner-identical system subject.

L158  Grounds (systemCapability s) canonicalArticulation (fun f => f ∈ facets) facets

It also requires same-claim Grounds for this system's output capability over all listed applicable facets.

L160/-- organon-map CoreReader.Integration.ownCapabilityGrounded

Opens provenance metadata binding CoreReader.Integration.ownCapabilityGrounded to the following source references; this metadata is not a proof premise.

L161organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L162organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L163organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L164-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L165theorem ownCapabilityGrounded :

Combines the actual content-validated self-assessment record with observation-supported capability Grounds and capability truth.

L166    OwnCapabilityDuty actualSystem actual [capabilityFacet] ∧ capability actual := by

States that the actual system's own capability duty is fulfilled and its claimed capability actually holds.

L167  refine ⟨⟨?_, ?_⟩, capabilityActual⟩

Supplies capabilityActual immediately, leaving the system-assessment record and corresponding Grounds.

L168  · exact ownAssessmentPerformed 0 (.system 0) (by simp [ownSubjects])

Uses the complete log's assessment of system zero as the owned-system work witness.

L169  · exact canonicalGrounds capability [capabilityFacet] (by simp)

Builds Grounds from the nonempty singleton capability-facet list.

L170      (by intro f hf; simp only [List.mem_singleton] at hf; cases hf; exact ⟨rfl, capabilityFacetChecked⟩)

The singleton's only facet has exactly the target claim and the already proved discharge.

L172/- This cost observation is true of both algorithms but does not discriminate their output behavior. -/

Documents the following definition or result: Records cost at most two for the same system implementation; both candidates pass.

L173def costAllowanceRecord : Record World :=

Records cost at most two for the same system implementation; both candidates pass.

L174  ⟨fun w => decide ((actualSystem.method.realize w).cost ≤ 2), true⟩

Records that implementation cost is at most two; both algorithm candidates satisfy this weaker cost observation.

L176def unsupportedCapabilityFacet : Facet World :=

Attempts to support the same output capability from only the permissive cost observation.

L177  .empirical [costAllowanceRecord] (fun _ => True) capability (fun _ => True)

Attempts to support output capability using only cost evidence, with no restrictive scope or uncertainty condition.

L179theorem costCompatibleWithFailure : Compatible [costAllowanceRecord] (.successor, .apply) := by

Computes that successor/apply satisfies the cost observation despite failing identity output.

L180  intro r hr

Takes a record belonging to the singleton cost-observation list.

L181  simp only [List.mem_singleton] at hr

Singleton membership identifies that record as costAllowanceRecord.

L182  subst r

Substitutes the actual cost record for r.

L183  rfl

Successor costs two, so the recorded at-most-two observation evaluates true.

L185theorem costDoesNotSupportOutput : ¬ Supports [costAllowanceRecord] capability := by

Applies alleged support to the compatible successor counterworld and input zero to derive contradiction.

L186  intro h

Assumes the cost observation supports output capability in every compatible world.

L187  have bad := h (.successor, .apply) costCompatibleWithFailure 0 trivial

Applies that assumption to the compatible successor world and input zero, obtaining the false equation 1=0.

L188  cases bad

Eliminates the impossible output equality, refuting cost-only support.

L190theorem unsupportedGrounds : ¬ Grounds capability canonicalArticulation

Extracts the bad facet's support obligation from alleged Grounds and contradicts the cost countermodel.

L191    (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet] := by

Tests the singleton package that makes this cost-only capability facet applicable.

L192  intro h

Assumes that inadequate singleton package nonetheless satisfies Grounds.

L193  have discharged := (h.2.2 unsupportedCapabilityFacet (by simp)).2.2.2

Extracts FacetDischarged for its actual cost-only capability facet from the Grounds premise.

L194  exact costDoesNotSupportOutput (fun w hw => discharged.2.1 w hw trivial)

Its support clause would yield cost-only Supports, contradicting costDoesNotSupportOutput.

L196/- Five separately adopted requirements govern distinct operations; the mode does not give them priority over one another. -/

Documents the following definition or result: Indexes five individual governance commitments, each with separately interpreted reasons and outcomes.

L197inductive Commitment | generation | consistency | reflexivity | grounds | choice

Indexes five individual governance commitments, each with separately interpreted reasons and outcomes.

L198  deriving DecidableEq, Repr

Generates decidable equality and display instances for the preceding datatype.

L200/- A Grounds policy governs arbitrary claims, articulations and applicable facets, rather than only one capability claim. -/

Documents the following definition or result: Applying mode permits a claim bundle only when Grounds holds; waiving mode permits every bundle.

L201def groundsPermission (mode : Mode) (claim : Claim World) (a : Facet World → Articulation World)

Applying mode permits a claim bundle only when Grounds holds; waiving mode permits every bundle.

L202    (applicable : Facet World → Prop) (facets : List (Facet World)) : Prop :=

Accepts an arbitrary applicability predicate and supplied facet package for the same claim/articulations.

L203  match mode with

Chooses the permission rule according to the governance mode.

L204  | .apply => Grounds claim a applicable facets

Apply mode permits a package only when it actually satisfies Grounds.

L205  | .waive => True

Waive mode permits every package without checking Grounds.

L207def GroundsProvision (mode : Mode) : Prop :=

States the general requirement that every permitted claim bundle has Grounds, across all claims, articulations, applicable facets and lists.

L208  ∀ claim a applicable facets, groundsPermission mode claim a applicable facets →

For every actual claim, articulation family and facet package, provision applies to any package the mode permits.

L209    Grounds claim a applicable facets

Every permitted package must satisfy its own corresponding Grounds duties.

L211theorem groundsProvisionMeaning (mode : Mode) : GroundsProvision mode ↔ mode = .apply := by

Proves applying mode enforces the general provision, while the concrete unsupported cost bundle refutes waiving mode.

L212  cases mode with

Checks the general provision separately for apply and waive modes.

L213  | apply => exact ⟨fun _ => rfl, fun _ _ _ _ _ h => h⟩

In apply mode permission already is Grounds, so the general provision passes by returning the supplied proof.

L214  | waive =>

For waive mode, the proof must show that unrestricted permission violates the general provision.

L215    constructor

Proves both directions of the impossible waive-mode equivalence.

L216    · intro h

Assumes the general provision holds even though this mode waives checks.

L217      exact False.elim (unsupportedGrounds (h capability canonicalArticulation

Applies that universal assumption to the actual unsupported capability package, which would contradict unsupportedGrounds.

L218        (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet] trivial))

Supplies its exact singleton applicability and package; waive permission is true, forcing the invalid Grounds result.

L219    · intro h; cases h

The reverse implication starts from waive=apply, an impossible constructor equality.

L221/- The consistency policy checks a whole same-context theory, not isolated judgments. -/

Documents the following definition or result: Applying mode requires consistency for a proposed theory/context; waiving mode permits it unconditionally.

L222def consistencyPermission (mode : Mode) (t : Theory World) (c : Context World Question) : Prop :=

Applying mode requires consistency for a proposed theory/context; waiving mode permits it unconditionally.

L223  match mode with | .apply => Consistent t c | .waive => True

Apply requires whole-theory consistency in context; waive imposes no such constraint.

L225def conflictingHeld : Theory World := union (singleton capability) (singleton (fun w => ¬ capability w))

Combines the actual capability claim with its negation in one theory.

L227theorem conflictConsequences :

Extracts both signed capability consequences from the simultaneously held contradictory claims.

L228    Consequence conflictingHeld context .correctOutput true ∧

The conflicting held theory entails positive output correctness under the fixed context.

L229    Consequence conflictingHeld context .correctOutput false := by

The same theory and context also entail its negative judgment.

L230  exact ⟨fun w hw => hw.1 capability (Or.inl rfl),

An admissible world's model of conflictingHeld must satisfy its explicitly included capability claim.

L231    fun w hw => hw.1 (fun w => ¬ capability w) (Or.inr rfl)⟩

That same model must also satisfy the explicitly included negation of capability.

L233theorem conflictingHeldInconsistent : ¬ Consistent conflictingHeld context :=

Uses those same-context opposite consequences to refute consistency.

L234  conflictRequiresChange conflictingHeld context .correctOutput conflictConsequences.1 conflictConsequences.2

Uses the two opposite same-context consequences to refute consistency of the conflicting held theory.

L236/- The selection policy applies the actual output/budget and relevant-reason conditions to every implementation. -/

Documents the following definition or result: Applying governance uses the separate feasible relevant-choice norm; waiving governance accepts every proposed reason list.

L237def choicePermission (mode : Mode) (req : Requirements) (i : Implementation) (reasons : List Reason) : Prop :=

Applying governance uses the separate feasible relevant-choice norm; waiving governance accepts every proposed reason list.

L238  match mode with | .apply => JustifiedChoice req i reasons | .waive => True

Apply enforces actual feasibility and reason relevance through JustifiedChoice; waive allows any selection package.

L240/- The following consequences are computed from distinct rule applications; they are not interchangeable support flags. -/

Documents the following definition or result: Applying mode proposes successor, while waiving proposes the unchanged copy operation.

L241def proposedOperation : Mode → Operation

Applying mode proposes successor, while waiving proposes the unchanged copy operation.

L242  | .apply => .successor

Applying the generation rule proposes successor, whose output can differ from copy.

L243  | .waive => .copy

Waiving that rule proposes the unchanged copy operation.

L245def selfSamples : Mode → List Nat

Applying mode tests zero and one; waiving mode tests only the passing sample one.

L246  | .apply => [0, 1]

Applying reflexive assessment checks both zero and one, including the arithmetic counterexample.

L247  | .waive => [1]

Waiving it checks only one, the sample where the arithmetic principle passes.

L249noncomputable def conflictDecision (mode : Mode) : Bool :=

Classically decides the consistency-permission proposition for the concrete conflicting theory; it is noncomputable, not a deployed checker.

L250  @decide (consistencyPermission mode conflictingHeld context) (Classical.propDecidable _)

Uses classical propositional decision to turn the whole conflicting-theory permission into a Boolean; no executable decision algorithm is supplied.

L252noncomputable def groundsDecision (mode : Mode) (facet : Facet World) : Bool :=

Classically decides whether the chosen mode permits the given exact singleton facet bundle.

L253  @decide (groundsPermission mode facet.claim canonicalArticulation (fun f => f = facet) [facet])

Decides permission for this facet's own claim and its exact singleton assessment package.

L254    (Classical.propDecidable _)

Supplies classical decidability for that potentially noncomputable Grounds proposition.

L256noncomputable def choiceDecision (mode : Mode) (i : Implementation) (reasons : List Reason) : Bool :=

Classically decides permission for the specified implementation/reasons under identity requirements.

L257  @decide (choicePermission mode identityRequirements i reasons) (Classical.propDecidable _)

Classically decides this implementation's permission under fixed identity requirements and its supplied reasons.

L259theorem decisionsApply : conflictDecision .apply = false ∧

Proves applying mode rejects contradiction, unsupported capability and infeasible cheap successor while accepting actual capability and identity choice.

L260    groundsDecision .apply unsupportedCapabilityFacet = false ∧

Applying Grounds rejects the cost-only capability package.

L261    groundsDecision .apply capabilityFacet = true ∧

Applying Grounds accepts the properly supported output-observation package.

L262    choiceDecision .apply cheapSuccessor [.method .simplicity] = false ∧

Applying choice rejects cheapSuccessor despite its relevant simplicity reason, because its output is infeasible.

L263    choiceDecision .apply identityImpl objectiveReason = true := by

Applying choice accepts identity with its actual output reason.

L264  classical

Enables the classical decidability instances used in these Boolean permission definitions.

L265  simp only [conflictDecision, groundsDecision, choiceDecision, consistencyPermission,

Unfolds the three Boolean decisions and their apply-mode consistency predicate.

L266    groundsPermission, choicePermission]

Also unfolds Grounds and choice permission, exposing the actual propositions each Boolean decides.

L267  exact ⟨decide_eq_false conflictingHeldInconsistent,

The proved inconsistency forces conflictDecision apply to false.

L268    decide_eq_false unsupportedGrounds, decide_eq_true capabilityGrounds,

The failed cost package decides false, while the discharged observation package decides true.

L269    decide_eq_false eligibleInternalReasonNotSufficient.2, decide_eq_true identityJustified⟩

The infeasible cheap method decides false; the feasible justified identity decides true.

L271theorem decisionsWaive : conflictDecision .waive = true ∧

Computes that waiving mode accepts the concrete contradiction, unsupported facet and infeasible choice.

L272    groundsDecision .waive unsupportedCapabilityFacet = true ∧

Waive mode accepts even the unsupported cost-only capability package.

L273    choiceDecision .waive cheapSuccessor [.method .simplicity] = true := by

It also accepts cheapSuccessor with simplicity alone despite the wrong output.

L274  exact ⟨@decide_eq_true (consistencyPermission .waive conflictingHeld context)

Starts the waiver calculation with consistencyPermission, which is definitionally True in this mode.

L275    (Classical.propDecidable _) trivial,

Uses that trivial permission proof to obtain the true Boolean conflict decision.

L276    @decide_eq_true (groundsPermission .waive unsupportedCapabilityFacet.claim canonicalArticulation

Next decides waiver permission for the exact unsupported capability facet's claim.

L277      (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet]) (Classical.propDecidable _) trivial,

Its singleton applicability/package is unchanged; waiver makes permission True and the decision true.

L278    @decide_eq_true (choicePermission .waive identityRequirements cheapSuccessor [.method .simplicity])

Finally decides waiver permission for the same cheap method and simplicity-only reasons.

L279      (Classical.propDecidable _) trivial⟩

That permission is again trivially True, completing all three waiver decisions.

L281/- Each application supplies its own outcome type, adopted objective, constraints and actual option-indexed reasons. -/

Documents the following definition or result: For each commitment, interprets governance modes as options with its own operational outcome, objective, constraint, actual reasons and scoped criticism response.

L282noncomputable def commitmentPositionFor (c : Commitment) (chosenMode : Mode) : ValuePosition World :=

For each commitment, interprets governance modes as options with its own operational outcome, objective, constraint, actual reasons and scoped criticism response.

L283  match c with

Chooses a different operational value-position adapter for each of the five commitments.

L284  | .generation => {

Constructs the value position for the generation commitment.

L285      Position := Mode, Outcome := Operation, adopted := chosenMode, selected := actualSystem.governance,

Its positions are governance modes, outcomes are operations, and adoption is compared with this same system's selected governance.

L286      outcome := fun _ mode => proposedOperation mode,

Maps a mode to the actual proposed successor-or-copy operation.

L287      objective := fun op => op.run 0 ≠ Operation.copy.run 0,

The adopted generation objective requires output at zero to differ from copy's zero output.

L288      constraints := fun _ mode => Generative (policyFor mode),

Also requires the mode's actual policy to satisfy the adopted Generative constraints.

L289      starting := singleton (fun w => actualSystem.governance w = chosenMode),

Explicitly assumes the same system has selected chosenMode; this is a starting commitment, not a derived universal fact.

L290      reasons := [fun _ mode => (proposedOperation mode).run 0 = 1 ∧ Operation.copy.run 0 = 0],

Its option-dependent reason compares the proposed operation's 0→1 behavior with copy's 0→0 behavior.

L291      limits := fun w => w.1 = .identity,

Limits this generation position to worlds whose implementation candidate is identity.

L292      relevantCriticism := fun _ => ¬ Expanded baseState inflatedState,

Keeps actual inventory inflation without expansion as a relevant criticism of the generation commitment.

L293      response := fun _ => some "Pursuing expansion does not guarantee it; assess the actual before and after capabilities separately" }

Responds that orientation does not guarantee progress and before/after capabilities need separate assessment; the stored response is nonempty text.

L294  | .consistency => {

Constructs the distinct value position for the consistency commitment.

L295      Position := Mode, Outcome := Bool, adopted := chosenMode, selected := actualSystem.governance,

Uses modes as positions and a Boolean conflict-admission decision as outcome, tied to the same selected governance.

L296      outcome := fun _ mode => conflictDecision mode,

Its actual outcome is the mode's decision on the whole conflicting theory.

L297      objective := fun accepted => accepted = false,

Requires that decision to reject the conflicting theory.

L298      constraints := fun _ mode => consistencyPermission mode held context,

Simultaneously requires the actual held theory and context to pass the same mode's consistency permission.

L299      starting := singleton (fun w => actualSystem.governance w = chosenMode),

States adoption of chosenMode by the same system as this position's explicit starting assumption.

L300      reasons := [fun _ _ => Consequence conflictingHeld context .correctOutput true ∧

The consistency reason begins with the conflicting theory's positive output-correctness consequence.

L301        Consequence conflictingHeld context .correctOutput false],

It also includes the opposite consequence under exactly the same question and context.

L302      limits := fun w => w.1 = .identity,

Limits this consistency position to identity-candidate worlds.

L303      relevantCriticism := fun _ => ¬ Entails (emptyTheory : Theory Bool) (fun w => w = true),

Uses the empty Bool theory's failure to entail truth at every world as the live incompleteness criticism.

L304      response := fun _ => some "Consistency alone does not establish sufficient support; assess the claim with its grounds as well" }

Responds that consistency alone does not establish sufficient support and the claim's grounds still need assessment.

L305  | .reflexivity => {

Constructs the value position for reflexive assessment.

L306      Position := Mode, Outcome := List Nat, adopted := chosenMode, selected := actualSystem.governance,

Uses modes as positions and an actual sample-input list as outcome, tied to the same selected governance.

L307      outcome := fun _ mode => selfSamples mode,

The mode chooses the sample set [0,1] or [1].

L308      objective := fun samples => ∃ n ∈ samples, ownArithmeticPrinciple n = false,

Requires some actually selected sample to expose a false result of the same arithmetic principle.

L309      constraints := fun _ mode => Reflexive 0 (ownRules 0) (workFor 0 mode),

Also requires full owner-zero rule/work reflexivity for that same mode.

L310      starting := singleton (fun w => actualSystem.governance w = chosenMode),

Explicitly adopts chosenMode for this same system as the starting commitment.

L311      reasons := [fun _ _ => ownArithmeticPrinciple 0 = false ∧ ownArithmeticPrinciple 1 = true],

The reason identifies actual arithmetic failure at zero and success at one.

L312      limits := fun w => w.1 = .identity,

Restricts this reflexivity position to identity-candidate worlds.

L313      relevantCriticism := fun _ => selfTest [1] = true ∧ ownArithmeticPrinciple 0 = false,

Retains the passing test at one together with the actual failure at zero as criticism.

L314      response := fun _ => some "A passing self-test does not certify the principle; retain the relevant counterexample and its scope" }

Responds that passing a self-test does not certify the principle and the counterexample's scope must be retained.

L315  | .grounds => {

Constructs the value position for the Grounds provision itself.

L316      Position := Mode, Outcome := Bool, adopted := chosenMode, selected := actualSystem.governance,

Uses modes as positions and a Boolean evidence-package decision as outcome, under the same system's governance.

L317      outcome := fun _ mode => groundsDecision mode unsupportedCapabilityFacet,

The actual outcome tests the unsupported cost-only capability facet.

L318      objective := fun accepted => accepted = false,

Requires rejection of that unsupported evidence package.

L319      constraints := fun _ mode => groundsPermission mode capability canonicalArticulation

Also requires permission for the actual capability claim with its content-derived articulations.

L320        (fun f => f = capabilityFacet) [capabilityFacet],

That positive constraint uses exactly the properly discharged singleton capabilityFacet package.

L321      starting := singleton (fun w => actualSystem.governance w = chosenMode),

States this same system's adoption of chosenMode as an explicit starting commitment.

L322      reasons := [fun _ _ => Compatible [costAllowanceRecord] (.successor, .apply) ∧

The Grounds reason records that the successor/apply world is compatible with the cost observation.

L323        ¬ capability (.successor, .apply)],

It pairs that compatibility with actual failure of the claimed output capability in that same world.

L324      limits := fun w => w.1 = .identity,

Restricts this Grounds position to identity-candidate worlds.

L325      relevantCriticism := fun _ => OutputContract outputOnlyProcess ∧ ¬ ExplanationContract outputOnlyProcess,

The criticism points to the same process having the output contract without an attached explanation contract.

L326      response := fun _ => some "Grounds allows an external output assessment without requiring this process to provide an internal explanation" }

Responds that external output assessment can supply Grounds without requiring this process to explain its internal generation.

L327  | .choice => {

Constructs the separate value position for implementation choice.

L328      Position := Mode, Outcome := Bool, adopted := chosenMode, selected := actualSystem.governance,

Uses modes as positions and a Boolean method-admission decision as outcome, under the same governance selection.

L329      outcome := fun _ mode => choiceDecision mode cheapSuccessor [.method .simplicity],

The tested choice is the cheap successor justified only by its simplicity reason.

L330      objective := fun accepted => accepted = false,

Requires rejection of that wrong-output choice.

L331      constraints := fun _ mode => choicePermission mode identityRequirements identityImpl objectiveReason,

Also requires acceptance of identity under the same requirements with its actual output reason.

L332      starting := singleton (fun w => actualSystem.governance w = chosenMode),

Explicitly adopts chosenMode for this system; the value starting point is not proved from neutral facts.

L333      reasons := [fun _ _ => cheapSuccessor.run 0 = 1 ∧ identityRequirements.expected 0 = 0 ∧

The choice reason contrasts cheapSuccessor's output one with the required output zero on the same input.

L334        cheapSuccessor.cost ≤ identityRequirements.budget],

Also records that the method fits the budget, so cheapness cannot conceal its output failure.

L335      limits := fun w => w.1 = .identity,

Limits this choice position to identity-candidate worlds.

L336      relevantCriticism := fun _ => identityImpl.conventional = true ∧ identityImpl.established = true,

Keeps identity's actual conventional and established status as a relevant criticism of excluding existing methods.

L337      response := fun _ => some "An existing conventional method remains eligible when actual output and budget reasons justify it" }

Responds that a conventional existing method remains eligible when actual output and budget reasons justify it.

L339noncomputable def commitmentPosition (c : Commitment) : ValuePosition World := commitmentPositionFor c .apply

Specializes each individually interpreted position to adopting applying governance.

L341/- The fact used as a reason has content before evaluating the adopted rule's consequence. -/

Documents the following definition or result: Checks every listed commitment-specific reason at the same actual world and adopted mode by concrete counterexamples or computation.

L342theorem positionReasons (c : Commitment) :

Checks every listed commitment-specific reason at the same actual world and adopted mode by concrete counterexamples or computation.

L343    ∀ r ∈ (commitmentPosition c).reasons, r actual (commitmentPosition c).adopted := by

Every actual listed reason for commitment c must hold at actual for its adopted apply option.

L344  cases c <;> intro r hr <;> dsimp [commitmentPosition, commitmentPositionFor] at hr ⊢ <;>

Separates the five commitments and unfolds each actual reason list while fixing a listed reason r.

L345    rcases List.mem_singleton.mp hr with rfl

Each list is a singleton, so the membership premise identifies r with that commitment's concrete reason.

L346  · exact ⟨rfl, rfl⟩

Generation's reason computes successor 0=1 and copy 0=0.

L347  · exact conflictConsequences

Consistency's reason uses the already proved positive and negative consequences of the same conflicting theory.

L348  · exact ⟨rfl, rfl⟩

Reflexivity's reason computes failure at zero and success at one for the same arithmetic principle.

L349  · refine ⟨costCompatibleWithFailure, ?_⟩

For Grounds, supplies the successor world's cost compatibility and leaves its capability failure to prove.

L350    intro h

Assumes that same successor world nevertheless has the required output capability.

L351    have bad := h 0 trivial

At required input zero, that assumption yields successor's output one equal to required zero.

L352    cases bad

Eliminates the impossible 1=0 equality, proving the capability failure part of the reason.

L353  · exact ⟨rfl, rfl, by decide⟩

Choice's reason computes output one, required zero and the cheap method's within-budget cost.

L355/- Each adopted rule has its stated consequence in this explicitly defined application; this is not ultimate value justification. -/

Documents the following definition or result: Proves each adopted mode has its stated objective and constraint using actual decision and compliance theorems, without asserting ultimate normative validity.

L356theorem positionConsequence (c : Commitment) (w : World) : (commitmentPosition c).consequence w := by

Proves each adopted mode has its stated objective and constraint using actual decision and compliance theorems, without asserting ultimate normative validity.

L357  cases c <;> dsimp [commitmentPosition, commitmentPositionFor, ValuePosition.consequence]

Unfolds each commitment's consequence into its actual objective and mode-dependent constraint.

L358  · exact ⟨by decide, ⟨Or.inl rfl, fun _ _ => trivial⟩⟩

Generation's apply option differs from copy at zero and its openPolicy satisfies valuation plus revisability.

L359  · exact ⟨decisionsApply.1, jointConsistent⟩

Consistency's apply option rejects the conflicting theory while the actual held theory remains consistent.

L360  · exact ⟨⟨0, by simp [selfSamples], rfl⟩, completeOwnWork_reflexive 0⟩

Reflexivity chooses the actual counterexample zero from [0,1] and supplies full contentful owned-work reflexivity.

L361  · exact ⟨decisionsApply.2.1, capabilityGrounds⟩

Grounds rejects the unsupported cost package while the proper capability package has Grounds.

L362  · exact ⟨decisionsApply.2.2.2.1, identityJustified⟩

Choice rejects cheapSuccessor and retains the justified feasible identity implementation.

L364theorem positionProcedure (c : Commitment) : ValueProcedure (commitmentPosition c) := by

Builds nonempty reason lists, joint adoption, checked option consequences and nonempty responses for every commitment; reason assumptions are not needed by the already proved consequences.

L365  refine ⟨?_, ?_, ?_, ?_⟩

Splits ValueProcedure into nonempty reasons, joint adoption, the scoped consequence rule and criticism response.

L366  · cases c <;> simp [commitmentPosition, commitmentPositionFor]

Checks that every commitment's actual reason list contains its singleton reason.

L367  · refine ⟨actual, ?_, ?_, ?_, positionReasons c⟩

Uses the same actual world for JointAdoption and supplies positionReasons c; remaining goals are starting-theory membership, limits and adoption.

L368    · cases c <;> exact (modelsSingleton _ _).2 rfl

In actual, governance is apply, so the singleton starting theory selecting the adopted mode holds.

L369    · cases c <;> rfl

For each commitment, actual's identity candidate satisfies its declared limit.

L370    · cases c <;> rfl

For each commitment, actual's selected governance equals the adopted apply option.

L371  · intro w _ _ _

Takes an arbitrary world and the procedure's starting, limit and all-reasons premises for its consequence clause.

L372    exact positionConsequence c w

Uses positionConsequence, which already proves that apply option's objective and constraints for every world; these premises are not needed here.

L373  · intro w _ _

For the response clause, takes a world with an in-scope relevant criticism.

L374    cases c <;> exact ⟨_, rfl, by decide⟩

Every commitment returns its actual stored nonempty response string, satisfying the response-existence requirement.

L376/- Criticism is instantiated within the adopted position's actual limit rather than made vacuous. -/

Documents the following definition or result: Provides an actual in-scope criticism case for each commitment, avoiding vacuous response obligations in these examples.

L377theorem criticismWithinScope (c : Commitment) :

Provides an actual in-scope criticism case for each commitment, avoiding vacuous response obligations in these examples.

L378    (commitmentPosition c).limits actual ∧ (commitmentPosition c).relevantCriticism actual := by

Requires both that actual is inside this commitment's limits and that its specific criticism really applies there.

L379  constructor

Separates the actual-limit check from the actual-criticism check.

L380  · cases c <;> rfl

Every limit asks for identity, which is actual's candidate by definition.

L381  · cases c

Checks each commitment's distinct criticism rather than assuming criticism vacuously.

L382    · simp [commitmentPosition, commitmentPositionFor, Expanded, baseState, inflatedState]

Generation's criticism holds because inflating baseline lists creates no newly understood or constructed operation.

L383    · exact consistentIncomplete.2.1

Consistency's criticism uses the empty theory's proved failure to entail the selected Bool claim.

L384    · exact ⟨rfl, rfl⟩

Reflexivity's criticism computes a passing sample at one and failure at zero.

L385    · exact ⟨outputNotExplanation.1, outputNotExplanation.2.1⟩

Grounds' criticism combines actual output correctness of outputOnlyProcess with its absent explanation contract.

L386    · exact ⟨rfl, rfl⟩

Choice's criticism holds because identity is actually conventional and established.

L388/- Waiving the rule changes the actual computed outcome or an explicit adopted constraint; old reasons cannot certify it unchanged. -/

Documents the following definition or result: Shows the waiving option fails each unchanged commitment-specific objective or constraint.

L389theorem oppositeConsequenceFails (c : Commitment) (w : World) :

Shows the waiving option fails each unchanged commitment-specific objective or constraint.

L390    ¬ (commitmentPositionFor c .waive).consequence w := by

Claims that every commitment's waive option fails its declared objective or constraint in any world.

L391  cases c <;> intro h

Separates the commitments and assumes the corresponding waive consequence, seeking a contradiction.

L392  · exact permissionNotValuation.2.2 h.2

Generation's consequence would require Generative neutralPolicy, contradicting permissionNotValuation's proved failure.

L393  · have bad : conflictDecision .waive = false := h.1

Consistency's assumed objective says waive must reject the conflicting theory.

L394    rw [decisionsWaive.1] at bad

But decisionsWaive computes acceptance=true, turning that objective into true=false.

L395    cases bad

Rejects that impossible Boolean equality for the consistency option.

L396  · obtain ⟨n, hn, hf⟩ := h.1

Reflexivity's assumed objective supplies a selected sample n where the arithmetic principle is false.

L397    change n ∈ [1] at hn

Waive mode's selected samples are exactly [1].

L398    have he : n = 1 := List.mem_singleton.mp hn

Membership in that singleton forces the supposed failing input n to be one.

L399    subst n

Replaces n with one in the alleged failure proof.

L400    cases hf

The principle actually returns true at one, contradicting its alleged false result.

L401  · have bad : groundsDecision .waive unsupportedCapabilityFacet = false := h.1

Grounds' assumed objective says waive rejects the specific unsupported capability package.

L402    rw [decisionsWaive.2.1] at bad

decisionsWaive instead says that same package is accepted, yielding true=false.

L403    cases bad

Rejects the impossible equality, so the waived Grounds consequence fails.

L404  · have bad : choiceDecision .waive cheapSuccessor [.method .simplicity] = false := h.1

Choice's assumed objective says waive rejects cheapSuccessor with simplicity alone.

L405    rw [decisionsWaive.2.2] at bad

decisionsWaive proves that exact selection is accepted, again yielding true=false.

L406    cases bad

Rejects that equality, completing failure of all five waive consequences.

L408theorem oppositeProcedureRejected (c : Commitment) : ¬ ValueProcedure (commitmentPositionFor c .waive) := by

Combines a hypothetical joint-adoption witness with consequence failure to reject the opposite mode's procedure.

L409  intro h

Assumes the opposite waive value position nevertheless satisfies ValueProcedure.

L410  obtain ⟨w, hs, hl, _, hr⟩ := h.2.1

Extracts its JointAdoption witness w, starting-theory proof hs, limit proof hl and all-reasons proof hr.

L411  exact oppositeConsequenceFails c w (h.2.2.1 w hs hl hr)

The assumed procedure's consequence clause applied to that same joint witness produces the waive consequence, which oppositeConsequenceFails c w refutes.

L413/- Each statement names adoption of a particular rule; its defined policy gives that option its meaning. -/

Documents the following definition or result: Extracts each position's adoption claim; all use the same governance selector but have separately assessed consequences and reasons.

L414noncomputable def commitmentClaim (c : Commitment) : Claim World := (commitmentPosition c).commitment

Extracts each position's adoption claim; all use the same governance selector but have separately assessed consequences and reasons.

L416noncomputable def commitmentFacet (c : Commitment) : Facet World := .value (commitmentPosition c)

Wraps the specific interpreted commitment position as a value facet.

L418/-- organon-map CoreReader.Integration.reasonsBelongToCommitments

Opens provenance metadata binding CoreReader.Integration.reasonsBelongToCommitments to the following source references; this metadata is not a proof premise.

L419organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L420organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L421organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L422-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L423theorem reasonsBelongToCommitments (c : Commitment) :

Provides per-commitment Grounds, a real joint adoption, actual relevant criticism and rejection of the opposite policy under the same interpreted objective.

L424    Grounds (commitmentClaim c) canonicalArticulation

Requires Grounds for the actual adoption claim of commitment c, with articulation built from its facet contents.

L425      (fun f => f = commitmentFacet c) [commitmentFacet c] ∧

Makes exactly commitmentFacet c applicable and supplies only that same facet.

L426    JointAdoption (commitmentPosition c) ∧

Additionally requires a nonempty jointly admissible adoption witness for that position.

L427    (commitmentPosition c).relevantCriticism actual ∧

Requires this particular commitment's criticism to actually hold at actual.

L428    ¬ ValueProcedure (commitmentPositionFor c .waive) := by

Also proves the opposite waive position fails the same value-procedure requirements.

L429  exact ⟨canonicalGroundsForSingleton (commitmentFacet c) (positionProcedure c),

Constructs singleton Grounds using that commitment's checked positionProcedure.

L430    (positionProcedure c).2.1, (criticismWithinScope c).2, oppositeProcedureRejected c⟩

Adds its joint witness, actual criticism and the proved rejection of its opposite position.

L432/- This claim concerns the Grounds rule for arbitrary claim/facet packages, not a single capability duty. -/

Documents the following definition or result: Proves the grounds position's adoption claim is extensionally the general Grounds provision for the selected governance mode.

L433theorem groundsCommitmentIsProvision : commitmentClaim .grounds = (fun w => GroundsProvision w.2) := by

Proves the grounds position's adoption claim is extensionally the general Grounds provision for the selected governance mode.

L434  funext w

To equate the two claims, fixes an arbitrary world w and compares their propositions there.

L435  apply propext

Uses proposition extensionality: equivalence of the two propositions suffices for their equality.

L436  exact (groundsProvisionMeaning w.2).symm

groundsProvisionMeaning says the general provision holds exactly in apply mode, matching this adoption claim in reverse direction.

L438/-- organon-map CoreReader.Integration.groundsSelfAssessment

Opens provenance metadata binding CoreReader.Integration.groundsSelfAssessment to the following source references; this metadata is not a proof premise.

L439organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L440organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L441organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L442-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L443theorem groundsSelfAssessment :

Applies value Grounds to the general Grounds provision itself, retaining actual scope/criticism and a rejected waiver variant.

L444    Grounds (fun w => GroundsProvision w.2) canonicalArticulation

Assesses the general GroundsProvision itself, quantified over claim/facet packages, with content-derived articulation.

L445      (fun f => f = commitmentFacet .grounds) [commitmentFacet .grounds] ∧

The applicable value aspect is exactly the grounds commitment's own facet.

L446    (commitmentPosition .grounds).limits actual ∧

Requires actual to satisfy that commitment's declared limit.

L447    (commitmentPosition .grounds).relevantCriticism actual ∧

Requires its criticism to actually apply at actual as well.

L448    ¬ ValueProcedure (commitmentPositionFor .grounds .waive) := by

Requires the opposite waived Grounds commitment to fail ValueProcedure.

L449  rw [← groundsCommitmentIsProvision]

Rewrites the general provision as the extensionally identical grounds adoption claim.

L450  exact ⟨(reasonsBelongToCommitments .grounds).1,

Reuses the actual Grounds proof for that same grounds commitment.

L451    (criticismWithinScope .grounds).1, (criticismWithinScope .grounds).2,

Supplies the separately checked actual limit and actual relevant criticism.

L452    oppositeProcedureRejected .grounds⟩

Supplies the proved failure of the opposite waived Grounds position.

L454/- This existing principle form implements the same system's choice rule on two actual proposals.

Documents the following definition or result: Stores the current philosophical principle form and its actual governance mode.

L455Input 0 names the identity proposal; input 1 names the cheap successor proposal. -/

Documents the following definition or result: Stores the current philosophical principle form and its actual governance mode.

L456structure PhilosophyMethod where

Stores the current philosophical principle form and its actual governance mode.

L457  form : Form

Stores the actual principle form this philosophy method implements.

L458  mode : Mode

Stores whether this same philosophy method applies or waives its governance checks.

L460def currentPhilosophy (s : System) (w : World) : PhilosophyMethod :=

Derives the reviewed philosophy object from this same system's principle form and governance selection.

L461  ⟨s.principleForm, s.governance w⟩

Builds the philosophy method from this system's own principle form and its governance in w.

L463noncomputable def PhilosophyMethod.review (p : PhilosophyMethod) (input : Nat) : Nat :=

Returns approval decisions for the identity proposal at zero and the cheap infeasible proposal otherwise, using this philosophy's actual governance mode.

L464  if input = 0 then

Input zero identifies the identity-method proposal; every other input follows the cheap-successor proposal branch.

L465    if choiceDecision p.mode identityImpl objectiveReason then 1 else 0

For identity, runs this philosophy method's actual choice policy and returns 1 for accept, 0 for reject.

L466  else if choiceDecision p.mode cheapSuccessor [.method .simplicity] then 1 else 0

For other inputs, applies the same policy to cheapSuccessor with simplicity alone, again encoding accept/reject as 1/0.

L468noncomputable def PhilosophyMethod.implementation (p : PhilosophyMethod) : Implementation where

Exposes that actual philosophical review procedure as an implementation with domain zero/one and matching output/trace proxies.

L469  name := "Current philosophy's proposal review"

Names the implementation as the current philosophy's actual proposal-review method.

L470  conventional := true

Marks this proposal-review implementation as conventional.

L471  established := true

Also marks the same implementation as established; later proof tests whether that alone justifies priority.

L472  run := p.review

The implementation's actual run is precisely this philosophy method's review function.

L473  cost := 1

Assigns cost one to this review implementation.

L474  domain n := n = 0 ∨ n = 1

Declares only proposal identifiers zero and one within its application domain.

L475  explanation := p.review

Provides the same review function as the implementation's explanation field.

L476  trace n := [n, p.review n]

Records a two-entry trace containing the proposal identifier and its actual review result.

L478def proposalRequirements : Requirements where

Requires accepting proposal zero and rejecting proposal one within budget one.

L479  inputs n := n = 0 ∨ n = 1

The application tests exactly proposal identifiers zero and one.

L480  expected n := if n = 0 then 1 else 0

Requires identity's proposal zero to be accepted as 1 and the other tested proposal to be rejected as 0.

L481  budget := 1

Allows this review method a cost budget of one.

L482  values _ := True

Imposes no additional restriction through the requirements' values predicate in this example.

L484theorem currentReviewCorrect : ∀ n, proposalRequirements.inputs n →

Computes both requested proposal decisions from applying-governance results.

L485    (currentPhilosophy actualSystem actual).review n = proposalRequirements.expected n := by

For each required proposal, the actual system's current philosophy review must equal the application's expected verdict.

L486  intro n hn

Takes a proposal n with proof hn that it is one of the required inputs.

L487  rcases hn with rfl | rfl <;>

Uses hn to restrict n to the concrete identity or cheap-successor proposal identifier.

L488    simp [PhilosophyMethod.review, currentPhilosophy, actualSystem, actual,

Unfolds the same current philosophy method and actual system to expose the real proposal decisions.

L489      proposalRequirements, decisionsApply.2.2.2.1, decisionsApply.2.2.2.2]

Uses decisionsApply to match accepted identity and rejected cheap successor against their required verdicts.

L491/- Status alone fails for this actual principle method; its demonstrated proposal decisions give a relevant reason. -/

Documents the following definition or result: Binds the implementation to the current principle/governance object, rejects status-only priority and justifies it by its two actual proposal decisions.

L492/-- organon-map CoreReader.Integration.existingPhilosophyNotPrivileged

Opens provenance metadata binding CoreReader.Integration.existingPhilosophyNotPrivileged to the following source references; this metadata is not a proof premise.

L493organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L494organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L495organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L496-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L497theorem existingPhilosophyNotPrivileged :

Binds the implementation to the current principle/governance object, rejects status-only priority and justifies it by its two actual proposal decisions.

L498    (currentPhilosophy actualSystem actual).form = actualSystem.principleForm ∧

Checks this philosophy method's form is exactly the actual system's current principle form.

L499    (currentPhilosophy actualSystem actual).mode = actualSystem.governance actual ∧

Checks its governance mode is exactly the same system's mode at actual.

L500    ¬ JustifiedChoice proposalRequirements

Begins the claim that status alone cannot justify choosing this actual review implementation.

L501      (currentPhilosophy actualSystem actual).implementation [.status .standing] ∧

The rejected reason list is exactly [.status .standing] for that same philosophy implementation.

L502    JustifiedChoice proposalRequirements

By contrast, asserts this implementation has a justified choice under the actual proposal requirements.

L503      (currentPhilosophy actualSystem actual).implementation [.method .output] ∧

That positive choice uses its actual output reason, not merely its name or established flag.

L504    (currentPhilosophy actualSystem actual).review 0 = 1 ∧

The same philosophy review actually accepts identity's proposal zero with result one.

L505    (currentPhilosophy actualSystem actual).review 1 = 0 := by

It actually rejects cheap successor's proposal one with result zero.

L506  refine ⟨rfl, rfl, statusOnlyFails _ _ _, ?_, currentReviewCorrect 0 (Or.inl rfl),

Provides same-form/mode identities, status-only rejection and correct proposal-zero evaluation; leaves positive output-based choice to prove.

L507    currentReviewCorrect 1 (Or.inr rfl)⟩

Also supplies currentReviewCorrect for required proposal one, proving its actual rejection.

L508  exact ⟨⟨currentReviewCorrect, by change 1 ≤ 1; decide⟩,

Builds the positive choice's feasibility from both correct proposal outputs and cost 1≤budget 1.

L509    .method .output, by simp, trivial, currentReviewCorrect⟩

Uses the listed .method .output reason and currentReviewCorrect as its actual relevance witness.

L511/- Applications choose their contract and requirements; the resulting claim is about this system's actual method. -/

Documents the following definition or result: Applies any supplied application contract and requirements to this system's actual world-dependent method.

L512def applicationClaim (s : System) (req : Requirements)

Applies any supplied application contract and requirements to this system's actual world-dependent method.

L513    (contract : Requirements → Implementation → Prop) : Claim World :=

Accepts an arbitrary application contract relating Requirements to the implementation being assessed.

L514  fun w => contract req (s.method.realize w)

At each world, applies that same contract and requirements to this system's actual method realization.

L516def ApplicationDuties (s : System) (w : World) (req : Requirements)

Conjoins full same-system reflexivity with Grounds for the exact parameterized application claim.

L517    (contract : Requirements → Implementation → Prop)

ApplicationDuties keeps the chosen application contract as an explicit parameter.

L518    (articulations : Facet World → Articulation World)

Also accepts the articulation supplied for each potentially relevant facet.

L519    (applicable : Facet World → Prop) (facets : List (Facet World)) : Prop :=

Keeps the actual applicability predicate separate from the supplied facet list.

L520  Reflexive s.owner (s.rules w) (s.work w) ∧

Requires full reflexivity of the same system owner's actual rules and work at w.

L521  Grounds (applicationClaim s req contract) articulations applicable facets

Requires matching Grounds for the claim produced by this system, these requirements and this contract.

L523/- These are consequences of an explicitly adopted duty, not a proof that arbitrary applications fulfill it. -/

Documents the following definition or result: Projects an explicitly assumed application-compliance interface into reflexivity, applicability coverage and matching discharged facets; it does not invent compliance.

L524/-- organon-map CoreReader.Integration.applicationRetainsDuties

Opens provenance metadata binding CoreReader.Integration.applicationRetainsDuties to the following source references; this metadata is not a proof premise.

L525organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L526organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L527organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L528-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L529theorem applicationRetainsDuties (s : System) (w : World) (req : Requirements)

Projects an explicitly assumed application-compliance interface into reflexivity, applicability coverage and matching discharged facets; it does not invent compliance.

L530    (contract : Requirements → Implementation → Prop)

The theorem retains the arbitrary application contract rather than fixing a single capability definition.

L531    (articulations : Facet World → Articulation World)

Retains the actual articulation family for that application's facets.

L532    (applicable : Facet World → Prop) (facets : List (Facet World))

Retains the application's own applicability predicate and supplied facet list.

L533    (h : ApplicationDuties s w req contract articulations applicable facets) :

Crucially assumes ApplicationDuties already holds for these exact objects; the theorem does not create compliance.

L534    Reflexive s.owner (s.rules w) (s.work w) ∧

The conclusion retains full same-owner rule/work reflexivity from that assumed duty.

L535    (∀ f, applicable f → f ∈ facets) ∧

It requires every actually applicable facet to occur in the supplied list, regardless of labels.

L536    (∀ f ∈ facets, f.claim = applicationClaim s req contract ∧

For every listed facet, its assessed claim must equal this system's actual parameterized application claim.

L537      Articulated (articulations f) ∧ FacetArticulated (articulations f) f ∧ FacetDischarged f) :=

That same facet must have an articulable, content-matching articulation and actually satisfy its discharge conditions.

L538  ⟨h.1, h.2.2.1, h.2.2.2⟩

Projects h.1 as reflexivity, h.2.2.1 as applicability coverage, and h.2.2.2 as each listed facet's same-claim, articulation and discharge checks.

L540def outputContract (req : Requirements) (i : Implementation) : Prop :=

Requires the implementation to meet the application's expected output on every requested input.

L541  ∀ n, req.inputs n → i.run n = req.expected n

The output contract checks this implementation's actual run against the chosen expected output on every required input.

L543def successorRequirements : Requirements :=

Changes the same application requirements from identity to successor output while retaining other fields.

L544  { identityRequirements with expected := fun n => n + 1 }

Keeps identityRequirements' inputs and other fields but changes expected output to n+1.

L546/- Holding the system and observation fixed while changing the actual objective changes the capability claim. -/

Documents the following definition or result: Reuses the old observation while changing the assessed claim to the successor objective, setting up a same-object scope test.

L547def changedObjectiveFacet : Facet World :=

Reuses the old observation while changing the assessed claim to the successor objective, setting up a same-object scope test.

L548  .empirical [observation] (fun _ => True)

Reuses the old actual observation for an empirical facet with unrestricted scope.

L549    (applicationClaim actualSystem successorRequirements outputContract) (fun _ => True)

Changes its assessed claim to this same system meeting successorRequirements; the uncertainty predicate remains trivial.

L551/-- organon-map CoreReader.Integration.applicationVariation

Opens provenance metadata binding CoreReader.Integration.applicationVariation to the following source references; this metadata is not a proof premise.

L552organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L553organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L554organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L555-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L556theorem applicationVariation :

In this example, the original identity contract retains its fulfilled duties; the changed successor contract fails for the same actual method, and the specified retained-observation package cannot ground it.

L557    ApplicationDuties actualSystem actual identityRequirements outputContract

The original identity-output application fulfills ApplicationDuties for the actual system and world.

L558      canonicalArticulation (fun f => f = capabilityFacet) [capabilityFacet] ∧

That positive instance uses the already supported capabilityFacet and its own constructed articulation.

L559    ¬ applicationClaim actualSystem successorRequirements outputContract actual ∧

But the same actual system does not meet the changed successor-output contract.

L560    ¬ Grounds (applicationClaim actualSystem successorRequirements outputContract)

Nor does the changed claim acquire Grounds from the retained observation package.

L561      canonicalArticulation (fun f => f = changedObjectiveFacet) [changedObjectiveFacet] := by

This failure concerns exactly changedObjectiveFacet's singleton package, not every possible evidence package.

L562  refine ⟨⟨completeOwnWork_reflexive 0, capabilityGrounds⟩, ?_, ?_⟩

Builds the original duty from full owned reflexivity and capabilityGrounds, then leaves changed behavior and changed evidence failures.

L563  · intro h

Assumes the actual identity method meets the new successor contract.

L564    have bad := h 0 trivial

At required input zero, this would force actual output zero to equal expected one.

L565    cases bad

Eliminates the impossible 0=1 equality, refuting the changed actual capability claim.

L566  · intro h

Assumes the retained observation singleton nevertheless gives Grounds for that changed claim.

L567    have discharged := (h.2.2 changedObjectiveFacet (by simp)).2.2.2

Extracts the actual changedObjectiveFacet's discharge from that assumed Grounds package.

L568    have bad := discharged.2.1 actual ((observationIdentifies actual).2 rfl) trivial 0 trivial

Its support rule applied to the compatible actual world and input zero yields the same false output equality 0=1.

L569    cases bad

Rejects that equality, proving the specified retained-observation package cannot ground the new claim.

L571/- The very system satisfies the charter while its true cost evidence fails to establish its output capability. -/

Documents the following definition or result: Exhibits this actual charter-compliant system with compatible cost evidence whose specified capability facet is unsupported; other valid grounds can still exist.

L572/-- organon-map CoreReader.Integration.charterNotGrounds

Opens provenance metadata binding CoreReader.Integration.charterNotGrounds to the following source references; this metadata is not a proof premise.

L573organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L574organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L575organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L576-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L577theorem charterNotGrounds :

Exhibits this actual charter-compliant system with compatible cost evidence whose specified capability facet is unsupported; other valid grounds can still exist.

L578    Charter actualSystem actual ∧

The same actual system satisfies all represented Charter conditions.

L579    Compatible [costAllowanceRecord] actual ∧

Its actual world is compatible with the true at-most-two cost observation.

L580    ¬ Grounds capability canonicalArticulation

Nevertheless, that cost evidence does not provide Grounds for its output capability.

L581      (fun f => f = unsupportedCapabilityFacet) [unsupportedCapabilityFacet] := by

The denied Grounds is the particular unsupportedCapabilityFacet singleton, not every possible assessment bundle.

L582  exact ⟨charterChecked, (by intro r hr; cases List.mem_singleton.mp hr; rfl), unsupportedGrounds⟩

Combines charterChecked, direct compatibility of actual with the cost record, and the already proved unsupportedGrounds counterexample.

L584/- A single inhabited system/context carries the charter, its own actual claim and support,

Documents the following definition or result: Constructs one shared system/world satisfying actual judgments, full reflexivity, capability evidence, feasible choice and each interpreted commitment's Grounds; it is a bounded model, not universal philosophical correctness.

L585contentful principle work, and separately reasoned governance commitments. -/

L586/-- organon-map CoreReader.Integration.jointWitness

Opens provenance metadata binding CoreReader.Integration.jointWitness to the following source references; this metadata is not a proof premise.

L587organon.preamble#p1 sha256 2ff45595af647eddc9fc095b3f3854f284bf3740ae7af1bacdb98773ffa44097

Records source reference organon.preamble#p1 with content digest 2ff45595af647eddc9fc095b3f3854f284bf3740ae7af1bacdb98773ffa44097; matching a digest establishes source identity, not semantic fidelity.

L588organon.preamble#p2 sha256 2ff45595af647eddc9fc095b3f3854f284bf3740ae7af1bacdb98773ffa44097

Records source reference organon.preamble#p2 with content digest 2ff45595af647eddc9fc095b3f3854f284bf3740ae7af1bacdb98773ffa44097; matching a digest establishes source identity, not semantic fidelity.

L589organon.charter.overview#p2 sha256 75d7d941d3c07ea748c4a9261d36a75fbd5664ff9c817c4034a9a36a3a12664c

Records source reference organon.charter.overview#p2 with content digest 75d7d941d3c07ea748c4a9261d36a75fbd5664ff9c817c4034a9a36a3a12664c; matching a digest establishes source identity, not semantic fidelity.

L590organon.charter.overview#p3 sha256 75d7d941d3c07ea748c4a9261d36a75fbd5664ff9c817c4034a9a36a3a12664c

Records source reference organon.charter.overview#p3 with content digest 75d7d941d3c07ea748c4a9261d36a75fbd5664ff9c817c4034a9a36a3a12664c; matching a digest establishes source identity, not semantic fidelity.

L591organon.relationships.roles#p1 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L592organon.relationships.roles#p2 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L593organon.relationships.roles#p3 sha256 24b533c77fe93d0570da65ee361893f2c445842f48ee6f315f99f8abc06a0e5e

L594-/

Closes the preceding documentation/provenance comment; it adds no executable code.

L595theorem jointWitness :

Constructs one shared system/world satisfying actual judgments, full reflexivity, capability evidence, feasible choice and each interpreted commitment's Grounds; it is a bounded model, not universal philosophical correctness.

L596    ∃ s : System, ∃ w : World,

Requires an actual system/world pair as the joint witness, so the combined claim is nonempty.

L597      Admissible (systemHeld s) (systemContext s) w ∧ Charter s w ∧

That same pair must be admissible for its jointly held/contextual claims and satisfy its Charter.

L598      OwnCapabilityDuty s w [capabilityFacet] ∧ systemCapability s w ∧

It must also have its own capability duty fulfilled by capabilityFacet and possess the claimed capability.

L599      JustifiedChoice s.requirements (s.method.realize w) objectiveReason ∧

The same realized method must be feasibly chosen under its own requirements using objectiveReason.

L600      (∀ c : Commitment, Grounds (commitmentClaim c) canonicalArticulation

For every one of the five commitments, the corresponding actual adoption claim must have Grounds.

L601        (fun f => f = commitmentFacet c) [commitmentFacet c]) ∧

Each commitment uses its own exact singleton value facet and corresponding applicability.

L602      s = actualSystem ∧ w = actual := by

Finally identifies the witnesses with actualSystem and actual, preventing unrelated existential substitutions.

L603  exact ⟨actualSystem, actual, actualAdmissible, charterChecked,

Chooses that exact pair and supplies its actual admissibility and checked Charter.

L604    ownCapabilityGrounded.1, capabilityActual, identityJustified,

Adds this same system's owned capability duty, actual capability and justified identity choice.

L605    fun c => (reasonsBelongToCommitments c).1, rfl, rfl⟩

Uses each commitment's existing Grounds proof, then closes the two witness-identity equalities by construction.

L607end CoreReader.Integration

Closes the current namespace.

leanified/CoreReader/Integration.lean ​

leanified/CoreReader/Integration.lean