leanified/CoreReader/Engineering/Domain.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 · 902 lines
L1import StdLoads Lean's standard library for lists, arithmetic, strings and decidable finite checks used throughout the model.
L3namespace CoreReader.EngineeringPlaces the application vocabulary and results in CoreReader.Engineering, keeping them distinct from the inherited Core interfaces.
L5/- This is a bounded engineering application model. Work units count explicitThe work numbers count stipulated edit operations in a bounded scenario; they are neither a universal conversion between burdens nor measurements of future engineering performance.
L6operations; they are not a universal exchange rate or empirical forecast. -/The work numbers count stipulated edit operations in a bounded scenario; they are neither a universal conversion between burdens nor measurements of future engineering performance.
L7inductive Maintainer whereThe three maintainer roles distinguish the original author, a successor and an agent, so original-author editability need not imply continuing maintenance capability.
L8 | original | successor | agentThe three maintainer roles distinguish the original author, a successor and an agent, so original-author editability need not imply continuing maintenance capability.
L9 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Maintainer; these support concrete case evaluation, not a philosophical claim about that type.
L10inductive Tool whereThe available operations distinguish editing, compilation, contract checking and migration; a change path must have the required tool available.
L11 | editor | compiler | contractRunner | migrationRunnerThe available operations distinguish editing, compilation, contract checking and migration; a change path must have the required tool available.
L12 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Tool; these support concrete case evaluation, not a philosophical claim about that type.
L13inductive Knowledge whereKnowledge distinguishes private implementation layout from the public contract and documented change/migration guides; these prerequisites will separate maintainer capabilities.
L14 | privateLayout | publicContract | changeGuide | migrationGuideKnowledge distinguishes private implementation layout from the public contract and documented change/migration guides; these prerequisites will separate maintainer capabilities.
L15 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Knowledge; these support concrete case evaluation, not a philosophical claim about that type.
L16inductive Change whereThe change vocabulary includes six major evolution operations, independent/coordinated work, design revision and an open named alternative. The nine-element examples do not exhaust the type.
L17 | addition | replacement | deletion | withdrawal | redrawing | migrationThe change vocabulary includes six major evolution operations, independent/coordinated work, design revision and an open named alternative. The nine-element examples do not exhaust the type.
L18 | independent | coordinated | designRevision | other (name : String)The change vocabulary includes six major evolution operations, independent/coordinated work, design revision and an open named alternative. The nine-element examples do not exhaust the type.
L19 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Change; these support concrete case evaluation, not a philosophical claim about that type.
L20inductive Candidate whereThree candidate designs permit comparison of present simplicity, credible evolution support and extra registered extensibility; their merits are supplied by later behavior and work data.
L21 | presentSimple | evolvable | maximalThree candidate designs permit comparison of present simplicity, credible evolution support and extra registered extensibility; their merits are supplied by later behavior and work data.
L22 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Candidate; these support concrete case evaluation, not a philosophical claim about that type.
L23inductive Burden whereSeven distinct burden dimensions cover understanding, construction, diagnosis, verification, coordination, operation and migration; no sum across them is required.
L24 | understanding | construction | diagnosis | verification | coordinationSeven distinct burden dimensions cover understanding, construction, diagnosis, verification, coordination, operation and migration; no sum across them is required.
L25 | operation | migrationSeven distinct burden dimensions cover understanding, construction, diagnosis, verification, coordination, operation and migration; no sum across them is required.
L26 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Burden; these support concrete case evaluation, not a philosophical claim about that type.
L28def maintainers : List Maintainer := [.original, .successor, .agent]The concrete activity includes all three maintainer roles, making successor and agent claims nonvacuous.
L29def changes : List Change := [.addition, .replacement, .deletion, .withdrawal,Registers nine ordinary changes for the finite examples; named other changes can still be represented separately.
L30 .redrawing, .migration, .independent, .coordinated, .designRevision]Registers nine ordinary changes for the finite examples; named other changes can still be represented separately.
L31def burdens : List Burden := [.understanding, .construction, .diagnosis,Lists every represented cost dimension so threat searches examine each dimension independently.
L32 .verification, .coordination, .operation, .migration]Lists every represented cost dimension so threat searches examine each dimension independently.
L34structure Activity whereAn engineering activity groups the people or agents, software, tools, knowledge and lifecycle expectations relevant to a capability claim.
L35 participants : List MaintainerRecords the maintainers participating in this activity; membership is later required for individual change capability.
L36 software : StringIdentifies the software being maintained; this identity also binds later revision reports to their task.
L37 tools : List ToolRecords available tools rather than assuming every requested tool exists.
L38 available : Maintainer → List KnowledgeAssigns knowledge separately to each maintainer, allowing an original author to know private details unavailable to successors.
L39 scheduledReleases : NatCounts scheduled releases as one concrete indicator of continuing development expectations.
L40 scheduledMaintenance : NatCounts scheduled maintenance work independently of releases.
L41 boundedRuns : Option NatAn optional finite run bound represents genuinely bounded use; absence of a bound alone is not the definition of continuing activity.
L42 label : StringKeeps a descriptive label separate from lifecycle facts, allowing the misleading label temporary to be tested.
L44/-- organon-map CoreReader.Engineering.ActivityScopeBegins a provenance comment attaching CoreReader.Engineering.ActivityScope to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L45software-engineering.purpose#p1 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p1 for CoreReader.Engineering.ActivityScope, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L46software-engineering.purpose#p2 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p2 for CoreReader.Engineering.ActivityScope, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L47software-engineering.purpose#p3 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p3 for CoreReader.Engineering.ActivityScope, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L48-/Closes the source-mapping comment for CoreReader.Engineering.ActivityScope; executable declarations resume after the comment.
L49abbrev ActivityScope (a : Activity) : Prop :=Activity scope is a concrete admissibility condition for the engineering subject, rather than an intrinsic intention attributed to code.
L50 a.participants ≠ [] ∧ a.software ≠ "" ∧ a.tools ≠ [] ∧Requires actual participants, a nonempty software identifier and some available tools.
L51 a.participants.all (fun m => !(a.available m).isEmpty) = trueEvery listed maintainer must have some available knowledge; this does not yet show the knowledge suffices for every change.
L53abbrev Continuing (a : Activity) : Prop :=Continuing activity means both planned releases and maintenance are positive in this model; the name of the activity is irrelevant.
L54 0 < a.scheduledReleases ∧ 0 < a.scheduledMaintenanceContinuing activity means both planned releases and maintenance are positive in this model; the name of the activity is irrelevant.
L56abbrev BoundedLifecycle (a : Activity) : Prop :=A bounded lifecycle requires a declared finite run limit and zero planned releases and maintenance; a temporary label alone cannot satisfy it.
L57 a.boundedRuns.isSome = true ∧ a.scheduledReleases = 0 ∧A bounded lifecycle requires a declared finite run limit and zero planned releases and maintenance; a temporary label alone cannot satisfy it.
L58 a.scheduledMaintenance = 0A bounded lifecycle requires a declared finite run limit and zero planned releases and maintenance; a temporary label alone cannot satisfy it.
L60def continuingActivity : Activity := {The continuing queue activity includes all maintainers and all four tools; its software identity is the order-preserving queue.
L61 participants := maintainers, software := "order-preserving queue",The continuing queue activity includes all maintainers and all four tools; its software identity is the order-preserving queue.
L62 tools := [.editor, .compiler, .contractRunner, .migrationRunner],The continuing queue activity includes all maintainers and all four tools; its software identity is the order-preserving queue.
L63 available := fun m => match m withOnly the original maintainer receives privateLayout. Successors and agents have public contracts and guides, creating a real prerequisite difference.
L64 | .original => [.privateLayout, .publicContract, .changeGuide, .migrationGuide]Only the original maintainer receives privateLayout. Successors and agents have public contracts and guides, creating a real prerequisite difference.
L65 | _ => [.publicContract, .changeGuide, .migrationGuide],Only the original maintainer receives privateLayout. Successors and agents have public contracts and guides, creating a real prerequisite difference.
L66 scheduledReleases := 3, scheduledMaintenance := 6,The activity schedules three releases and six maintenance units, so both continuing-lifecycle indicators are positive.
L67 boundedRuns := none, label := "temporary" }There is no finite run bound even though the descriptive label says temporary; later cases reject that label as evidence of a bounded lifecycle.
L69def temporaryActivity : Activity := { continuingActivity withThe one-shot variant removes all planned releases and maintenance and sets a single-run limit, creating a genuinely bounded example.
L70 scheduledReleases := 0, scheduledMaintenance := 0, boundedRuns := some 1,The one-shot variant removes all planned releases and maintenance and sets a single-run limit, creating a genuinely bounded example.
L71 label := "one-shot import" }The one-shot variant removes all planned releases and maintenance and sets a single-run limit, creating a genuinely bounded example.
L72def prototypeActivity : Activity := { temporaryActivity withThe prototype retains the zero-maintenance bounded setup but allows four runs.
L73 boundedRuns := some 4, label := "bounded prototype" }The prototype retains the zero-maintenance bounded setup but allows four runs.
L74def retiringActivity : Activity := { temporaryActivity withThe retiring service uses the same bounded setup with two remaining runs.
L75 boundedRuns := some 2, label := "retiring service" }The retiring service uses the same bounded setup with two remaining runs.
L77structure EditStep whereEach edit step records where work occurs, which knowledge and tool it needs, and its assigned work units.
L78 component : NatIdentifies the component touched by this work step.
L79 requires : KnowledgeStates the knowledge prerequisite that the acting maintainer must possess.
L80 tool : ToolStates the tool needed for this step.
L81 units : NatAssigns a natural-number cost to this explicit operation; later totals sum these units.
L82 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for EditStep; these support concrete case evaluation, not a philosophical claim about that type.
L84def changePath (c : Candidate) (d : Change) : List EditStep :=Builds an explicit work path for a candidate and intended change, rather than assigning capability from a design label.
L85 let guide := if c = .presentSimple then Knowledge.privateLayout else .changeGuidePresentSimple requires private layout knowledge; the other designs use the change guide, which successors possess.
L86 let base : List EditStep := [⟨0, guide, .editor, 1⟩,Every ordinary path starts with one edit at component 0 and one public-contract check there, each costing one unit.
L87 ⟨0, .publicContract, .contractRunner, 1⟩]Every ordinary path starts with one edit at component 0 and one public-contract check there, each costing one unit.
L88 match d withDispatch on the requested Change to choose its corresponding editing path; the following branches distinguish the different directions.
L89 | .addition | .independent => baseAddition and independent change use only that two-unit base path.
L90 | .replacement | .deletion => base ++ [⟨1, guide, .compiler, 1⟩]Replacement and deletion add a one-unit compilation at component 1 using the design's selected guide.
L91 | .coordinated => base ++ [⟨1, guide, .compiler, 3⟩, ⟨2, .publicContract, .contractRunner, 3⟩]Coordinated change adds compilation at component 1 and public-contract verification at component 2, each costing three units.
L92 | .migration => base ++ [⟨1, .migrationGuide, .migrationRunner, 8⟩]Migration adds an eight-unit migration-runner step requiring the migration guide.
L93 | .withdrawal | .redrawing | .designRevision =>Withdrawal, boundary redrawing and design revision branch on the selected design; this is where simplicity and evolution have different work paths.
L94 if c = .presentSimple then base ++Withdrawal, boundary redrawing and design revision branch on the selected design; this is where simplicity and evolution have different work paths.
L95 [⟨1, guide, .editor, 5⟩, ⟨2, guide, .compiler, 5⟩,The simple design adds private-guide edit and compilation plus a public-contract check, each costing five units, bringing total work to seventeen.
L96 ⟨2, .publicContract, .contractRunner, 5⟩]The simple design adds private-guide edit and compilation plus a public-contract check, each costing five units, bringing total work to seventeen.
L97 else base ++ [⟨1, guide, .editor, 2⟩, ⟨1, .publicContract, .contractRunner, 2⟩]Other designs instead add a two-unit edit and two-unit public-contract check at component 1, totaling six units with the base.
L98 | .other name =>The open change constructor receives a concrete special case only for csv export.
L99 if name = "csv export" thenThe open change constructor receives a concrete special case only for csv export.
L100 if c = .maximal then base ++ [⟨3, .migrationGuide, .compiler, 2⟩]Maximal handles CSV export with a documented migration-guide compilation at component 3 costing two extra units.
L101 else base ++ [⟨3, .privateLayout, .compiler, 20⟩]Other designs require privateLayout and twenty extra compilation units for CSV export, so a successor lacks that path's prerequisite.
L102 else []Unrecognized names receive no path; the nonempty-path requirement prevents vacuous capability from an empty list.
L104def changeWork (c : Candidate) (d : Change) : Nat :=Total work is the sum of the actual path steps' assigned units, not the number of modules or extension points.
L105 ((changePath c d).map EditStep.units).sumTotal work is the sum of the actual path steps' assigned units, not the number of modules or extension points.
L107abbrev CanChange (a : Activity) (c : Candidate) (m : Maintainer) (d : Change) : Prop :=Individual change capability is indexed by the actual activity, design, maintainer and intended change.
L108 (changePath c d) ≠ [] ∧ m ∈ a.participants ∧ (changePath c d).allCapability requires a nonempty path, participating maintainer, and every path step's knowledge and tool prerequisites; a failed prerequisite blocks the claim.
L109 (fun step => (a.available m).contains step.requires && a.tools.contains step.tool) = trueCapability requires a nonempty path, participating maintainer, and every path step's knowledge and tool prerequisites; a failed prerequisite blocks the claim.
L111abbrev ContinuingCapability (a : Activity) (c : Candidate) (d : Change) : Prop :=Continuing capability requires a nonempty path executable with the knowledge and tools of every listed maintainer; activity scope supplies the separate nonempty-participant condition.
L112 (changePath c d) ≠ [] ∧ a.participants.all (fun m => (changePath c d).allContinuing capability requires a nonempty path executable with the knowledge and tools of every listed maintainer; activity scope supplies the separate nonempty-participant condition.
L113 (fun step => (a.available m).contains step.requires && a.tools.contains step.tool)) = trueContinuing capability requires a nonempty path executable with the knowledge and tools of every listed maintainer; activity scope supplies the separate nonempty-participant condition.
L115/- Maximal is maximal only on this explicitly registered finite set. TheMaximality will concern only a registered finite direction set. CSV has concrete work and state content; unsupported names cannot acquire capability from an empty path.
L116extra CSV direction has an actual documented compilation path and later stateMaximality will concern only a registered finite direction set. CSV has concrete work and state content; unsupported names cannot acquire capability from an empty path.
L117transformation; unsupported names do not gain a capability from an empty path. -/Maximality will concern only a registered finite direction set. CSV has concrete work and state content; unsupported names cannot acquire capability from an empty path.
L118def registeredDirections : List Change := changes ++ [.other "csv export"]Adds the named CSV export direction to the nine ordinary changes, producing ten registered directions.
L119def supportedDirections (a : Activity) (c : Candidate) : List Change :=Keeps exactly those registered directions that every continuing maintainer can execute for the chosen design.
L120 registeredDirections.filter (fun d => decide (ContinuingCapability a c d))Keeps exactly those registered directions that every continuing maintainer can execute for the chosen design.
L121abbrev MaximumRegisteredCapability (a : Activity) (c : Candidate) : Prop :=A candidate has maximum registered capability when it supports every direction in that fixed list; this is not maximality over every conceivable change.
L122 registeredDirections.all (fun d => decide (ContinuingCapability a c d)) = trueA candidate has maximum registered capability when it supports every direction in that fixed list; this is not maximality over every conceivable change.
L124/- A software value here is a passive function: no intention is stored in it.The passive software function is separated from maintainers' selected intentions; the example does not attribute generative orientation to every artifact.
L125An engineering intention is an agent's selected set of changes. -/The passive software function is separated from maintainers' selected intentions; the example does not attribute generative orientation to every artifact.
L126def passiveArtifact (xs : List Nat) : List Nat := xsThe artifact returns its input unchanged and makes no change proposal.
L128def orientation : Maintainer → List Change := fun _ => [.designRevision, .migration]Each represented maintainer intends design revision and migration; this is the activity's explicit selected intention.
L130inductive EngineeringAction whereActions distinguish proposing a change from executing software to obtain an output list.
L131 | propose (direction : Change)Actions distinguish proposing a change from executing software to obtain an output list.
L132 | execute (result : List Nat)Actions distinguish proposing a change from executing software to obtain an output list.
L133 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for EngineeringAction; these support concrete case evaluation, not a philosophical claim about that type.
L135def maintainerActions (m : Maintainer) : List EngineeringAction :=Maintainer intentions become actual propose actions for each selected direction.
L136 (orientation m).map EngineeringAction.proposeMaintainer intentions become actual propose actions for each selected direction.
L138def artifactActions (input : List Nat) : List EngineeringAction :=The artifact's only action executes its passive function; the action list contains no proposal constructor.
L139 [.execute (passiveArtifact input)]The artifact's only action executes its passive function; the action list contains no proposal constructor.
L141/-- organon-map CoreReader.Engineering.subjectLifecycleCasesBegins a provenance comment attaching CoreReader.Engineering.subjectLifecycleCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L142software-engineering.purpose#p1 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p1 for CoreReader.Engineering.subjectLifecycleCases, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L143software-engineering.purpose#p2 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p2 for CoreReader.Engineering.subjectLifecycleCases, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L144software-engineering.purpose#p3 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p3 for CoreReader.Engineering.subjectLifecycleCases, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L145-/Closes the source-mapping comment for CoreReader.Engineering.subjectLifecycleCases; executable declarations resume after the comment.
L146theorem subjectLifecycleCases :Collects concrete positive scope, maintainer-capability and lifecycle cases for the shared queue activity.
L147 ActivityScope continuingActivity ∧The continuing activity satisfies the nonempty engineering-subject scope condition.
L148 CanChange continuingActivity .evolvable .successor .designRevision ∧The successor has the tools and public knowledge needed for evolvable design revision.
L149 CanChange continuingActivity .evolvable .agent .designRevision ∧The agent also has the prerequisites for that same design revision.
L150 continuingActivity.label = "temporary" ∧ Continuing continuingActivity ∧The concrete activity remains continuing even while carrying the temporary label.
L151 ¬ BoundedLifecycle continuingActivity ∧ BoundedLifecycle temporaryActivity ∧The continuing activity is not bounded, while the one-shot, prototype and retiring variants meet their explicit finite lifecycle conditions.
L152 BoundedLifecycle prototypeActivity ∧ BoundedLifecycle retiringActivity := by decideThe continuing activity is not bounded, while the one-shot, prototype and retiring variants meet their explicit finite lifecycle conditions. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L154/-- organon-map CoreReader.Engineering.subjectLimitsBegins a provenance comment attaching CoreReader.Engineering.subjectLimits to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L155software-engineering.purpose#p1 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p1 for CoreReader.Engineering.subjectLimits, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L156software-engineering.purpose#p2 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p2 for CoreReader.Engineering.subjectLimits, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L157software-engineering.purpose#p3 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p3 for CoreReader.Engineering.subjectLimits, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L158-/Closes the source-mapping comment for CoreReader.Engineering.subjectLimits; executable declarations resume after the comment.
L159theorem subjectLimits :Collects counterexamples to inferring continuing capability or software intention from weaker facts.
L160 CanChange continuingActivity .presentSimple .original .designRevision ∧The original maintainer can revise the simple design because private layout knowledge is available to that maintainer.
L161 ¬ CanChange continuingActivity .presentSimple .successor .designRevision ∧The successor cannot perform that same simple-design revision because the private prerequisite is absent.
L162 ¬ ContinuingCapability continuingActivity .presentSimple .designRevision ∧Consequently the simple design does not support this revision for every continuing maintainer.
L163 continuingActivity.label = "temporary" ∧ ¬ BoundedLifecycle continuingActivity ∧The temporary label coexists with failure of the actual bounded-lifecycle condition.
L164 orientation .agent ≠ [] ∧ passiveArtifact [2, 1] = [2, 1] ∧The agent's intention is nonempty, while the passive artifact still merely returns [2,1].
L165 EngineeringAction.propose .designRevision ∈ maintainerActions .agent ∧A design-revision proposal occurs among agent actions but not among the artifact's execution actions.
L166 EngineeringAction.propose .designRevision ∉ artifactActions [2, 1] := by decideA design-revision proposal occurs among agent actions but not among the artifact's execution actions. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L168/- Ground is intentionally parameterized: the examples below do not exhaustCredibility is parameterized by an articulability test and a support relation; the following examples do not validate every possible supplied relation.
L169possible sources of credibility. The supplied support relation needs review. -/Credibility is parameterized by an articulability test and a support relation; the following examples do not validate every possible supplied relation.
L170/-- organon-map CoreReader.Engineering.CredibleDirectionBegins a provenance comment attaching CoreReader.Engineering.CredibleDirection to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L171software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.CredibleDirection, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L172software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.CredibleDirection, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L173-/Closes the source-mapping comment for CoreReader.Engineering.CredibleDirection; executable declarations resume after the comment.
L174abbrev CredibleDirection {Ground : Type} (grounds : List Ground)Allows any ground type, preserving an open set of possible credibility sources.
L175 (articulated : Ground → Bool) (supports : Ground → Change → Bool)The application supplies separate tests for whether a ground is articulated and whether it supports the intended direction.
L176 (d : Change) : Prop :=A direction is credible here when at least one listed ground passes both tests for that same direction.
L177 grounds.any (fun g => articulated g && supports g d) = trueA direction is credible here when at least one listed ground passes both tests for that same direction.
L179inductive DirectionGround whereThe concrete examples instantiate ground records without making these constructors an exhaustive philosophical taxonomy.
L180 | plan (release : Nat) (committed : List Change)A plan records a release number and committed changes.
L181 | knowledge (service : String) (affected : List Change) (mechanism : String)Domain knowledge records the relevant service, affected changes and a mechanism account.
L182 | history (service : String) (observed : List Change)History records a service and observed change directions.
L183 | other (account : String) (supported : List Change)An other constructor keeps room for a separately articulated account and its supported changes.
L184 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for DirectionGround; these support concrete case evaluation, not a philosophical claim about that type.
L186def articulateGround : DirectionGround → BoolChecks the concrete ground records for the identifying content required by this application.
L187 | .plan release ds => release > 0 && !ds.isEmptyA plan must name a positive release and at least one committed direction.
L188 | .knowledge service ds mechanism => service != "" && !ds.isEmpty && mechanism != ""Knowledge must identify a service, some affected directions and a nonempty mechanism account.
L189 | .history service ds => service != "" && !ds.isEmptyA history needs a named service and some observations.
L190 | .other account ds => account != "" && !ds.isEmptyAn other ground needs a nonempty account and direction list.
L192def supportGround : DirectionGround → Change → BoolInterprets support according to this bounded application's concrete records, rather than deriving arbitrary real-world relevance from strings.
L193 | .plan release ds, d => release > 0 && ds.contains dA positive-release plan supports a direction only when it explicitly contains that direction.
L194 | .knowledge service ds mechanism, d =>The designated queue knowledge supports listed directions when its mechanism is tenant-config-reload; this named mechanism is an application interpretation.
L195 service == "queue" && mechanism == "tenant-config-reload" && ds.contains dThe designated queue knowledge supports listed directions when its mechanism is tenant-config-reload; this named mechanism is an application interpretation.
L196 | .history service ds, d => service == "queue" && (ds.filter (· == d)).length >= 2A queue history supports a direction when it occurs at least twice in the recorded list; this is a chosen finite support rule.
L197 | .other account ds, d => account == "reviewed customer migration requirement" && ds.contains dThe particular reviewed customer migration account supports only directions listed in that account.
L199abbrev initialGrounds : List DirectionGround := [.plan 2 [.designRevision, .migration]]The initial grounds commit release 2 to design revision and migration.
L200def forecastGrounds : List DirectionGround := [.plan 3 [.deletion]]The revised forecast commits release 3 to deletion instead.
L201abbrev credible (gs : List DirectionGround) (d : Change) : Prop :=Specializes generic credibility to DirectionGround using the concrete articulation and support interpretations above.
L202 CredibleDirection gs articulateGround supportGround dSpecializes generic credibility to DirectionGround using the concrete articulation and support interpretations above.
L204abbrev WarrantedAccommodation (gs : List DirectionGround) (d : Change)The chosen accommodation test requires credible direction, positive objective gain and investment no greater than that gain; it is a local sufficient criterion, not a universal numerical exchange rule.
L205 (objectiveGain investment : Nat) : Prop :=The chosen accommodation test requires credible direction, positive objective gain and investment no greater than that gain; it is a local sufficient criterion, not a universal numerical exchange rule.
L206 credible gs d ∧ 0 < objectiveGain ∧ investment ≤ objectiveGainThe chosen accommodation test requires credible direction, positive objective gain and investment no greater than that gain; it is a local sufficient criterion, not a universal numerical exchange rule.
L208/-- organon-map CoreReader.Engineering.credibilityCasesBegins a provenance comment attaching CoreReader.Engineering.credibilityCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L209software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.credibilityCases, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L210software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.credibilityCases, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L211-/Closes the source-mapping comment for CoreReader.Engineering.credibilityCases; executable declarations resume after the comment.
L212theorem credibilityCases :Bundles positive plan, knowledge and history support with unsupported-imagination and revised-forecast contrasts.
L213 credible initialGrounds .designRevision ∧The actual release-2 plan supports design revision.
L214 credible [.knowledge "queue" [.designRevision] "tenant-config-reload"] .designRevision ∧The designated queue mechanism provides the declared knowledge support for design revision.
L215 credible [.history "queue" [.migration, .migration]] .migration ∧Two recorded queue migrations meet the concrete historical support criterion.
L216 ¬ credible [] (.other "quantum backend") ∧An empty ground list does not support an imagined quantum backend.
L217 credible forecastGrounds .deletion ∧ ¬ credible forecastGrounds .designRevision := by decideThe changed forecast supports deletion and no longer supports design revision. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L219def abstractionComplexity : Candidate → NatAssigns present abstraction complexity 1, 3 and 30 to simple, evolvable and maximal candidates; these are scenario parameters.
L220 | .presentSimple => 1 | .evolvable => 3 | .maximal => 30Assigns present abstraction complexity 1, 3 and 30 to simple, evolvable and maximal candidates; these are scenario parameters.
L222def implementedVariants : List Candidate := [.presentSimple]Only the simple candidate is currently implemented, allowing credibility without multiple existing implementations.
L224/- No scalar conversion across burden dimensions is used by the priority rule. -/The priority rule compares each burden against its own capacity instead of converting them into one score.
L225structure CostVector whereA cost vector can assign a separate natural-number amount to each burden; this auxiliary structure does not force aggregation.
L226 amount : Burden → NatA cost vector can assign a separate natural-number amount to each burden; this auxiliary structure does not force aggregation.
L227structure CostLimits whereCost limits pair a capacity with an identified objective for each burden, so a claimed threat must concern something concrete.
L228 capacity : Burden → NatCost limits pair a capacity with an identified objective for each burden, so a claimed threat must concern something concrete.
L229 objective : Burden → StringCost limits pair a capacity with an identified objective for each burden, so a claimed threat must concern something concrete.
L231def cost : Candidate → Burden → NatEvery burden of the simple baseline costs one unit in this scenario.
L232 | .presentSimple, _ => 1Every burden of the simple baseline costs one unit in this scenario.
L233 | .evolvable, .understanding => 3Evolvable understanding cost is three units.
L234 | .evolvable, .construction => 4Evolvable construction cost is four units.
L235 | .evolvable, .diagnosis => 2Evolvable diagnosis cost is two units.
L236 | .evolvable, .verification => 4Evolvable verification cost is four units.
L237 | .evolvable, .coordination => 2Evolvable coordination cost is two units.
L238 | .evolvable, .operation => 2Evolvable operational cost is two units.
L239 | .evolvable, .migration => 8Evolvable migration cost is eight units, illustrating a burden that need not be cheap.
L240 | .maximal, _ => 40The maximal candidate costs forty units in every represented burden.
L242def normalLimits : CostLimits := {The ordinary context has capacity twelve for each burden, enough for the evolvable candidate's assigned costs.
L243 capacity := fun _ => 12,The ordinary context has capacity twelve for each burden, enough for the evolvable candidate's assigned costs.
L244 objective := fun b => match b withAssign each Burden its objective name by matching on the burden; the following branches supply the distinct engineering objectives.
L245 | .understanding => "successor onboarding capacity"The understanding limit concerns successor onboarding capacity.
L246 | .construction => "release construction capacity"Construction capacity is tied to preparing a release.
L247 | .diagnosis => "incident diagnosis window"Diagnosis capacity concerns the incident diagnosis window.
L248 | .verification => "release verification capacity"Verification capacity concerns checking a release.
L249 | .coordination => "available team coordination"Coordination capacity concerns available teamwork.
L250 | .operation => "runtime resource budget"Operational capacity concerns the runtime resource budget.
L251 | .migration => "retirement migration capacity" }Migration capacity concerns eventual retirement migration.
L253structure Requirements whereNecessary requirements remain separate from the value preference for evolution.
L254 orderRequired : BoolIndicates whether the identified output-order contract is required.
L255 maxUnsafeOperations : NatBounds the permitted number of unsafe operations.
L256 maxLatency : NatBounds observed latency.
L257 minRetention : NatSets the required minimum retention.
L259def normalRequirements : Requirements := ⟨true, 0, 10, 30⟩The ordinary requirements demand order, zero unsafe operations, latency at most ten and retention at least thirty.
L260def behavior : Candidate → List Nat → List Nat := fun _ xs => xs.eraseDupsAll three candidate behaviors remove duplicate list values in the given order; this local equality does not equate their maintenance paths or costs.
L262/- Candidate profiles are observations in this bounded scenario. ModifiedProfiles are observations stipulated for this scenario; later variants independently violate each of the four requirement gates.
L263profiles below test all four independent necessary-requirement gates. -/Profiles are observations stipulated for this scenario; later variants independently violate each of the four requirement gates.
L264structure CandidateProfile whereA profile records the four behavior/safety/performance quantities relevant to these requirements.
L265 orderOutput : List NatStores the output observed on the identified order test.
L266 unsafeOperations : NatStores the number of unsafe operations in this profile.
L267 latency : NatStores this profile's latency observation.
L268 retention : NatStores this profile's retention observation.
L270def profile (c : Candidate) : CandidateProfile := ⟨behavior c [2, 1, 2], 0, 5, 30⟩Each original profile observes de-duplication on [2,1,2], zero unsafe operations, latency five and retention thirty.
L271abbrev Meets (r : Requirements) (p : CandidateProfile) : Prop :=Meeting requirements checks the order result [2,1] whenever order is required; it does not impose order when the requirement is disabled.
L272 (r.orderRequired = true → p.orderOutput = [2, 1]) ∧Meeting requirements checks the order result [2,1] whenever order is required; it does not impose order when the requirement is disabled.
L273 p.unsafeOperations ≤ r.maxUnsafeOperations ∧ p.latency ≤ r.maxLatency ∧Safety and latency must stay at or below their maxima, and retention must reach its minimum.
L274 r.minRetention ≤ p.retentionSafety and latency must stay at or below their maxima, and retention must reach its minimum.
L276structure Context whereA context binds the activity, requirements, evidence, costs and selected departure account used by the domain norm.
L277 activity : ActivityCarries the actual engineering activity and its maintainer conditions.
L278 required : RequirementsCarries the relevant necessary requirements.
L279 evidence : List DirectionGroundCarries the grounds for credible future directions.
L280 limits : CostLimitsCarries per-burden objective capacities.
L281 departure : Option BurdenOptionally identifies the burden used to justify departing from evolution priority.
L282 profiles : Candidate → CandidateProfile := profileProvides candidate observations, defaulting to the ordinary profiles but allowing explicit test variants.
L284def currentContinuing : Context := {The shared ordinary context uses the continuing queue, normal requirements, release-2 grounds and capacity-twelve limits, with no claimed departure.
L285 activity := continuingActivity, required := normalRequirements,The shared ordinary context uses the continuing queue, normal requirements, release-2 grounds and capacity-twelve limits, with no claimed departure.
L286 evidence := initialGrounds, limits := normalLimits, departure := none }The shared ordinary context uses the continuing queue, normal requirements, release-2 grounds and capacity-twelve limits, with no claimed departure.
L288abbrev ConcreteThreat (ctx : Context) (c : Candidate) (b : Burden) : Prop :=A concrete threat requires added cost above both the simple baseline and the named objective's capacity; naming a burden without those inequalities is insufficient.
L289 cost .presentSimple b < cost c b ∧ ctx.limits.capacity b < cost c b ∧A concrete threat requires added cost above both the simple baseline and the named objective's capacity; naming a burden without those inequalities is insufficient.
L290 ctx.limits.objective b ≠ ""A concrete threat requires added cost above both the simple baseline and the named objective's capacity; naming a burden without those inequalities is insufficient.
L292abbrev HasThreat (ctx : Context) (c : Candidate) : Prop :=A threat exists if one of the seven represented burden dimensions meets the concrete-threat condition.
L293 burdens.any (fun b => decide (ConcreteThreat ctx c b)) = trueA threat exists if one of the seven represented burden dimensions meets the concrete-threat condition.
L295/-- organon-map CoreReader.Engineering.JustifiedDepartureBegins a provenance comment attaching CoreReader.Engineering.JustifiedDeparture to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L296software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.JustifiedDeparture, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L297-/Closes the source-mapping comment for CoreReader.Engineering.JustifiedDeparture; executable declarations resume after the comment.
L298abbrev JustifiedDeparture (ctx : Context) (c : Candidate) : Prop :=Define justified departure for this context and candidate through a recorded burden whose concrete cost threat must hold.
L299 match ctx.departure withInspect this same context’s departure option to distinguish an absent explanation from a named burden.
L300 | none => FalseWith no recorded departure burden, justification is False; absence supplies no exception.
L301 | some b => ConcreteThreat ctx c bFor the recorded burden b, require ConcreteThreat for this exact context, candidate and burden.
L303instance (ctx : Context) (c : Candidate) : Decidable (JustifiedDeparture ctx c) := bySupplies a decision procedure for the departure proposition so finite examples can be checked by computation.
L304 unfold JustifiedDepartureExposes the match on the optional selected burden in JustifiedDeparture.
L305 split <;> infer_instanceSplits none versus some burden and lets Lean obtain decidability of False or the concrete arithmetic/string condition.
L307abbrev PriorityConditions (ctx : Context) : Prop :=Priority applicability is a conjunction of lifecycle, feasibility, credibility and actual comparative capability conditions.
L308 Continuing ctx.activity ∧ ActivityScope ctx.activity ∧Requires a continuing activity with a valid engineering-subject scope.
L309 Meets ctx.required (ctx.profiles .presentSimple) ∧ Meets ctx.required (ctx.profiles .evolvable) ∧Both simple and evolvable alternatives must satisfy the same context's necessary requirements.
L310 credible ctx.evidence .designRevision ∧The context must contain credible grounds for design revision, not merely an imagined addition.
L311 ContinuingCapability ctx.activity .evolvable .designRevision ∧Every continuing maintainer must be able to perform that design revision with evolvable.
L312 changeWork .evolvable .designRevision < changeWork .presentSimple .designRevision ∧The actual design-revision path must cost less work in evolvable than in simple.
L313 abstractionComplexity .presentSimple < abstractionComplexity .evolvableEvolvable must incur more present abstraction complexity, making the intended tradeoff nontrivial.
L315/-- organon-map CoreReader.Engineering.EvolutionPriorityBegins a provenance comment attaching CoreReader.Engineering.EvolutionPriority to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L316software-engineering.purpose#p3 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p3 for CoreReader.Engineering.EvolutionPriority, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L317software-engineering.evolution-priority#p1 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p1 for CoreReader.Engineering.EvolutionPriority, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L318software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.EvolutionPriority, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L319software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.EvolutionPriority, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L320-/Closes the source-mapping comment for CoreReader.Engineering.EvolutionPriority; executable declarations resume after the comment.
L321abbrev EvolutionPriority (ctx : Context) (chosen : Candidate) : Prop :=This is the adopted defeasible priority: when all applicability conditions hold, select evolvable unless its added cost has an explicitly justified departure. It is not deduced from those facts alone.
L322 PriorityConditions ctx → chosen = .evolvable ∨ JustifiedDeparture ctx .evolvableThis is the adopted defeasible priority: when all applicability conditions hold, select evolvable unless its added cost has an explicitly justified departure. It is not deduced from those facts alone.
L324theorem currentPriorityConditions : PriorityConditions currentContinuing := by decideComputes that the ordinary shared context satisfies all priority conditions. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L325theorem currentNoThreat : ¬ HasThreat currentContinuing .evolvable ∧Computes that the ordinary evolvable costs threaten no represented objective and support no claimed departure.
L326 ¬ JustifiedDeparture currentContinuing .evolvable := by decideComputes that the ordinary evolvable costs threaten no represented objective and support no claimed departure. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L328def threatened (b : Burden) : Context := { currentContinuing withThe threatened variant lowers only the selected burden's capacity to one and records that burden as the departure reason; other capacities remain twelve.
L329 limits := { normalLimits with capacity := fun x => if x = b then 1 else 12 },The threatened variant lowers only the selected burden's capacity to one and records that burden as the departure reason; other capacities remain twelve.
L330 departure := some b }The threatened variant lowers only the selected burden's capacity to one and records that burden as the departure reason; other capacities remain twelve.
L332/-- organon-map CoreReader.Engineering.priorityWhenApplicableBegins a provenance comment attaching CoreReader.Engineering.priorityWhenApplicable to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L333software-engineering.evolution-priority#p1 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p1 for CoreReader.Engineering.priorityWhenApplicable, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L334software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.priorityWhenApplicable, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L335software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.priorityWhenApplicable, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L336-/Closes the source-mapping comment for CoreReader.Engineering.priorityWhenApplicable; executable declarations resume after the comment.
L337theorem priorityWhenApplicable (ctx : Context) (chosen : Candidate)The conditional result ranges over any context and chosen candidate in this application vocabulary.
L338 (rule : EvolutionPriority ctx chosen) (applicable : PriorityConditions ctx)Assumes both adoption of the priority rule and actual applicability; neither premise is derived merely from the theorem statement.
L339 (noDeparture : ¬ JustifiedDeparture ctx .evolvable) :Also assumes there is no justified cost departure.
L340 chosen = .evolvable ∧Under those premises, the choice must be evolvable and therefore carry the stated extra abstraction complexity.
L341 abstractionComplexity .presentSimple < abstractionComplexity chosen := byUnder those premises, the choice must be evolvable and therefore carry the stated extra abstraction complexity.
L342 have hc := (rule applicable).resolve_right noDepartureApplies the adopted implication to actual conditions and eliminates its departure alternative using noDeparture.
L343 exact ⟨hc, hc ▸ applicable.2.2.2.2.2.2.2⟩Pairs the resulting choice equality with the applicability premise's final complexity inequality, substituting the actual chosen candidate.
L345theorem currentSimpleViolates : ¬ EvolutionPriority currentContinuing .presentSimple := byShows that choosing simple in the ordinary applicable, no-threat context violates the adopted evolution priority.
L346 intro hTemporarily assumes the simple choice satisfies the rule in order to derive a contradiction.
L347 have bad := (h currentPriorityConditions).resolve_right currentNoThreat.2Actual applicability activates that rule, and absence of departure forces the impossible simple=evolvable equality.
L348 cases badEliminates equality between distinct candidate constructors, completing the negative result.
L350def withEvolvableProfile (p : CandidateProfile) : Context := { currentContinuing withReplaces only evolvable's observed profile while preserving the other candidate profiles and context, isolating a necessary-requirement variation.
L351 profiles := fun c => if c = .evolvable then p else profile c }Replaces only evolvable's observed profile while preserving the other candidate profiles and context, isolating a necessary-requirement variation.
L353theorem unmetRequirementsBlockPriority :Check that each of the four displayed requirement failures makes PriorityConditions false. This only disables priority activation: EvolutionPriority and the later DomainSatisfied do not impose an unconditional Meets rejection.
L354 ¬ PriorityConditions (withEvolvableProfile { profile .evolvable with orderOutput := [1, 2] }) ∧Changing the observed order from [2,1] to [1,2] invalidates priority applicability.
L355 ¬ PriorityConditions (withEvolvableProfile { profile .evolvable with unsafeOperations := 1 }) ∧One unsafe operation exceeds the permitted zero and invalidates applicability.
L356 ¬ PriorityConditions (withEvolvableProfile { profile .evolvable with latency := 11 }) ∧Latency eleven exceeds the limit ten and invalidates applicability.
L357 ¬ PriorityConditions (withEvolvableProfile { profile .evolvable with retention := 29 }) := byRetention twenty-nine falls below thirty and invalidates applicability.
L358 simp [PriorityConditions, withEvolvableProfile, currentContinuing, Meets,Simplifies applicability, the altered profile and requirement predicates; each branch reduces to its explicit failed equality or numerical bound.
L359 normalRequirements]Simplifies applicability, the altered profile and requirement predicates; each branch reduces to its explicit failed equality or numerical bound.
L361/-- organon-map CoreReader.Engineering.priorityConditionsCasesBegins a provenance comment attaching CoreReader.Engineering.priorityConditionsCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L362software-engineering.purpose#p3 sha256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60bRecords the source reference software-engineering.purpose/p3 for CoreReader.Engineering.priorityConditionsCases, with direct-body SHA256 946a96680b1a00867f58e7921588e5a56e79b336ba3d322b8aef1122cc75a60b. This is a traceability binding, not a new premise or semantic proof.
L363software-engineering.evolution-priority#p1 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p1 for CoreReader.Engineering.priorityConditionsCases, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L364software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.priorityConditionsCases, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L365software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.priorityConditionsCases, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L366-/Closes the source-mapping comment for CoreReader.Engineering.priorityConditionsCases; executable declarations resume after the comment.
L367theorem priorityConditionsCases :Bundles ordinary priority, four requirement failures, an accounted cost exception and the nonmaximal chosen design.
L368 EvolutionPriority currentContinuing .evolvable ∧Choosing evolvable satisfies the adopted priority in the ordinary context.
L369 ¬ Meets normalRequirements { profile .evolvable with orderOutput := [1, 2] } ∧Reordered output fails the ordinary order requirement.
L370 ¬ Meets normalRequirements { profile .evolvable with unsafeOperations := 1 } ∧One unsafe operation fails the safety requirement.
L371 ¬ Meets normalRequirements { profile .evolvable with latency := 11 } ∧Latency eleven fails the performance bound.
L372 ¬ Meets normalRequirements { profile .evolvable with retention := 29 } ∧Retention twenty-nine fails the minimum retention requirement.
L373 EvolutionPriority (threatened .verification) .presentSimple ∧With a concrete verification-capacity threat, the rule permits the simple choice through its departure branch.
L374 ¬ JustifiedDeparture { threatened .verification with departure := none } .evolvable ∧Removing the departure account leaves no justified departure even when the threatened cost data remain.
L375 abstractionComplexity .evolvable < abstractionComplexity .maximal := byThe preferred evolvable design has complexity three, below maximal's thirty; the priority is not a duty to maximize complexity.
L376 refine ⟨by decide, by decide, by decide, by decide, by decide, by decide, ?_, by decide⟩Builds the conjunction by finite decisions, leaving only the absent-departure branch for simplification.
L377 simp [JustifiedDeparture]An absent departure reduces JustifiedDeparture to False, proving that negative branch.
L379/-- organon-map CoreReader.Engineering.priorityChoicesBegins a provenance comment attaching CoreReader.Engineering.priorityChoices to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L380software-engineering.evolution-priority#p1 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p1 for CoreReader.Engineering.priorityChoices, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L381software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.priorityChoices, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L382software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.priorityChoices, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L383-/Closes the source-mapping comment for CoreReader.Engineering.priorityChoices; executable declarations resume after the comment.
L384theorem priorityChoices :Presents the actual ordinary evolution choice, ordinary simple rejection and threatened-context simple allowance together.
L385 EvolutionPriority currentContinuing .evolvable ∧The ordinary evolvable choice follows the adopted rule.
L386 ¬ EvolutionPriority currentContinuing .presentSimple ∧The ordinary simple choice fails that same rule.
L387 EvolutionPriority (threatened .verification) .presentSimple := byThe verification-threat context gives a justified exception for choosing simple.
L388 exact ⟨by decide, currentSimpleViolates, by decide⟩Combines computed positive examples with the previously proved no-threat simple-choice contradiction.
L390/-- organon-map CoreReader.Engineering.credibilityLimitsBegins a provenance comment attaching CoreReader.Engineering.credibilityLimits to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L391software-engineering.evolution-priority#p2 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p2 for CoreReader.Engineering.credibilityLimits, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L392software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.credibilityLimits, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L393-/Closes the source-mapping comment for CoreReader.Engineering.credibilityLimits; executable declarations resume after the comment.
L394theorem credibilityLimits :Separates credible planned change from existing implementation count, imaginative possibilities and maximum registered capability.
L395 credible initialGrounds .designRevision ∧ implementedVariants.length = 1 ∧The design-revision plan is credible while only one candidate is implemented.
L396 ¬ WarrantedAccommodation [] (.other "quantum backend") 0 5 ∧An imagined quantum backend with no grounds and zero gain does not justify an investment of five.
L397 ¬ credible initialGrounds (.other "quantum backend") ∧The initial plan does not support the imagined quantum-backend direction.
L398 EvolutionPriority currentContinuing .evolvable ∧The ordinary evolvable choice still satisfies the domain priority.
L399 abstractionComplexity .evolvable < abstractionComplexity .maximal ∧The preferred design's present complexity is lower than maximal's.
L400 cost .evolvable .construction < cost .evolvable .migration ∧Construction and migration costs differ within evolvable, retaining distinct burdens instead of one universal cost rate.
L401 ¬ MaximumRegisteredCapability continuingActivity .evolvable ∧Evolvable does not support every registered direction for all continuing maintainers.
L402 MaximumRegisteredCapability continuingActivity .maximal ∧Maximal does support every direction in the explicitly registered finite set.
L403 (supportedDirections continuingActivity .evolvable).length = 9 ∧Evolvable supports nine registered directions.
L404 (supportedDirections continuingActivity .maximal).length = 10 ∧Maximal supports ten, making its extra extensibility substantive rather than merely a name.
L405 ¬ credible initialGrounds (.other "csv export") := by decideCSV export is not supported by the current plan, so its technical availability does not itself establish present credibility. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L407/-- organon-map CoreReader.Engineering.costCasesBegins a provenance comment attaching CoreReader.Engineering.costCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L408software-engineering.evolution-priority#p3 sha256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04Records the source reference software-engineering.evolution-priority/p3 for CoreReader.Engineering.costCases, with direct-body SHA256 c2237515e869b2f88269cf19e3c97ef80c3c87342d1a03cd911cac03fe5a3a04. This is a traceability binding, not a new premise or semantic proof.
L409-/Closes the source-mapping comment for CoreReader.Engineering.costCases; executable declarations resume after the comment.
L410theorem costCases :Checks each of the seven burdens as a possible concrete reason for departing from priority.
L411 JustifiedDeparture (threatened .understanding) .evolvable ∧Reducing understanding capacity to one makes the evolvable understanding cost a justified departure.
L412 JustifiedDeparture (threatened .construction) .evolvable ∧The analogous construction-capacity threat justifies departure.
L413 JustifiedDeparture (threatened .diagnosis) .evolvable ∧The analogous diagnosis-capacity threat justifies departure.
L414 JustifiedDeparture (threatened .verification) .evolvable ∧The analogous verification-capacity threat justifies departure.
L415 JustifiedDeparture (threatened .coordination) .evolvable ∧The analogous coordination-capacity threat justifies departure.
L416 JustifiedDeparture (threatened .operation) .evolvable ∧The analogous operational-capacity threat justifies departure.
L417 JustifiedDeparture (threatened .migration) .evolvable ∧The analogous migration-capacity threat justifies departure.
L418 ¬ JustifiedDeparture { currentContinuing with departure := some .migration } .evolvable := by decideMerely naming migration in the ordinary capacity-twelve context does not create a real threat or justified exception. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L420/- Total functions model an identified order-preserving de-duplication API.The following total functions represent an identified de-duplication API. Finite corpus equality is kept distinct from universal contract preservation.
L421The test corpus is explicitly finite; universal preservation is separate. -/The following total functions represent an identified de-duplication API. Finite corpus equality is kept distinct from universal contract preservation.
L422def orderedUnique (xs : List Nat) : List Nat := xs.eraseDupsRemoves duplicate values using the standard library's order-preserving list operation.
L423def orderedRefactor (xs : List Nat) : List Nat := xs.eraseDups ++ []The refactor performs the same de-duplication and appends an empty list, preserving output.
L424def insertOrdered (n : Nat) : List Nat → List NatTake a natural number and an arbitrary natural-number list; the type has no sorted-input premise. sortValues uses this helper for ordered insertion into its recursively sorted tail.
L425 | [] => [n]Inserting into an empty list yields the singleton value.
L426 | x :: xs => if n ≤ x then n :: x :: xs else x :: insertOrdered n xsPlaces the value before the first no-smaller head; otherwise keeps the head and recursively inserts into the tail.
L428def sortValues : List Nat → List NatSorting recursively uses the insertion operation; this changes ordering rather than only de-duplicating.
L429 | [] => []The empty list sorts to itself.
L430 | x :: xs => insertOrdered x (sortValues xs)Sorts the tail and inserts the original head into that sorted result.
L432def sortedUnique (xs : List Nat) : List Nat := (sortValues xs).eraseDupsThe alternative implementation sorts all values before removing duplicates, so it can violate the original order contract.
L434structure SoftwareState whereSoftware-state fields allow distinct kinds of evolution to change distinct aspects of the represented design.
L435 capabilities : List StringLists the represented capabilities of the software.
L436 implementation : NatIdentifies which implementation version is used.
L437 mechanisms : List StringLists concrete mechanisms that may be added or deleted.
L438 abstractions : List StringLists abstractions that may be retained or withdrawn.
L439 boundary : NatRecords a boundary revision index, separate from capability and implementation indices.
L440 technology : StringIdentifies the storage technology or model that may be migrated away from.
L441 batchSize : NatRecords the configured batch size.
L442 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for SoftwareState; these support concrete case evaluation, not a philosophical claim about that type.
L444def originalSoftware : SoftwareState :=The starting software de-duplicates, uses implementation 0, queue plus legacy cache, fixed batching, boundary index 0, legacy storage and batch size ten.
L445 ⟨["deduplicate"], 0, ["queue", "legacy cache"], ["fixed batch"], 0, "legacy store", 10⟩The starting software de-duplicates, uses implementation 0, queue plus legacy cache, fixed batching, boundary index 0, legacy storage and batch size ten.
L447def transform (d : Change) (s : SoftwareState) : SoftwareState := match d withEach change direction transforms actual selected fields of the software state; this is a stipulated state model, not an executable source-code editor.
L448 | .addition => { s with capabilities := s.capabilities ++ ["tenant batching"] }Addition retains existing capabilities and adds tenant batching.
L449 | .replacement => { s with implementation := s.implementation + 1 }Replacement increments the implementation identifier.
L450 | .deletion => { s with mechanisms := s.mechanisms.filter (· != "legacy cache") }Deletion removes legacy cache while retaining other mechanisms.
L451 | .withdrawal => { s with abstractions := s.abstractions.filter (· != "fixed batch") }Withdrawal removes the fixed-batch abstraction.
L452 | .redrawing => { s with boundary := s.boundary + 1 }Redrawing increments the boundary revision index.
L453 | .migration => { s with technology := "portable store" }Migration replaces legacy technology with portable storage.
L454 | .independent => { s with batchSize := 5 }Independent change updates only batch size to five.
L455 | .coordinated => { s with batchSize := 5, boundary := s.boundary + 1 }Coordinated change updates batch size and the boundary index together.
L456 | .designRevision => { s with batchSize := 5, abstractions := ["live configuration"], boundary := s.boundary + 1 }Design revision sets batch size five, replaces the abstraction with live configuration and redraws the boundary.
L457 | .other name =>The named CSV direction adds an actual CSV capability; unrecognized other directions leave the state unchanged.
L458 if name = "csv export" then { s with capabilities := s.capabilities ++ ["csv export"] }The named CSV direction adds an actual CSV capability; unrecognized other directions leave the state unchanged.
L459 else sThe named CSV direction adds an actual CSV capability; unrecognized other directions leave the state unchanged.
L461def evolutionBehavior (d : Change) : List Nat → List Nat :=Redrawing and design revision deliberately use sortedUnique behavior; other changes preserve orderedUnique behavior in this application.
L462 if d = .redrawing ∨ d = .designRevision then sortedUnique else orderedUniqueRedrawing and design revision deliberately use sortedUnique behavior; other changes preserve orderedUnique behavior in this application.
L464/- Changes include an open other constructor. Work, maintainer knowledge andOpen-ended change kinds, work requirements, maintainer knowledge and obligation treatment remain separate; they are not collapsed into a single extensibility score.
L465obligation treatment are separate dimensions, not one extensibility score. -/Open-ended change kinds, work requirements, maintainer knowledge and obligation treatment remain separate; they are not collapsed into a single extensibility score.
L466inductive ObligationTreatment whereA change claim explicitly says whether it preserves or deliberately revises obligations.
L467 | preserve | reviseA change claim explicitly says whether it preserves or deliberately revises obligations.
L468 deriving DecidableEq, ReprA change claim explicitly says whether it preserves or deliberately revises obligations. Automatically provides equality decisions and printable representations for ObligationTreatment; these support concrete case evaluation, not a philosophical claim about that type.
L469structure ChangeClaim whereGroups the intended direction, acting maintainer and declared obligation treatment in one claim.
L470 direction : ChangeIdentifies the change whose capability is being claimed.
L471 byMaintainer : MaintainerIdentifies the maintainer whose conditions must support that change.
L472 treatment : ObligationTreatmentStates whether the same identified obligation is preserved or deliberately revised.
L474abbrev contractInputs : List (List Nat) := [[], [2, 1, 2], [1, 3, 1], [4, 4]]The finite order corpus is exactly four lists: empty, [2,1,2], [1,3,1] and [4,4]; later finite preservation claims are limited to these inputs.
L475def PreservesOn {Input Output : Type} (scope : Input → Prop)Universal scoped preservation requires the new and old functions to agree for every input satisfying the supplied scope predicate.
L476 (old new : Input → Output) : Prop := ∀ x, scope x → new x = old xUniversal scoped preservation requires the new and old functions to agree for every input satisfying the supplied scope predicate.
L478abbrev PreservesFinite (old new : List Nat → List Nat) : Prop :=Finite preservation checks only the declared corpus by Boolean equality; it does not infer the preceding all-input property.
L479 contractInputs.all (fun xs => new xs == old xs) = trueFinite preservation checks only the declared corpus by Boolean equality; it does not infer the preceding all-input property.
L481/- The actual contracts and observer dependencies are inputs independent ofContracts and observer dependencies are supplied independently of the report, preventing report edits from redefining the actual old/new behavior or affected population.
L482any revision report. Reports cannot redefine the affected population or theContracts and observer dependencies are supplied independently of the report, preventing report edits from redefining the actual old/new behavior or affected population.
L483old/new retry behavior merely by changing their own fields. -/Contracts and observer dependencies are supplied independently of the report, preventing report edits from redefining the actual old/new behavior or affected population.
L484structure ObservableContract whereAn observable contract combines order behavior with a retry limit.
L485 order : List Nat → List NatThe order function is actual observable behavior, not just a contract name.
L486 maxAttempts : NatThe retry threshold belongs to the actual contract.
L488def retry (contract : ObservableContract) (attempts : Nat) : Bool :=A retry is permitted exactly when the attempt index is below maxAttempts, making changes in that threshold observable.
L489 attempts < contract.maxAttemptsA retry is permitted exactly when the attempt index is below maxAttempts, making changes in that threshold observable.
L491def orderContract (order : List Nat → List Nat) : ObservableContract := ⟨order, 3⟩An ordinary order contract pairs its function with threshold three.
L492def originalContract : ObservableContract := orderContract orderedUniqueThe original contract uses ordered de-duplication and threshold three.
L493def refactoredContract : ObservableContract := orderContract orderedRefactorThe refactored contract changes only to the extensionally identical refactor, retaining threshold three.
L494def revisedContract : ObservableContract := ⟨sortedUnique, 5⟩The deliberate revision uses sorted de-duplication and threshold five, changing both represented contract aspects.
L495def evolutionContract (d : Change) : ObservableContract :=The direction-specific contract uses its actual evolution behavior and raises retry threshold only for redrawing or design revision.
L496 ⟨evolutionBehavior d, if d = .redrawing ∨ d = .designRevision then 5 else 3⟩The direction-specific contract uses its actual evolution behavior and raises retry threshold only for redrawing or design revision.
L498def failureInputs : List Nat := [0, 1, 2, 3, 4, 5]The finite retry corpus contains attempt indices zero through five.
L499abbrev PreservesContractFinite (old new : ObservableContract) : Prop :=Finite whole-contract preservation requires both order equality on contractInputs and retry equality on failureInputs.
L500 PreservesFinite old.order new.order ∧Finite whole-contract preservation requires both order equality on contractInputs and retry equality on failureInputs.
L501 failureInputs.all (fun attempts => retry new attempts == retry old attempts) = trueFinite whole-contract preservation requires both order equality on contractInputs and retry equality on failureInputs.
L503inductive ContractAspect whereOrder and retry are distinct observable contract aspects, allowing different parties to depend on them.
L504 | order | retryOrder and retry are distinct observable contract aspects, allowing different parties to depend on them.
L505 deriving DecidableEq, ReprOrder and retry are distinct observable contract aspects, allowing different parties to depend on them. Automatically provides equality decisions and printable representations for ContractAspect; these support concrete case evaluation, not a philosophical claim about that type.
L506structure PartyDependency whereA dependency record connects a named party to the contract aspect it observes.
L507 party : StringIdentifies the party whose obligations may be affected.
L508 observes : ContractAspectIdentifies the particular observable aspect that party depends on.
L509 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for PartyDependency; these support concrete case evaluation, not a philosophical claim about that type.
L511def partyDependencies : List PartyDependency :=The queue consumer depends on order, while the queue operator depends on retry behavior; these dependencies are fixed outside the revision report.
L512 [⟨"queue consumer", .order⟩, ⟨"queue operator", .retry⟩]The queue consumer depends on order, while the queue operator depends on retry behavior; these dependencies are fixed outside the revision report.
L514def aspectChanged (old new : ObservableContract) : ContractAspect → BoolDetects changes from actual old/new contracts under the finite observations for each aspect.
L515 | .order => contractInputs.any (fun xs => new.order xs != old.order xs)Order changes when any declared order input produces a different output.
L516 | .retry => failureInputs.any (fun attempts => retry new attempts != retry old attempts)Retry changes when any declared attempt index produces a different permission result.
L518def affectedParties (old new : ObservableContract) : List String :=The affected-party list is computed from fixed dependencies whose observed aspect actually changes, not taken from the report's own claim.
L519 (partyDependencies.filter (fun dependency => aspectChanged old new dependency.observes)).mapThe affected-party list is computed from fixed dependencies whose observed aspect actually changes, not taken from the report's own claim.
L520 PartyDependency.partyThe affected-party list is computed from fixed dependencies whose observed aspect actually changes, not taken from the report's own claim.
L522structure ContractRevision whereThe revision account records intention, changed observations, parties, actual-limit claims, recorded limits and a procedure description.
L523 deliberate : BoolStates that a contract change is deliberate.
L524 revisedOrder : List NatRecords the revised order output on the distinguished sample.
L525 affected : List StringLists parties acknowledged by the report; duties later compare this to actual affected parties.
L526 oldFailureLimit : NatStates the claimed old retry threshold.
L527 newFailureLimit : NatStates the claimed new retry threshold.
L528 recordedOldFailureLimit : NatRetains the report's historical record of the old threshold.
L529 recordedNewFailureLimit : NatRetains the recorded new threshold.
L530 procedure : StringNames the chosen procedure; the philosophical account does not prescribe one particular procedure.
L532def normalRevision : ContractRevision := {The ordinary revision is deliberate and records the new sorted result [1,2].
L533 deliberate := true, revisedOrder := [1, 2],The ordinary revision is deliberate and records the new sorted result [1,2].
L534 affected := ["queue consumer", "queue operator"],Acknowledges both the consumer and operator affected by the two actual aspect changes.
L535 oldFailureLimit := 3, newFailureLimit := 5,States actual retry limits changing from three to five.
L536 recordedOldFailureLimit := 3, recordedNewFailureLimit := 5,The retained records also say three before and five after, rather than rewriting the old limit.
L537 procedure := "contract review" }Uses contract review as one possible procedure, without making its name a condition of validity.
L539abbrev RevisionDuties (old new : ObservableContract) (r : ContractRevision) : Prop :=Revision duties are evaluated against the independently supplied old/new contracts and the particular report.
L540 r.deliberate = true ∧ r.revisedOrder = new.order [2, 1, 2] ∧Requires deliberate revision and an accurate report of the new output on [2,1,2].
L541 (affectedParties old new).all (fun p => r.affected.contains p) = true ∧Every actually affected party must occur in the report; this permits extra listed parties and does not prescribe notification.
L542 r.oldFailureLimit = old.maxAttempts ∧ r.newFailureLimit = new.maxAttempts ∧Both claimed failure limits must equal the independently supplied actual thresholds.
L543 r.recordedOldFailureLimit = old.maxAttempts ∧The recorded old limit must still match the original contract.
L544 r.recordedNewFailureLimit = new.maxAttemptsThe recorded new limit must match the new contract.
L546/-- organon-map CoreReader.Engineering.ContractChangeAccountBegins a provenance comment attaching CoreReader.Engineering.ContractChangeAccount to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L547software-engineering.structural-judgment#p3 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p3 for CoreReader.Engineering.ContractChangeAccount, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L548-/Closes the source-mapping comment for CoreReader.Engineering.ContractChangeAccount; executable declarations resume after the comment.
L549abbrev ContractChangeAccount (old new : ObservableContract) (r : ContractRevision) : Prop :=A contract-change account either preserves all declared finite observations or supplies the deliberate-revision duties; these are distinct alternatives.
L550 PreservesContractFinite old new ∨ RevisionDuties old new rA contract-change account either preserves all declared finite observations or supplies the deliberate-revision duties; these are distinct alternatives.
L552/-- organon-map CoreReader.Engineering.EvolutionClaimBegins a provenance comment attaching CoreReader.Engineering.EvolutionClaim to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L553software-engineering.evolution-meaning#p1 sha256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6Records the source reference software-engineering.evolution-meaning/p1 for CoreReader.Engineering.EvolutionClaim, with direct-body SHA256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6. This is a traceability binding, not a new premise or semantic proof.
L554software-engineering.evolution-meaning#p2 sha256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6Records the source reference software-engineering.evolution-meaning/p2 for CoreReader.Engineering.EvolutionClaim, with direct-body SHA256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6. This is a traceability binding, not a new premise or semantic proof.
L555-/Closes the source-mapping comment for CoreReader.Engineering.EvolutionClaim; executable declarations resume after the comment.
L556abbrev EvolutionClaim (a : Activity) (c : Candidate) (claim : ChangeClaim) : Prop :=A capability claim concerns a specific maintainer and direction, with an explicit obligation treatment.
L557 CanChange a c claim.byMaintainer claim.direction ∧The named maintainer must actually be able to execute the intended direction's path.
L558 ContractChangeAccount originalContract (evolutionContract claim.direction) normalRevision ∧The same direction's actual old/new contract change must have a valid preservation or revision account.
L559 (changePath c claim.direction).any (fun step => step.tool == .contractRunner) = true ∧The direction's path must contain a contract-runner step, tying the claim to represented verification work.
L560 ((claim.treatment = .preserve ∧A preserve claim requires the distinguished sample to retain the original ordered output.
L561 evolutionBehavior claim.direction [2, 1, 2] = orderedUnique [2, 1, 2]) ∨A preserve claim requires the distinguished sample to retain the original ordered output.
L562 (claim.treatment = .revise ∧A revise claim instead requires an actual different output on that sample; the treatment label cannot silently reverse the observed relation.
L563 evolutionBehavior claim.direction [2, 1, 2] ≠ orderedUnique [2, 1, 2]))A revise claim instead requires an actual different output on that sample; the treatment label cannot silently reverse the observed relation.
L565/-- organon-map CoreReader.Engineering.evolutionKindsCasesBegins a provenance comment attaching CoreReader.Engineering.evolutionKindsCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L566software-engineering.evolution-meaning#p1 sha256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6Records the source reference software-engineering.evolution-meaning/p1 for CoreReader.Engineering.evolutionKindsCases, with direct-body SHA256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6. This is a traceability binding, not a new premise or semantic proof.
L567software-engineering.evolution-meaning#p2 sha256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6Records the source reference software-engineering.evolution-meaning/p2 for CoreReader.Engineering.evolutionKindsCases, with direct-body SHA256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6. This is a traceability binding, not a new premise or semantic proof.
L568-/Closes the source-mapping comment for CoreReader.Engineering.evolutionKindsCases; executable declarations resume after the comment.
L569theorem evolutionKindsCases :Collects actual state changes, successor capability and both preservation/revision claim examples.
L570 (transform .addition originalSoftware).capabilities = ["deduplicate", "tenant batching"] ∧Addition retains de-duplication and adds tenant batching.
L571 (transform .replacement originalSoftware).implementation = 1 ∧Replacement changes implementation index zero to one.
L572 (transform .deletion originalSoftware).mechanisms = ["queue"] ∧Deletion removes legacy cache, leaving the queue mechanism.
L573 (transform .withdrawal originalSoftware).abstractions = [] ∧Withdrawal removes the only fixed-batch abstraction, leaving the abstraction list empty.
L574 (transform .redrawing originalSoftware).boundary = 1 ∧Redrawing changes the boundary index from zero to one.
L575 (transform .migration originalSoftware).technology = "portable store" ∧Migration changes the storage technology to portable store.
L576 changes.all (fun d => decide (CanChange continuingActivity .evolvable .successor d)) = true ∧The successor can execute all nine ordinary evolvable change paths with the supplied tools and guides.
L577 EvolutionClaim continuingActivity .evolvable ⟨.replacement, .successor, .preserve⟩ ∧A successor's replacement is a valid preservation-type EvolutionClaim.
L578 EvolutionClaim continuingActivity .evolvable ⟨.redrawing, .agent, .revise⟩ ∧An agent's boundary redrawing is a valid deliberate-revision EvolutionClaim.
L579 changeWork .evolvable .independent < changeWork .evolvable .coordinated := by decideIndependent work costs two while coordinated work costs eight, so they need not require equal work. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L581/-- organon-map CoreReader.Engineering.evolutionDimensionsLimitsBegins a provenance comment attaching CoreReader.Engineering.evolutionDimensionsLimits to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L582software-engineering.evolution-meaning#p1 sha256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6Records the source reference software-engineering.evolution-meaning/p1 for CoreReader.Engineering.evolutionDimensionsLimits, with direct-body SHA256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6. This is a traceability binding, not a new premise or semantic proof.
L583software-engineering.evolution-meaning#p2 sha256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6Records the source reference software-engineering.evolution-meaning/p2 for CoreReader.Engineering.evolutionDimensionsLimits, with direct-body SHA256 c3fa878716f4370ebd1d352d2c135255695cfec6e1d33900a184cb46acb80bf6. This is a traceability binding, not a new premise or semantic proof.
L584-/Closes the source-mapping comment for CoreReader.Engineering.evolutionDimensionsLimits; executable declarations resume after the comment.
L585theorem evolutionDimensionsLimits :Shows that different evolution dimensions have different costs and capabilities, including an actual maximum-versus-evolvable contrast.
L586 changeWork .presentSimple .addition = 2 ∧Simple-design addition costs two units.
L587 changeWork .presentSimple .withdrawal = 17 ∧Withdrawing its fixed structure costs seventeen units, much more than addition.
L588 changeWork .evolvable .independent < changeWork .evolvable .coordinated ∧Evolvable independent change costs less than its coordinated change.
L589 EvolutionPriority currentContinuing .evolvable ∧These uneven costs coexist with satisfaction of evolution priority.
L590 9 < changeWork .evolvable .migration ∧Evolvable migration costs ten, so it exceeds nine despite the priority's satisfaction.
L591 CanChange continuingActivity .presentSimple .original .addition ∧The original maintainer can add to the simple design.
L592 CanChange continuingActivity .evolvable .original .addition ∧The original maintainer can also add to evolvable.
L593 CanChange continuingActivity .presentSimple .original .designRevision ∧The original maintainer's private knowledge permits simple-design revision.
L594 CanChange continuingActivity .evolvable .original .designRevision ∧The original maintainer can also perform evolvable design revision.
L595 changeWork .evolvable .designRevision < changeWork .presentSimple .designRevision ∧For the same design-revision direction, evolvable uses six work units versus simple's seventeen.
L596 changeWork .evolvable .addition = changeWork .presentSimple .addition ∧Both designs use two units for addition; an advantage on design revision is not a strict advantage on every dimension.
L597 (transform (.other "csv export") originalSoftware).capabilities = ["deduplicate", "csv export"] ∧CSV export changes the actual capability list to include CSV alongside de-duplication.
L598 CanChange continuingActivity .maximal .successor (.other "csv export") ∧The successor has the guides and tools for maximal's CSV path.
L599 ¬ CanChange continuingActivity .evolvable .successor (.other "csv export") := byThe successor lacks privateLayout needed by evolvable's CSV path, despite its other advantages.
L600 exact ⟨by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide, by decide⟩Constructs every conjunct with Lean's decision procedure over the explicit finite paths, states and arithmetic; no empirical generalization occurs.
L602theorem oneDimensionDoesNotEntailEveryDimension :States a counterexample to universal strict improvement from a single-direction advantage.
L603 changeWork .evolvable .designRevision < changeWork .presentSimple .designRevision ∧Retains the genuine strict improvement for design revision.
L604 ¬ (∀ d : Change, changeWork .evolvable d < changeWork .presentSimple d) := byDenies that evolvable requires strictly less work for every Change, including additions and named other directions.
L605 refine ⟨by decide, ?_⟩Computes the positive revision inequality and leaves the universal negative to a counterexample argument.
L606 intro allDirectionsAssumes strict improvement in every direction to derive a contradiction.
L607 exact (by decide : ¬ changeWork .evolvable .addition < changeWork .presentSimple .addition)Specializes that assumption to addition, where both work totals equal two; the claimed strict inequality is false.
L608 (allDirections .addition)Specializes that assumption to addition, where both work totals equal two; the claimed strict inequality is false.
L610def propagation (c : Candidate) (d : Change) : List Nat :=Change propagation is the distinct list of component identifiers touched by the actual path, retaining relations to the intended change.
L611 ((changePath c d).map EditStep.component).eraseDupsChange propagation is the distinct list of component identifiers touched by the actual path, retaining relations to the intended change.
L613def batchCount (items size : Nat) : Nat := (items + size - 1) / sizeComputes a natural-number batch-count expression (items+size−1)/size. It is intended for positive batch sizes; Lean subtraction and division are total even outside that intended domain.
L614def staticBatch (items _runtimeSize : Nat) : Nat := batchCount items 10The static predictor deliberately ignores runtimeSize and always computes with size ten.
L615def liveBatch (items runtimeSize : Nat) : Nat := batchCount items runtimeSizeThe live predictor uses the supplied runtime batch size, allowing the fixed assumption to be tested.
L617structure StructuralEvidence whereA structural evidence record connects an intended change to participants, propagation, observations and work accounts.
L618 intended : ChangeIdentifies the change this evidence is supposed to support.
L619 participants : List MaintainerIdentifies the relevant maintainers in the evidence account.
L620 touched : List NatRecords which components the change touches.
L621 contractObservations : List (List Nat)Records the exact input corpus used to observe contracts.
L622 observedBefore : List (List Nat)Records outputs before the change on that corpus.
L623 observedAfter : List (List Nat)Records outputs after the change on the same corpus.
L624 understandingWork : NatStores the represented understanding-work quantity, here instantiated from total path work.
L625 verificationWork : NatStores a verification-work quantity, instantiated below as the number of contract-runner steps rather than their unit sum.
L626 boundaryGain : NatStores a claimed work gain over the simple design for this intended change.
L628def structuralEvidence (c : Candidate) (d : Change) : StructuralEvidence := {Builds a concrete evidence record from the candidate's path and the same intended direction.
L629 intended := d, participants := maintainers, touched := propagation c d,Binds the direction, all maintainers and the actual deduplicated propagation list.
L630 contractObservations := contractInputs,Uses exactly the declared finite contract corpus.
L631 observedBefore := contractInputs.map orderedUnique,Computes the old observations with orderedUnique.
L632 observedAfter := contractInputs.map (evolutionBehavior d),Computes the new observations with that direction's actual evolutionBehavior.
L633 understandingWork := changeWork c d,The understanding-work field equals the intended path's total assigned work.
L634 verificationWork := ((changePath c d).filter (fun step => step.tool == .contractRunner)).length,Verification counts actual contractRunner steps in the same path.
L635 boundaryGain := changeWork .presentSimple d - changeWork c d }Work gain is simple work minus chosen work using natural subtraction, which truncates at zero rather than recording negative gains.
L637/-- organon-map CoreReader.Engineering.StructuralAccountBegins a provenance comment attaching CoreReader.Engineering.StructuralAccount to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L638software-engineering.structural-judgment#p1 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p1 for CoreReader.Engineering.StructuralAccount, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L639software-engineering.structural-judgment#p2 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p2 for CoreReader.Engineering.StructuralAccount, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L640-/Closes the source-mapping comment for CoreReader.Engineering.StructuralAccount; executable declarations resume after the comment.
L641abbrev StructuralAccount (a : Activity) (c : Candidate) (e : StructuralEvidence) : Prop :=A valid structural account must match the actual activity, candidate and intended change; merely filling record fields is insufficient.
L642 e.participants = a.participants ∧ e.touched = propagation c e.intended ∧Recorded participants must equal the activity's, and touched components must equal actual propagation for the claimed direction.
L643 e.contractObservations = contractInputs ∧The account must identify the prescribed finite observation inputs exactly.
L644 e.observedBefore = contractInputs.map orderedUnique ∧Its before-results must be the original ordered behavior on those inputs.
L645 e.observedAfter = contractInputs.map (evolutionBehavior e.intended) ∧Its after-results must come from the same intended direction's behavior.
L646 e.understandingWork = changeWork c e.intended ∧The claimed understanding work must match the selected path's total work.
L647 e.verificationWork = ((changePath c e.intended).filterThe verification field must match the actual number of contract-runner steps; this checks a concrete work relation, not a free assessment flag.
L648 (fun step => step.tool == .contractRunner)).length ∧The verification field must match the actual number of contract-runner steps; this checks a concrete work relation, not a free assessment flag.
L649 e.boundaryGain = changeWork .presentSimple e.intended - changeWork c e.intendedThe claimed gain must equal the actual simple-minus-selected work difference for the same intended change.
L651structure InterfaceView whereVisible interface metadata is separated from executable behavior and edit paths for later insufficiency counterexamples.
L652 signature : StringStores the visible function signature text.
L653 modules : NatStores a claimed module count, later compared with actual component lists.
L654 extensionPoints : NatStores the visible extension-point count.
L655 principle : StringStores a named design principle; its name alone will not prove capability.
L656 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for InterfaceView; these support concrete case evaluation, not a philosophical claim about that type.
L658def sameShape : InterfaceView := ⟨"List Nat → List Nat", 8, 12, "dependency inversion"⟩Several designs share the same List Nat→List Nat signature, eight modules, twelve extension points and dependency-inversion label.
L659def moduleAssumptions : List (Nat × Nat) :=All eight components, numbered zero through seven, assume batch size ten.
L660 (List.range 8).map (fun component => (component, 10))All eight components, numbered zero through seven, assume batch size ten.
L662def modulesNeedingRevision (newSize : Nat) : List Nat :=Changing batch size selects the components whose stored assumption differs from the new size; at size five all eight need revision.
L663 (moduleAssumptions.filter (fun p => p.2 != newSize)).map Prod.fstChanging batch size selects the components whose stored assumption differs from the new size; at size five all eight need revision.
L665structure Boundary whereA boundary carries actual endpoint identifiers and a contract label, allowing relation-sensitive checks.
L666 caller : NatIdentifies the caller endpoint of the edge.
L667 callee : NatIdentifies the callee endpoint of the edge.
L668 contract : StringStores the edge's contract label; later checks also require work and actual output equality, so this string is not sufficient evidence.
L669 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for Boundary; these support concrete case evaluation, not a philosophical claim about that type.
L671structure EngineeringDesign whereA complete represented design combines metadata with its actual function, paths, components, boundaries and assumptions.
L672 metadata : InterfaceViewKeeps the visible metadata alongside the substantive design fields.
L673 run : List Nat → List NatCarries the actual behavior used in contract comparisons.
L674 paths : Change → List EditStepSupplies concrete edit steps separately for each intended change.
L675 components : List NatLists actual component identifiers, allowing endpoint-presence checks.
L676 boundaries : List BoundaryLists the design's actual represented edges.
L677 batchAssumptions : List (Nat × Nat)Associates components with their fixed batch-size assumptions.
L679def privateDesign : EngineeringDesign := {The private design has the shared metadata, ordered behavior and simple-design paths; it has eight components, no explicit edges and eight fixed-batch assumptions.
L680 metadata := sameShape, run := orderedUnique, paths := changePath .presentSimple,The private design has the shared metadata, ordered behavior and simple-design paths; it has eight components, no explicit edges and eight fixed-batch assumptions.
L681 components := List.range 8, boundaries := [], batchAssumptions := moduleAssumptions }The private design has the shared metadata, ordered behavior and simple-design paths; it has eight components, no explicit edges and eight fixed-batch assumptions.
L683def documentedDesign : EngineeringDesign := {The documented design changes only the work paths to evolvable's guide-based paths; metadata and observable behavior stay the same.
L684 privateDesign with paths := changePath .evolvable }The documented design changes only the work paths to evolvable's guide-based paths; metadata and observable behavior stay the same.
L686def sortedDesign : EngineeringDesign := { documentedDesign with run := sortedUnique }The sorted variant changes actual behavior while retaining documented design metadata and paths, enabling a same-signature contract counterexample.
L688/- This application has a caller at component 2 and a callee at component 1.This finite application treats editing callee 1 as crossing the actual 2→1 edge and requiring caller-side order verification; neither an edge label nor a named contract proves that verification occurred or output was preserved.
L689Editing the callee crosses that actual edge. The caller must recheck theThis finite application treats editing callee 1 as crossing the actual 2→1 edge and requiring caller-side order verification; neither an edge label nor a named contract proves that verification occurred or output was preserved.
L690observable order contract in this finite case; the contract name alone is notThis finite application treats editing callee 1 as crossing the actual 2→1 edge and requiring caller-side order verification; neither an edge label nor a named contract proves that verification occurred or output was preserved.
L691evidence that either the verification work or the observable equality holds. -/This finite application treats editing callee 1 as crossing the actual 2→1 edge and requiring caller-side order verification; neither an edge label nor a named contract proves that verification occurred or output was preserved.
L692def coordinatedBoundary : Boundary := ⟨2, 1, "order-preserving queue"⟩Instantiates the concrete edge from caller 2 to callee 1 with the queue's order-contract label.
L694def boundaryDesign : EngineeringDesign :=Adds that actual edge to documentedDesign's boundary list, tying the later check to a design containing the edge.
L695 { documentedDesign with boundaries := [coordinatedBoundary] }Adds that actual edge to documentedDesign's boundary list, tying the later check to a design containing the edge.
L697def crossesBoundary (design : EngineeringDesign) (direction : Change) (edge : Boundary) : Bool :=Boundary crossing is checked for one actual design, one intended direction and one edge.
L698 design.boundaries.contains edge && design.components.contains edge.caller &&The edge must belong to the design and its caller must be an actual component.
L699 design.components.contains edge.callee && edge.caller != edge.callee &&Its callee must also exist, and caller and callee must be different components.
L700 (design.paths direction).any (fun step => step.component == edge.callee &&The intended path must actually edit or compile the callee component; an unrelated edge does not establish propagation across this boundary.
L701 (step.tool == .editor || step.tool == .compiler))The intended path must actually edit or compile the callee component; an unrelated edge does not establish propagation across this boundary.
L703def boundaryObligationChecked (design : EngineeringDesign) (direction : Change)The boundary-obligation test is indexed by the same design, intended change and edge, so results for unrelated boundaries cannot substitute.
L704 (edge : Boundary) : Bool :=The boundary-obligation test is indexed by the same design, intended change and edge, so results for unrelated boundaries cannot substitute.
L705 crossesBoundary design direction edge &&Requires the actual boundary-crossing relation before treating a caller-side check as a cross-boundary obligation.
L706 (design.paths direction).any (fun step => step.component == edge.caller &&The same change path must contain a caller-component contractRunner step requiring publicContract knowledge.
L707 step.tool == .contractRunner && step.requires == .publicContract) &&The same change path must contain a caller-component contractRunner step requiring publicContract knowledge.
L708 decide (PreservesFinite orderedUnique design.run)The actual design behavior must preserve orderedUnique on the declared finite order corpus; a check-step label without output equality fails.
L710def omittedCallerCheck : EngineeringDesign :=Construct omittedCallerCheck as a design variant whose paths omit caller contract-runner work, for the later boundary-obligation counterexample.
L711 { boundaryDesign with paths := fun direction =>Copy boundaryDesign’s other fields unchanged and replace paths with a function that transforms the path for each requested direction.
L712 (boundaryDesign.paths direction).filter (fun step =>Filter the original boundaryDesign path for this same direction, retaining precisely the steps accepted by the following predicate.
L713 !(step.component == coordinatedBoundary.caller && step.tool == .contractRunner)) }Exclude a step exactly when it is at coordinatedBoundary.caller and uses contractRunner; keep all other steps and finish the record update.
L715def otherCalleeBoundary : Boundary := { coordinatedBoundary with callee := 7 }Moves the callee endpoint to component 7 while retaining the caller and contract label.
L717def otherCalleeDesign : EngineeringDesign :=The alternate design actually contains the changed edge, so the negative crossing test is about its endpoint/path mismatch rather than simple absence of the edge.
L718 { boundaryDesign with boundaries := [otherCalleeBoundary] }The alternate design actually contains the changed edge, so the negative crossing test is about its endpoint/path mismatch rather than simple absence of the edge.
L720theorem actualCrossBoundaryObligation :Checks positive and negative relations among actual edges, intended work, caller obligations and observable behavior.
L721 crossesBoundary boundaryDesign .coordinated coordinatedBoundary = true ∧Coordinated work in boundaryDesign crosses its actual 2→1 edge.
L722 boundaryObligationChecked boundaryDesign .coordinated coordinatedBoundary = true ∧That work includes the required caller check and retains the finite order contract.
L723 crossesBoundary omittedCallerCheck .coordinated coordinatedBoundary = true ∧Removing the caller check does not remove the callee edit, so the boundary is still crossed.
L724 boundaryObligationChecked omittedCallerCheck .coordinated coordinatedBoundary = false ∧Nevertheless the cross-boundary obligation is unmet after the caller check is removed.
L725 crossesBoundary otherCalleeDesign .coordinated otherCalleeBoundary = false ∧The edge to callee 7 is not crossed because the coordinated path does not edit or compile that callee.
L726 boundaryObligationChecked { boundaryDesign with run := sortedUnique }Replacing only run with sortedUnique violates the order obligation despite unchanged edge and checking steps; the finite conjunction is proved by computation.
L727 .coordinated coordinatedBoundary = false := by decideReplacing only run with sortedUnique violates the order obligation despite unchanged edge and checking steps; the finite conjunction is proved by computation. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L729/-- organon-map CoreReader.Engineering.structuralCasesBegins a provenance comment attaching CoreReader.Engineering.structuralCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L730software-engineering.structural-judgment#p1 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p1 for CoreReader.Engineering.structuralCases, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L731software-engineering.structural-judgment#p2 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p2 for CoreReader.Engineering.structuralCases, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L732-/Closes the source-mapping comment for CoreReader.Engineering.structuralCases; executable declarations resume after the comment.
L733theorem structuralCases :The registered structural case bundle includes actual propagation, contract observations, work and the new explicit cross-boundary checks.
L734 StructuralAccount continuingActivity .evolvable (structuralEvidence .evolvable .designRevision) ∧The evolvable design-revision evidence matches the actual continuing activity and intended path.
L735 (propagation .presentSimple .designRevision).length = 3 ∧Simple design revision touches three distinct components.
L736 (propagation .evolvable .designRevision).length = 2 ∧Evolvable design revision touches two distinct components.
L737 (changePath .evolvable .coordinated).any (fun s => s.component == 2 && s.requires == .publicContract) = true ∧Coordinated work contains a component-2 step needing public-contract knowledge; the following new cases additionally bind it to a real edge.
L738 PreservesFinite orderedUnique orderedRefactor ∧The refactor preserves ordered behavior on the declared finite contract corpus.
L739 (structuralEvidence .evolvable .designRevision).observedBefore ≠The actual before/after observation lists differ for deliberate design revision; the change is not falsely called preservation.
L740 (structuralEvidence .evolvable .designRevision).observedAfter ∧The actual before/after observation lists differ for deliberate design revision; the change is not falsely called preservation.
L741 staticBatch 21 10 = liveBatch 21 10 ∧ staticBatch 21 5 ≠ liveBatch 21 5 ∧The static batch assumption agrees at runtime size ten but fails at size five for twenty-one items.
L742 changeWork .presentSimple .withdrawal = 17 ∧Withdrawing the simple design's structure takes seventeen units, retaining an eventual-exit cost.
L743 (crossesBoundary boundaryDesign .coordinated coordinatedBoundary = true ∧The coordinated path crosses the actual caller-2/callee-1 boundary.
L744 boundaryObligationChecked boundaryDesign .coordinated coordinatedBoundary = true ∧That boundary's public-contract verification and finite order obligation are fulfilled.
L745 crossesBoundary omittedCallerCheck .coordinated coordinatedBoundary = true ∧The callee edit still crosses the boundary when caller verification is omitted.
L746 boundaryObligationChecked omittedCallerCheck .coordinated coordinatedBoundary = false ∧The omitted caller verification causes the obligation test to fail.
L747 crossesBoundary otherCalleeDesign .coordinated otherCalleeBoundary = false ∧An edge whose callee is component 7 does not match this edit path and is not crossed.
L748 boundaryObligationChecked { boundaryDesign with run := sortedUnique }The same edge and steps with sortedUnique behavior fail actual finite order preservation; decide checks all clauses of this concrete structural bundle.
L749 .coordinated coordinatedBoundary = false) := by decideThe same edge and steps with sortedUnique behavior fail actual finite order preservation; decide checks all clauses of this concrete structural bundle. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L751abbrev DesignCanChange (a : Activity) (design : EngineeringDesign)Generalizes individual capability from a candidate tag to an actual EngineeringDesign with its own paths.
L752 (m : Maintainer) (d : Change) : Prop :=Generalizes individual capability from a candidate tag to an actual EngineeringDesign with its own paths.
L753 design.paths d ≠ [] ∧ m ∈ a.participants ∧Requires an actual nonempty design path and a participating maintainer.
L754 (design.paths d).all (fun step =>Every actual path step must be executable with that maintainer's knowledge and the activity's tools.
L755 (a.available m).contains step.requires && a.tools.contains step.tool) = trueEvery actual path step must be executable with that maintainer's knowledge and the activity's tools.
L757def designWork (design : EngineeringDesign) (d : Change) : Nat :=Computes work from this design object's actual path units, so path mutations can change or preserve the total explicitly.
L758 ((design.paths d).map EditStep.units).sumComputes work from this design object's actual path units, so path mutations can change or preserve the total explicitly.
L760def designModulesNeedingRevision (design : EngineeringDesign) (newSize : Nat) : List Nat :=Finds components whose own recorded batch assumptions differ from the proposed runtime size.
L761 (design.batchAssumptions.filter (fun p => p.2 != newSize)).map Prod.fstFinds components whose own recorded batch assumptions differ from the proposed runtime size.
L763/- In this finite model, a facade adds an actual component, forwarding edgeThe first facade adds a component, forwarding edge and verification step while preserving output; it supplies neither missing private knowledge nor removal of existing edit work.
L764and contract verification step. It preserves observable order but does notThe first facade adds a component, forwarding edge and verification step while preserving output; it supplies neither missing private knowledge nor removal of existing edit work.
L765remove the original edit/compilation work or supply private maintainer knowledge. -/The first facade adds a component, forwarding edge and verification step while preserving output; it supplies neither missing private knowledge nor removal of existing edit work.
L766def introduceBoundary (design : EngineeringDesign) : EngineeringDesign := {Constructs the first explicit boundary-introduction transformation on a complete design.
L767 metadata := { design.metadata with modules := design.metadata.modules + 1, extensionPoints := design.metadata.extensionPoints + 1 },The visible module and extension-point counts both increase by one.
L768 run := fun xs => design.run (xs ++ []),The wrapper appends an empty list to input before calling the original behavior, preserving the result.
L769 paths := fun d => if (design.paths d).isEmpty then [] elseAn absent original path stays absent; merely wrapping cannot create support for an unknown change.
L770 design.paths d ++ [⟨design.components.length, .publicContract, .contractRunner, 1⟩],An existing path gains one public-contract verification unit at the new component identifier.
L771 components := design.components ++ [design.components.length],Adds the original component-list length as a new component identifier; it is fresh for the concrete zero-through-seven starting design.
L772 boundaries := design.boundaries ++Adds a forwarding edge from that new component to component 0 carrying the original signature label.
L773 [⟨design.components.length, 0, design.metadata.signature⟩],Adds a forwarding edge from that new component to component 0 carrying the original signature label.
L774 batchAssumptions := design.batchAssumptions }Leaves all fixed batch assumptions unchanged, so the wrapper does not resolve their coupling.
L776def wrappedDesign : EngineeringDesign := introduceBoundary privateDesignApplies the first facade transformation to the private design for a concrete increased-work counterexample.
L778/- This second facade relocates the existing contract-verification work toThe second facade moves existing verification to the new component instead of adding work; real boundary and path changes still do not supply private knowledge or lower total work.
L779the new component. It changes the actual boundary and step locations withoutThe second facade moves existing verification to the new component instead of adding work; real boundary and path changes still do not supply private knowledge or lower total work.
L780reducing the work or making the private edit knowledge public. -/The second facade moves existing verification to the new component instead of adding work; real boundary and path changes still do not supply private knowledge or lower total work.
L781def relocateVerification (design : EngineeringDesign) : EngineeringDesign := {Begins with the same boundary-introducing design, retaining its new component, edge and equivalent behavior.
L782 introduceBoundary design withBegins with the same boundary-introducing design, retaining its new component, edge and equivalent behavior.
L783 paths := fun d => (design.paths d).map (fun step =>Rebuilds the work paths from the original design's steps, removing the extra appended verification step of the first facade.
L784 if step.tool = .contractRunner then { step with component := design.components.length }Moves each original contractRunner step to the new component while preserving its knowledge, tool and units.
L785 else step) }Leaves every nonverification step unchanged, completing a relocation without changing work units.
L787def sameWorkDesign : EngineeringDesign := relocateVerification privateDesignThe concrete same-work design is the private design after this verification relocation.
L789/-- organon-map CoreReader.Engineering.structureNotCapabilityBegins a provenance comment attaching CoreReader.Engineering.structureNotCapability to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L790software-engineering.structural-judgment#p1 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p1 for CoreReader.Engineering.structureNotCapability, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L791software-engineering.structural-judgment#p2 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p2 for CoreReader.Engineering.structureNotCapability, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L792-/Closes the source-mapping comment for CoreReader.Engineering.structureNotCapability; executable declarations resume after the comment.
L793theorem structureNotCapability :Collects counterexamples showing that signature, module count, principle name and new boundaries do not alone prove the claimed capability or lower work.
L794 (privateDesign.metadata.signature = sortedDesign.metadata.signature ∧Private and sorted designs share a signature but give different order results on [2,1,2]; identical interface shape does not establish contract equivalence.
L795 privateDesign.run [2, 1, 2] = [2, 1] ∧ sortedDesign.run [2, 1, 2] ≠ [2, 1]) ∧Private and sorted designs share a signature but give different order results on [2,1,2]; identical interface shape does not establish contract equivalence.
L796 (privateDesign.metadata.modules = privateDesign.components.length ∧The private design's declared eight modules equal its actual component-list length.
L797 privateDesign.batchAssumptions.length = 8 ∧It contains eight actual recorded batch assumptions, not merely a module-count label.
L798 (designModulesNeedingRevision privateDesign 5).length = 8) ∧All eight components need assumption revision when runtime batch size changes to five.
L799 (privateDesign.metadata.principle = "dependency inversion" ∧The private design carries the dependency-inversion principle name.
L800 privateDesign.metadata = documentedDesign.metadata ∧Private and documented designs share all visible metadata.
L801 ¬ DesignCanChange continuingActivity privateDesign .successor .designRevision ∧Despite that label, the successor cannot revise the private design because its paths need private layout knowledge.
L802 DesignCanChange continuingActivity documentedDesign .successor .designRevision) ∧The successor can revise the documented design with its genuinely different guide-based paths.
L803 (privateDesign.boundaries.length = 0 ∧ wrappedDesign.boundaries.length = 1 ∧The first facade changes the actual boundary count from zero to one.
L804 wrappedDesign.components.length = 9 ∧It also increases actual component count from eight to nine.
L805 wrappedDesign.boundaries = [⟨8, 0, "List Nat → List Nat"⟩] ∧The new actual edge is exactly component 8→0 with the original list-function signature.
L806 wrappedDesign.run [2, 1, 2] = privateDesign.run [2, 1, 2] ∧The first facade retains the original observed output on [2,1,2].
L807 designWork privateDesign .designRevision = 17 ∧The original private design needs seventeen units for design revision.
L808 designWork wrappedDesign .designRevision = 18 ∧The first facade needs eighteen units after its extra verification step.
L809 ¬ designWork wrappedDesign .designRevision < designWork privateDesign .designRevision) ∧Thus this actual boundary introduction does not reduce the intended design-revision work.
L810 (sameWorkDesign.boundaries = [⟨8, 0, "List Nat → List Nat"⟩] ∧The relocation variant also has the concrete edge 8→0.
L811 sameWorkDesign.components.length = 9 ∧The relocation variant has nine actual components.
L812 sameWorkDesign.paths .designRevision ≠ privateDesign.paths .designRevision ∧Its design-revision path differs from the original because verification component identifiers moved.
L813 sameWorkDesign.run [2, 1, 2] = privateDesign.run [2, 1, 2] ∧The relocation retains the original observed order result.
L814 designWork sameWorkDesign .designRevision = designWork privateDesign .designRevision ∧Its total assigned work equals the original path's total exactly.
L815 designWork sameWorkDesign .designRevision = 17 ∧That unchanged total is seventeen units.
L816 ¬ DesignCanChange continuingActivity sameWorkDesign .successor .designRevision) := byThe successor still lacks required private knowledge after relocation, so the new boundary does not establish continuing capability.
L817 exact ⟨by decide, by decide, by decide, by decide, by decide⟩Proves the five concrete counterexample groups by decision procedures on their actual records, functions and arithmetic.
L819/-- organon-map CoreReader.Engineering.contractPreservationBegins a provenance comment attaching CoreReader.Engineering.contractPreservation to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L820software-engineering.structural-judgment#p3 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p3 for CoreReader.Engineering.contractPreservation, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L821-/Closes the source-mapping comment for CoreReader.Engineering.contractPreservation; executable declarations resume after the comment.
L822theorem contractPreservation {Input Output : Type} (scope : Input → Prop)The general preservation theorem is polymorphic in inputs/outputs and keeps an explicitly supplied scope.
L823 (old new : Input → Output) (observations : ∀ x, scope x → new x = old x) :Its premise already supplies equality of new and old behavior for every input in that scope.
L824 PreservesOn scope old new := observationsReturns that same universal scoped equality as PreservesOn; it does not derive universal preservation from finite tests.
L826theorem changedObservationNotPreserved {Input Output : Type} (scope : Input → Prop)A single actual differing observation inside the declared scope refutes scoped preservation.
L827 (old new : Input → Output) (x : Input) (inside : scope x)Fixes the old/new functions, an input and proof that this input lies inside the scope.
L828 (different : new x ≠ old x) : ¬ PreservesOn scope old new := byAssumes an actual output difference there and concludes that preservation cannot hold.
L829 intro hTemporarily assumes scoped preservation.
L830 exact different (h x inside)Specializes preservation to the in-scope counterexample and contradicts its known output difference.
L832theorem contractRevisionObligations (old new : ObservableContract)The revision-obligation theorem compares the same actual old/new observable contracts.
L833 (r : ContractRevision) (account : ContractChangeAccount old new r)Requires a report already satisfying the preservation-or-revision account.
L834 (changed : ¬ PreservesContractFinite old new) :Also assumes that actual finite contract preservation fails.
L835 RevisionDuties old new r := account.resolve_left changedEliminates the preservation alternative, leaving the report's revision duties; it does not manufacture an account from changed behavior alone.
L837def retiredBehavior (xs : List Nat) : List Nat :=The retired behavior changes only input [99], which is outside the declared finite contract corpus, while retaining orderedUnique elsewhere.
L838 if xs = [99] then [] else orderedUnique xsThe retired behavior changes only input [99], which is outside the declared finite contract corpus, while retaining orderedUnique elsewhere.
L840/-- organon-map CoreReader.Engineering.contractCasesBegins a provenance comment attaching CoreReader.Engineering.contractCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L841software-engineering.structural-judgment#p3 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p3 for CoreReader.Engineering.contractCases, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L842-/Closes the source-mapping comment for CoreReader.Engineering.contractCases; executable declarations resume after the comment.
L843theorem contractCases :Collects preservation, deliberate revision, missing-party rejection and procedure flexibility cases.
L844 ContractChangeAccount originalContract refactoredContract normalRevision ∧The refactored contract has a valid account through finite preservation.
L845 ContractChangeAccount originalContract revisedContract normalRevision ∧The revised order/retry contract has a valid account through actual revision duties.
L846 ¬ ContractChangeAccount originalContract revisedContract { normalRevision with affected := [] } ∧An empty acknowledged-party list cannot account for the actual consumer/operator changes.
L847 PreservesFinite orderedUnique retiredBehavior ∧ retiredBehavior [99] ≠ orderedUnique [99] ∧The retired behavior preserves every declared finite input but differs at [99], demonstrating the scope limit.
L848 ContractChangeAccount originalContract revisedContract { normalRevision with procedure := "paired audit" } := by decideChanging the procedure name to paired audit keeps the account valid; no particular procedure is mandated. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L850/-- organon-map CoreReader.Engineering.contractDistinctionsBegins a provenance comment attaching CoreReader.Engineering.contractDistinctions to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L851software-engineering.structural-judgment#p3 sha256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42Records the source reference software-engineering.structural-judgment/p3 for CoreReader.Engineering.contractDistinctions, with direct-body SHA256 8014457feae3410a7220426dbbe4293f7b5d1d2aa152f4085ccd1f03d5983a42. This is a traceability binding, not a new premise or semantic proof.
L852-/Closes the source-mapping comment for CoreReader.Engineering.contractDistinctions; executable declarations resume after the comment.
L853theorem contractDistinctions :Separates actual order preservation, retry change, party effects and accurate historical contract reporting.
L854 PreservesFinite orderedUnique orderedRefactor ∧The append-empty refactor preserves the finite ordered contract.
L855 ¬ PreservesFinite orderedUnique sortedUnique ∧Sorting before de-duplication does not preserve that same order contract.
L856 retry originalContract 3 = false ∧ retry revisedContract 3 = true ∧At attempt index three the old threshold forbids retry but the new threshold allows it, making failure-policy change concrete.
L857 ¬ PreservesContractFinite originalContract revisedContract ∧The combined order/retry contract therefore is not preserved.
L858 affectedParties originalContract revisedContract = ["queue consumer", "queue operator"] ∧The fixed dependency map identifies exactly the consumer and operator as affected in this example.
L859 ¬ ContractChangeAccount originalContract revisedContractAcknowledging only the consumer omits the operator affected by retry change, so the revision account fails.
L860 { normalRevision with affected := ["queue consumer"] } ∧Acknowledging only the consumer omits the operator affected by retry change, so the revision account fails.
L861 ¬ ContractChangeAccount originalContract revisedContractChanging both reported old-limit fields to five still fails because the independent actual old contract has threshold three.
L862 { normalRevision with oldFailureLimit := 5, recordedOldFailureLimit := 5 } ∧Changing both reported old-limit fields to five still fails because the independent actual old contract has threshold three.
L863 ContractChangeAccount originalContract revisedContract normalRevision ∧The unaltered normalRevision correctly accounts for the deliberate changes.
L864 PreservesFinite orderedUnique retiredBehavior ∧ retiredBehavior [99] ≠ orderedUnique [99] := by decideFinite preservation still allows the intentionally out-of-scope difference at [99]; it is not all-input equivalence. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L866/- Revision records time-indexed evidence rather than changing a past event.Revision concerns current choices under time-indexed evidence; it does not alter the truth of an already observed prediction.
L867Judgment is choice under current evidence; forecast truth is a separate value. -/Revision concerns current choices under time-indexed evidence; it does not alter the truth of an already observed prediction.
L868structure RevisionState whereA revision state records the current evidence, maintenance setting, costs, objectives and selected design at one time.
L869 time : NatOrders states by a natural-number time index.
L870 forecast : List ChangeRecords expected future change directions.
L871 maintenance : NatRecords the amount of expected maintenance.
L872 maintainers : List MaintainerRecords who is expected to maintain the software.
L873 migrationCost : NatRecords the relevant migration cost.
L874 objectiveCapacity : NatRecords the objective's capacity against that cost.
L875 choice : CandidateRecords the design chosen under those conditions.
L876 deriving DecidableEq, ReprAutomatically provides equality decisions and printable representations for RevisionState; these support concrete case evaluation, not a philosophical claim about that type.
L877structure RevisionRecord whereA revision record keeps actual and reported states plus a separately checkable prediction outcome and criticism coverage.
L878 software : StringBinds the report to a named software task.
L879 old : RevisionStateCarries the old state claimed by the report.
L880 current : RevisionStateCarries the current state.
L881 recordedOld : RevisionStatePreserves what the report records about the old state for comparison with independent history.
L882 recordedCurrent : RevisionStatePreserves what it records about the current state.
L883 predictedBatchCount : NatStates the earlier predicted batch count.
L884 actualBatchCount : NatStates the actually observed batch count.
L885 reportedPredictionSucceeded : BoolRecords whether the report declares the prediction successful; later checks bind this Boolean to actual historical equality.
L886 consideredChanges : List ChangeLists change directions considered by this revision.
L887 criticizedDirections : List ChangeLists directions kept within the declared criticism scope.
L889abbrev MaterialGroundsChanged (old current : RevisionState) : Prop :=Material changes concern substantive grounds rather than a mere later timestamp or relabeled choice.
L890 old.forecast ≠ current.forecast ∨ old.maintenance ≠ current.maintenance ∨A change in expected directions or maintenance amount counts as changed grounds.
L891 old.maintainers ≠ current.maintainers ∨Changing the maintainers also changes the relevant conditions.
L892 old.migrationCost ≠ current.migrationCost ∨ old.objectiveCapacity ≠ current.objectiveCapacityChanged migration cost or objective capacity supplies another material-ground difference.
L894def oldState : RevisionState := ⟨0, [.designRevision], 6, [.original], 8, 12, .evolvable⟩The old state at time zero expects design revision, six maintenance units, the original maintainer, cost eight/capacity twelve and evolvable.
L895def newState : RevisionState := ⟨1, [.deletion], 2, [.successor, .agent], 14, 10, .presentSimple⟩The new state at time one expects deletion, two maintenance units, successor/agent maintainers, cost fourteen/capacity ten and simple.
L897structure HistoricalEvidence whereHistoricalEvidence is an input separate from the mutable report, anchoring the task, old state and past prediction/observation.
L898 software : StringIdentifies which software the historical event concerns.
L899 state : RevisionStatePreserves the actual historical revision state.
L900 predictedBatchCount : NatPreserves the historical prediction independently of the new report.
L901 actualBatchCount : NatPreserves the historical observed result independently of the report.
L903/- Independent event content: the recorded predictor used a fixed batch sizeThe recorded event used a predictor fixed at ten while reality used runtime size five for twenty-one items; the mismatch is retained as event content.
L904of ten; the actual event had runtime size five and twenty-one queue items. -/The recorded event used a predictor fixed at ten while reality used runtime size five for twenty-one items; the mismatch is retained as event content.
L905def observedHistory : HistoricalEvidence :=Fixes the queue history to oldState, predicted count three and actual count five computed by the two real functions.
L906 ⟨"order-preserving queue", oldState, staticBatch 21 5, liveBatch 21 5⟩Fixes the queue history to oldState, predicted count three and actual count five computed by the two real functions.
L908abbrev RevisionAccountAgainst (history : HistoricalEvidence) (r : RevisionRecord) : Prop :=Checks a report against this independently supplied historical object, rather than comparing report fields only with each other.
L909 r.software = history.software ∧The report's software identity must match the historical task.
L910 r.old = history.state ∧ r.recordedOld = history.state ∧Both its old-state claim and recorded old state must equal the independent historical state.
L911 r.predictedBatchCount = history.predictedBatchCount ∧The report must retain the actual historical predicted count.
L912 r.actualBatchCount = history.actualBatchCount ∧It must retain the actual historical observed count.
L913 r.old.time < r.current.time ∧ r.recordedCurrent = r.current ∧Time must advance, and the current-state record must accurately reflect the current state.
L914 (r.old.choice ≠ r.current.choice → MaterialGroundsChanged r.old r.current) ∧A changed design choice requires material grounds to have changed; this condition alone is not a proof that every such redesign is substantively justified.
L915 r.reportedPredictionSucceeded = decide (history.predictedBatchCount = history.actualBatchCount) ∧The reported success flag must equal the decision of actual historical prediction/observation equality, preventing retrospective relabeling.
L916 r.consideredChanges.all (fun d => r.criticizedDirections.contains d) = trueEvery considered direction must remain in the listed criticism scope; this finite coverage is not a universal proof of reflexive correctness.
L918/-- organon-map CoreReader.Engineering.RevisionAccountBegins a provenance comment attaching CoreReader.Engineering.RevisionAccount to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L919software-engineering.revision#p2 sha256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99Records the source reference software-engineering.revision/p2 for CoreReader.Engineering.RevisionAccount, with direct-body SHA256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99. This is a traceability binding, not a new premise or semantic proof.
L920software-engineering.revision#p1 sha256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99Records the source reference software-engineering.revision/p1 for CoreReader.Engineering.RevisionAccount, with direct-body SHA256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99. This is a traceability binding, not a new premise or semantic proof.
L921-/Closes the source-mapping comment for CoreReader.Engineering.RevisionAccount; executable declarations resume after the comment.
L922abbrev RevisionAccount (r : RevisionRecord) : Prop := RevisionAccountAgainst observedHistory rSpecializes the generic history-bound account to the fixed observed queue history.
L924theorem failedHistoryNotRewritten (history : HistoricalEvidence) (r : RevisionRecord)The anti-rewriting result works for any supplied history and report, not only the queue numbers.
L925 (account : RevisionAccountAgainst history r)Assumes that the report satisfies the full account against that same historical object.
L926 (failed : history.predictedBatchCount ≠ history.actualBatchCount) :Assumes the actual historical prediction differs from the observation.
L927 r.reportedPredictionSucceeded = false := byConcludes that an accurate report must mark the prediction unsuccessful.
L928 simpa [failed] using account.2.2.2.2.2.2.2.2.1Extracts the account's success-flag equality and simplifies it using the historical failure premise, yielding false.
L930def revisionRecord : RevisionRecord := {Builds the ordinary revision report with accurate old/new states and the preserved failed forecast.
L931 software := "order-preserving queue",Uses the same order-preserving queue identity as observedHistory.
L932 old := oldState, current := newState, recordedOld := oldState, recordedCurrent := newState,Actual and recorded states agree with oldState and newState respectively.
L933 predictedBatchCount := staticBatch 21 5, actualBatchCount := liveBatch 21 5,Uses the actual static/live counts for twenty-one items at runtime size five.
L934 reportedPredictionSucceeded := false,Truthfully marks that prediction unsuccessful.
L935 consideredChanges := changes, criticizedDirections := changes }Considers all nine ordinary directions and keeps all nine within criticism scope.
L937abbrev SupportedAlternative (gs : List DirectionGround) (d : Change) : Prop := credible gs dFor this retention adapter, a supported alternative is a direction credible under the context's ground interpretation.
L939abbrev RetentionJustified (ctx : Context) (alternatives : List Change) : Prop :=Retention may be justified by the declared lack-of-contribution or concrete-cost conditions; this is an application criterion.
L940 alternatives.all (fun d => !decide (SupportedAlternative ctx.evidence d)) = true ∨One branch requires every listed alternative to lack credible support in the context.
L941 JustifiedDeparture ctx .evolvableThe other branch permits retention through an explicitly justified evolvable cost departure.
L943def stableRecord : RevisionRecord := { revisionRecord withThe stable variant keeps the chosen design evolvable in both actual and recorded current states, while retaining changed evidence, honest failed prediction and criticism coverage.
L944 current := { newState with choice := .evolvable },The stable variant keeps the chosen design evolvable in both actual and recorded current states, while retaining changed evidence, honest failed prediction and criticism coverage.
L945 recordedCurrent := { newState with choice := .evolvable } }The stable variant keeps the chosen design evolvable in both actual and recorded current states, while retaining changed evidence, honest failed prediction and criticism coverage.
L947/-- organon-map CoreReader.Engineering.revisionCasesBegins a provenance comment attaching CoreReader.Engineering.revisionCases to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L948software-engineering.revision#p2 sha256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99Records the source reference software-engineering.revision/p2 for CoreReader.Engineering.revisionCases, with direct-body SHA256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99. This is a traceability binding, not a new premise or semantic proof.
L949software-engineering.revision#p1 sha256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99Records the source reference software-engineering.revision/p1 for CoreReader.Engineering.revisionCases, with direct-body SHA256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99. This is a traceability binding, not a new premise or semantic proof.
L950-/Closes the source-mapping comment for CoreReader.Engineering.revisionCases; executable declarations resume after the comment.
L951theorem revisionCases :Exhibits a valid revision with all five material-ground differences, a preserved prediction failure and two justifications for retention.
L952 RevisionAccount revisionRecord ∧The ordinary report satisfies the account against the fixed independent history.
L953 revisionRecord.old.forecast ≠ revisionRecord.current.forecast ∧Its forecast changes from design revision to deletion.
L954 revisionRecord.old.maintenance ≠ revisionRecord.current.maintenance ∧Its maintenance amount changes from six to two.
L955 revisionRecord.old.maintainers ≠ revisionRecord.current.maintainers ∧Its maintainer set changes from the original author to successor and agent.
L956 revisionRecord.old.migrationCost ≠ revisionRecord.current.migrationCost ∧Its migration cost changes from eight to fourteen.
L957 revisionRecord.old.objectiveCapacity ≠ revisionRecord.current.objectiveCapacity ∧Its objective capacity changes from twelve to ten.
L958 revisionRecord.predictedBatchCount ≠ revisionRecord.actualBatchCount ∧The prediction three still differs from the actual five; revising the decision does not change this failure.
L959 RetentionJustified currentContinuing [.other "quantum backend"] ∧A quantum-backend alternative lacking credible grounds supplies the no-supported-alternative retention case.
L960 RetentionJustified (threatened .migration) [.migration] := by decideA genuine migration-capacity threat supplies the cost-based retention case. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L962def observations : List (Nat × Nat) := [(21, 10), (30, 10), (40, 10)]The successful observation set uses only runtime size ten with item counts twenty-one, thirty and forty.
L963def revisionsMade : List Nat := [1, 2, 3]Records three revision identifiers, whose count alone will not establish correctness.
L964def agreedBatch (reviewers : List Maintainer) (items size : Nat) : List Nat :=Every named reviewer reports the same static predictor result, modeling agreement without adding independent support or changing the actual predictor.
L965 reviewers.map (fun _ => staticBatch items size)Every named reviewer reports the same static predictor result, modeling agreement without adding independent support or changing the actual predictor.
L967def rewrittenOldRecord : RevisionRecord := { revisionRecord withThe first tampering variant changes both claimed and recorded old forecasts together, testing that agreement between report fields cannot override independent history.
L968 old := { oldState with forecast := [.deletion] },The first tampering variant changes both claimed and recorded old forecasts together, testing that agreement between report fields cannot override independent history.
L969 recordedOld := { oldState with forecast := [.deletion] } }The first tampering variant changes both claimed and recorded old forecasts together, testing that agreement between report fields cannot override independent history.
L971def rewrittenPredictionRecord : RevisionRecord := { revisionRecord withThe second variant changes the predicted count to five and calls it successful, attempting to rewrite the old prediction to match observation.
L972 predictedBatchCount := 5, reportedPredictionSucceeded := true }The second variant changes the predicted count to five and calls it successful, attempting to rewrite the old prediction to match observation.
L974def rewrittenObservationRecord : RevisionRecord := { revisionRecord withThe third variant changes the observed count to three and calls the prediction successful, attempting to rewrite the actual event.
L975 actualBatchCount := 3, reportedPredictionSucceeded := true }The third variant changes the observed count to three and calls the prediction successful, attempting to rewrite the actual event.
L977def unrelatedSoftwareRecord : RevisionRecord := {The identity variant assigns the report to unrelated software while keeping its numerical data, testing task binding.
L978 revisionRecord with software := "unrelated batch processor" }The identity variant assigns the report to unrelated software while keeping its numerical data, testing task binding.
L980theorem historicalTamperingRejected :Shows that fixed historical evidence rejects coordinated report-field tampering and software-identity substitution.
L981 RevisionAccount revisionRecord ∧The unchanged report remains valid.
L982 ¬ RevisionAccount rewrittenOldRecord ∧Changing both old-state fields cannot satisfy the independently fixed history.
L983 ¬ RevisionAccount rewrittenPredictionRecord ∧Rewriting the predicted count and success flag is rejected.
L984 ¬ RevisionAccount rewrittenObservationRecord ∧Rewriting the observed count and success flag is also rejected.
L985 observedHistory.predictedBatchCount = 3 ∧ observedHistory.actualBatchCount = 5 ∧The independent history retains prediction three and observation five throughout these variants.
L986 ¬ RevisionAccount unrelatedSoftwareRecord := byA report for unrelated software fails the task-identity requirement.
L987 exact ⟨by decide, by decide, by decide, by decide, by decide, by decide, by decide⟩Computes all seven concrete validity/failure and historical-number clauses without editing the historical object.
L989/-- organon-map CoreReader.Engineering.revisionLimitsBegins a provenance comment attaching CoreReader.Engineering.revisionLimits to the source clauses listed below; the comment does not alter Lean meaning or prove correspondence.
L990software-engineering.revision#p2 sha256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99Records the source reference software-engineering.revision/p2 for CoreReader.Engineering.revisionLimits, with direct-body SHA256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99. This is a traceability binding, not a new premise or semantic proof.
L991software-engineering.revision#p1 sha256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99Records the source reference software-engineering.revision/p1 for CoreReader.Engineering.revisionLimits, with direct-body SHA256 5d31bed0197ea7e7028eb7a85e56059516421c6c27613cc5479e0b98c5111d99. This is a traceability binding, not a new premise or semantic proof.
L992-/Closes the source-mapping comment for CoreReader.Engineering.revisionLimits; executable declarations resume after the comment.
L993theorem revisionLimits :Collects limits on retrospective success, revision count, agreement, repeated local success and justified stability.
L994 RevisionAccount revisionRecord ∧The ordinary historical account is valid.
L995 ¬ RevisionAccount { revisionRecord with reportedPredictionSucceeded := true } ∧Merely flipping reportedPredictionSucceeded to true invalidates the account.
L996 revisionsMade.length = 3 ∧Three revisions have occurred in the explicit list, but their number supplies no correctness theorem.
L997 agreedBatch maintainers 21 5 = [3, 3, 3] ∧ liveBatch 21 5 = 5 ∧All three maintainers agree on the static result three, while the live result is five; agreement does not erase the counterexample.
L998 observations.all (fun p => staticBatch p.1 p.2 == liveBatch p.1 p.2) = true ∧Every listed size-ten observation agrees between static and live predictors.
L999 staticBatch 21 5 ≠ liveBatch 21 5 ∧Those repeated successes coexist with a failure at runtime size five.
L1000 RevisionAccount stableRecord ∧ stableRecord.current.choice = stableRecord.old.choice ∧The stable report remains history-valid and keeps the old design choice, showing revision openness need not force every act to change design.
L1001 RetentionJustified currentContinuing [.other "quantum backend"] := byThe unsupported quantum-backend alternative still permits retaining the current design.
L1002 refine ⟨by decide, ?_, by decide, by decide, by decide, by decide,Builds the conjunction with finite decisions, leaving only the falsely reported-success account to an explicit reduction.
L1003 by decide, by decide, by decide, by decide⟩Builds the conjunction with finite decisions, leaving only the falsely reported-success account to an explicit reduction.
L1004 dsimp [RevisionAccount, RevisionAccountAgainst, observedHistory, MaterialGroundsChanged, revisionRecord, oldState, newState]Expands the fixed history, actual report and material-change predicates so the false success claim is exposed as the concrete three-versus-five mismatch.
L1005 decideThe remaining decidable contradiction is checked computationally.
L1007def groundedChanges : DirectionGround → List ChangeExtracts each record's listed directions regardless of ground constructor; this extraction records forecast content and does not itself prove credibility.
L1008 | .plan _ ds | .knowledge _ ds _ | .history _ ds | .other _ ds => dsExtracts each record's listed directions regardless of ground constructor; this extraction records forecast content and does not itself prove credibility.
L1010def currentRevisionState (ctx : Context) (chosen : Candidate) : RevisionState := {Builds a current revision state from the actual context and selected design rather than independent report placeholders.
L1011 time := 1, forecast := ctx.evidence.flatMap groundedChanges,Sets time one and concatenates the directions listed in the actual context evidence into the forecast.
L1012 maintenance := ctx.activity.scheduledMaintenance, maintainers := ctx.activity.participants,Copies maintenance amount and participating maintainers from the same activity.
L1013 migrationCost := cost chosen .migration,Uses the selected design's actual assigned migration cost.
L1014 objectiveCapacity := ctx.limits.capacity .migration,Uses the same context's migration objective capacity.
L1015 choice := chosen }Records the actual chosen candidate.
L1017def revisionFor (ctx : Context) (chosen : Candidate) : RevisionRecord := {The report retains historical data from stableRecord but binds software, actual current state and recorded current state to this context and chosen candidate.
L1018 stableRecord with software := ctx.activity.software, current := currentRevisionState ctx chosen, recordedCurrent := currentRevisionState ctx chosen }The report retains historical data from stableRecord but binds software, actual current state and recorded current state to this context and chosen candidate.
L1020theorem revisionContextIdentity :Checks that the instantiated revision report really belongs to the shared engineering context and satisfies its fixed-history account.
L1021 (revisionFor currentContinuing .evolvable).software = currentContinuing.activity.software ∧Its software identifier equals the activity's actual identifier.
L1022 (revisionFor currentContinuing .evolvable).software = observedHistory.software ∧ (revisionFor currentContinuing .evolvable).current.maintenance =The same identifier matches historical evidence, and current maintenance equals the activity's schedule.
L1023 currentContinuing.activity.scheduledMaintenance ∧The same identifier matches historical evidence, and current maintenance equals the activity's schedule.
L1024 (revisionFor currentContinuing .evolvable).current.maintainers = currentContinuing.activity.participants ∧Current maintainers equal the actual participant list.
L1025 (revisionFor currentContinuing .evolvable).current.migrationCost = cost .evolvable .migration ∧Current migration cost equals evolvable's assigned cost.
L1026 (revisionFor currentContinuing .evolvable).current.objectiveCapacity =Current objective capacity equals the shared context's migration capacity.
L1027 currentContinuing.limits.capacity .migration ∧Current objective capacity equals the shared context's migration capacity.
L1028 (revisionFor currentContinuing .evolvable).current.choice = .evolvable ∧The recorded current choice is actually evolvable.
L1029 RevisionAccount (revisionFor currentContinuing .evolvable) := by decideThe fully bound report satisfies RevisionAccount; the concrete checks are decided from its actual fields. The closing by decide proves the stated concrete proposition by evaluating its decision procedure; it does not generalize beyond the displayed objects and scope.
L1031/- Whole domain satisfaction keeps actual subject, credibility, account andThe whole domain bundle retains actual subject, credibility, accounts and revision duties on one context. Its chosen finite application records do not claim universal engineering adequacy.
L1032revision duties. The same context is passed to priority and every domain duty.The whole domain bundle retains actual subject, credibility, accounts and revision duties on one context. Its chosen finite application records do not claim universal engineering adequacy.
L1033Application account choices below are finite records, not universal claims. -/The whole domain bundle retains actual subject, credibility, accounts and revision duties on one context. Its chosen finite application records do not claim universal engineering adequacy.
L1034abbrev DomainSatisfied (ctx : Context) (chosen : Candidate) : Prop :=Combine the represented domain duties for one context and selected design. This bundle has no unconditional Meets field; priority applicability is not an overall requirement-rejection test.
L1035 ActivityScope ctx.activity ∧ EvolutionPriority ctx chosen ∧Require ActivityScope and the conditional EvolutionPriority. If PriorityConditions is false, that implication holds vacuously; this conjunct does not reject the choice for unmet requirements, while the remaining domain duties still apply.
L1036 credible ctx.evidence .designRevision ∧Requires actual credible grounds for the design-revision direction.
L1037 (ctx.departure ≠ none → JustifiedDeparture ctx .evolvable) ∧If a departure is recorded, it must be a justified concrete-cost departure; absent departure creates no extra exception.
L1038 EvolutionClaim ctx.activity chosen ⟨.designRevision, .successor, .revise⟩ ∧Requires the successor's actual design-revision capability with explicit revision of obligations.
L1039 StructuralAccount ctx.activity chosen (structuralEvidence chosen .designRevision) ∧Requires a structural account matching the same activity, chosen candidate and design-revision evidence.
L1040 ContractChangeAccount (orderContract (behavior chosen)) (evolutionContract .designRevision) normalRevision ∧Requires a preservation-or-revision account comparing the selected design's order contract with the actual design-revision contract.
L1041 RevisionAccount (revisionFor ctx chosen)Requires the same context/candidate revision report to satisfy the fixed independent historical account.
L1043theorem currentDomainSatisfied : DomainSatisfied currentContinuing .evolvable := byConstructs actual whole-domain satisfaction for the shared continuing evolvable example.
L1044 refine ⟨by decide, by decide, by decide, ?_, by decide, by decide, by decide, by decide⟩Computes the concrete subject, priority, credibility, change, structural, contract and history obligations; leaves the conditional departure check.
L1045 simp [currentContinuing]The ordinary context records departure=none, so the implication requiring justification for a recorded departure is vacuously satisfied; priority itself still has actual applicability and no cost escape.
L1047end CoreReader.EngineeringCloses the engineering namespace; all declarations above remain available under CoreReader.Engineering.