leanified/CoreReader/Engineering/Values.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 · 201 lines

LeanLine explanation

L1import CoreReader.Adopted

Import CoreReader.Adopted, making its declarations and transitive dependencies available; this line adds no new proposition.

L2import CoreReader.Engineering.Domain

Import CoreReader.Engineering.Domain, making its declarations and transitive dependencies available; this line adds no new proposition.

L4namespace CoreReader.Engineering

Open namespace CoreReader.Engineering for the following declarations.

L6open CoreReader.Logic CoreReader.Evidence CoreReader.Adopted

Allow unqualified references to declarations in CoreReader.Logic CoreReader.Evidence CoreReader.Adopted; their meaning is unchanged.

L8inductive CoreCommitment | generation | consistency | reflexivity | grounds | choice

Define five Core commitment identifiers: generation, consistency, reflexivity, grounds and choice.

L9  deriving DecidableEq, Repr

Derive DecidableEq, Repr: decidable equality and printable representations of these constructors.

L11def coreCommitments : List CoreCommitment :=

coreCommitments is the finite list of all represented commitment identifiers.

L12  [.generation, .consistency, .reflexivity, .grounds, .choice]

List each of the five constructors once, in the displayed order.

L14/- Initial adoption is explicit. The following reasons neither infer adoption

Comment identifies adoption as an explicit starting choice; reasons do not infer the adoption itself.

L15from facts nor claim that every alternative value position is untenable. -/

Comment rejects both deriving adoption from facts and claiming all alternative values untenable.

L16def coreAdopted (_ : CoreCommitment) : Bool := true

Every commitment is explicitly marked adopted; no factual premise derives this Boolean choice.

L18inductive AdoptionReason

AdoptionReason is a typed family of concrete rationale data, not itself a proof.

L19  | plannedChange (release : Nat) (direction : Change)

plannedChange records a natural-number release and a Change direction.

L20  | incompatibleOrders (input : List Nat)

incompatibleOrders stores the actual input list used to compare output orders.

L21  | ownMethodCounterexample (items size : Nat)

ownMethodCounterexample stores item count and runtime size.

L22  | unsupportedScope (items observedSize extendedSize : Nat)

unsupportedScope distinguishes observed and extended sizes for a fixed item count.

L23  | statusBudgetContrast (statusSelected : Candidate) (capacity : Nat)

statusBudgetContrast records a status-selected alternative and a natural-number capacity.

L24  deriving DecidableEq, Repr

Derive DecidableEq, Repr: decidable equality and printable representations of these constructors.

L26def reasonFor : CoreCommitment → AdoptionReason

Assign one concrete rationale value to every Core commitment.

L27  | .generation => .plannedChange 2 .designRevision

Generation uses planned release 2 and designRevision.

L28  | .consistency => .incompatibleOrders [2, 1, 2]

Consistency uses the order-sensitive input [2, 1, 2].

L29  | .reflexivity => .ownMethodCounterexample 21 5

Reflexivity uses 21 items at runtime size 5.

L30  | .grounds => .unsupportedScope 21 10 5

Grounds compares observation at size 10 with extension to size 5 for 21 items.

L31  | .choice => .statusBudgetContrast .maximal 12

Choice contrasts maximal against understanding capacity 12.

L33/- Each factual reason has contents specific to the principle's purpose. The

Comment introduces factual reasons specialized to each principle's purpose.

L34context is the very continuing activity and its current requirements/grounds.

Comment fixes their context to this continuing activity and its actual requirements/evidence.

L35Matching a constructor alone is insufficient: the represented facts must hold. -/

Comment requires actual reason contents to hold, beyond matching constructor names.

L36abbrev ReasonRelevant : CoreCommitment → AdoptionReason → Candidate → Prop

ReasonRelevant is a proposition on principle, structured reason and selected design; it checks actual reason content.

L37  | .generation, .plannedChange release direction, _ =>

For generation with a planned-change reason, selection is irrelevant to this branch.

L38      DirectionGround.plan release [direction, .migration] ∈ currentContinuing.evidence ∧

The precise release plan containing direction and migration must occur in current evidence.

L39      credible currentContinuing.evidence direction ∧ Continuing currentContinuing.activity

That direction must be credible and the current activity continuing.

L40  | .consistency, .incompatibleOrders input, _ =>

For consistency, use the input carried by the incompatible-orders reason.

L41      currentContinuing.required.orderRequired = true ∧

The actual current requirements must demand order preservation.

L42      orderedUnique input ≠ sortedUnique input

Order-preserving and sorted duplicate removal must differ on that input.

L43  | .reflexivity, .ownMethodCounterexample items size, _ =>

For reflexivity, use the reason's item count and challenged size.

L44      staticBatch items 10 = liveBatch items 10 ∧ staticBatch items size ≠ liveBatch items size

Require agreement at old size 10 and disagreement at the challenged size.

L45  | .grounds, .unsupportedScope items observedSize extendedSize, _ =>

For grounds, compare the reason's observed and extended sizes.

L46      staticBatch items observedSize = liveBatch items observedSize ∧

Static and live forecasts must agree at the observed size.

L47      staticBatch items extendedSize ≠ liveBatch items extendedSize

They must disagree at the proposed extended size.

L48  | .choice, .statusBudgetContrast candidate capacity, selected =>

For choice, distinguish the contrasted candidate from the actually selected design.

L49      capacity = currentContinuing.limits.capacity .understanding ∧

The stated capacity must equal the current understanding capacity.

L50      capacity < abstractionComplexity candidate ∧ abstractionComplexity selected ≤ capacity

The contrasted candidate exceeds that capacity while the actual selection stays within it.

L51  | _, _, _ => False

Any mismatched principle/reason constructors yield False.

L53abbrev valueScope (selected : Candidate) : Prop := abstractionComplexity selected ≤ 3

The value procedure's disclosed scope is designs of abstraction complexity at most 3.

L55/- A small operational experiment explains each adopted safeguard's purpose.

Comment introduces a small operational experiment explaining each safeguard's purpose.

L56These consequences are limited to the stated experiment, not a total value score.

Comment limits consequences to that experiment, excluding a total value score.

L57The disabled branch supplies a real contrast for this application policy. -/

Comment identifies the disabled branch as an actual contrast within this application policy.

L58def safeguardExperiment (principle : CoreCommitment) (enabled : Bool)

safeguardExperiment varies a named safeguard's enabled Boolean.

L59    (selected : Candidate) : Bool :=

It also takes the actual selected design and returns an operational Boolean result.

L60  match principle with

Select the experiment by principle; this is no aggregate value metric.

L61  | .generation =>

The generation branch measures availability of a credible planned change.

L62      let allowed : List Change := if enabled then [.designRevision, .migration] else []

Enable both designRevision and migration, or disable them with an empty allowed list.

L63      allowed.contains .designRevision && decide (credible currentContinuing.evidence .designRevision)

Pass only if designRevision is allowed and currently credible.

L64  | .consistency =>

The consistency branch measures refusal of incompatible simultaneous demands.

L65      let firstDemand := orderedUnique [2, 1, 2]

Compute the first demand using order-preserving duplicate removal.

L66      let secondDemand := sortedUnique [2, 1, 2]

Compute the second demand using sorted duplicate removal on the same input.

L67      let permitsBoth := if enabled then firstDemand == secondDemand else true

An enabled check permits both demands only if equal; disabling it permits both unconditionally.

L68      !permitsBoth

The experiment succeeds when simultaneous permission is rejected.

L69  | .reflexivity =>

The reflexivity branch tests the actual batch forecast on itself.

L70      let selfTests := if enabled then [(21, 10), (21, 5)] else [(21, 10)]

Enable the old and challenged sizes, or retain only the old size when disabled.

L71      selfTests.any (fun point => staticBatch point.1 point.2 != liveBatch point.1 point.2)

Pass when some listed point yields unequal static and live forecasts.

L72  | .grounds =>

The grounds branch tests the licensed input scope.

L73      let licensed := if enabled then [10] else [10, 5]

Enable licensing only size 10; disabling broadens licensing to 10 and 5.

L74      licensed.all (fun size => staticBatch 21 size == liveBatch 21 size)

Require forecast equality for every licensed size, with 21 items fixed.

L75  | .choice =>

The choice branch measures conformity to understanding capacity.

L76      let selectedByRule := if enabled then selected else .maximal

Enable the supplied choice, or select maximal when the safeguard is disabled.

L77      decide (abstractionComplexity selectedByRule ≤ currentContinuing.limits.capacity .understanding)

Decide whether that actual rule selection fits the current understanding capacity.

L79def criticismFor : CoreCommitment → String

Assign a revisability/criticism response string to each principle.

L80  | .generation => "Reconsider this reason if the committed change or continuing maintenance ends."

The generation response identifies loss of committed change or ongoing maintenance as a reconsideration condition.

L81  | .consistency => "Reconsider the comparison if the parties deliberately revise the observable order contract."

The consistency response allows reconsidering the comparison after deliberate revision of the order contract.

L82  | .reflexivity => "This counterexample concerns the stated batch rule; it does not validate all self-assessment."

The reflexivity response limits the counterexample to this batch rule, not all self-assessment.

L83  | .grounds => "A new input condition requires its own support; success at size ten does not cover size five."

The grounds response denies extending size-10 success to size 5 without its own support.

L84  | .choice => "If objectives or budgets change, compare the actual alternatives and reasons again."

The choice response calls for renewed comparison if objectives or budgets change.

L86def governancePosition (principle : CoreCommitment) : ValuePosition Candidate where

For one principle, build a ValuePosition over Candidate with explicit adoption and bounded supporting reasons.

L87  Position := Bool

The value-position alternatives are Boolean enabled/disabled states.

L88  Outcome := Bool

The experiment's outcome type is Bool.

L89  adopted := true

Adopt the enabled value position explicitly.

L90  selected _ := coreAdopted principle

For every design, selected position is that principle's adoption flag.

L91  outcome selected enabled := safeguardExperiment principle enabled selected

Outcomes run the same principle's experiment using design and enabled position.

L92  objective result := result = true

The objective is experiment success, represented by true.

L93  constraints selected _ := valueScope selected

Constraints require the design's valueScope regardless of Boolean position.

L94  starting := singleton valueScope

The starting theory consists solely of the valueScope proposition.

L95  reasons := [fun selected _ => ReasonRelevant principle (reasonFor principle) selected]

The singleton reason requires actual relevance for the same principle and selected design.

L96  limits := valueScope

The application limit is again valueScope.

L97  relevantCriticism _ := True

All Candidate values count as relevant criticism; no narrower filter is encoded.

L98  response _ := some (criticismFor principle)

Every criticism receives the principle's fixed response string.

L100theorem adoptionReasonRelevant (principle : CoreCommitment) (selected : Candidate)

Prove reason relevance for every principle and selected design within scope.

L101    (scope : valueScope selected) : ReasonRelevant principle (reasonFor principle) selected := by

The premise bounds selected complexity by 3; the conclusion uses its exact reasonFor value.

L102  cases principle

Split the five principle constructors.

L103  · dsimp only [ReasonRelevant, reasonFor]; decide

For generation, unfold reason content and compute plan membership, credibility and continuation.

L104  · dsimp only [ReasonRelevant, reasonFor]; decide

For consistency, unfold and compute the order requirement and differing outputs.

L105  · dsimp only [ReasonRelevant, reasonFor]; decide

For reflexivity, unfold and compute old success and challenged forecast failure.

L106  · dsimp only [ReasonRelevant, reasonFor]; decide

For grounds, unfold and compute observed equality and extended inequality.

L107  · refine ⟨rfl, by decide, ?_⟩

For choice, prove capacity identity and maximal over-budget, leaving the selected-design bound.

L108    exact Nat.le_trans scope (by decide)

Chain selected complexity ≤ 3 with 3 ≤ 12 to obtain the required bound.

L110theorem safeguardEnabled (principle : CoreCommitment) (selected : Candidate)

Prove the enabled experiment succeeds for every principle within the disclosed scope.

L111    (scope : valueScope selected) : safeguardExperiment principle true selected = true := by

Retain the scope premise and state an actual Boolean equality to true.

L112  cases principle

Split by the five principles to compute each distinct experiment.

L113  · dsimp only [safeguardExperiment]; decide

For generation, expand the enabled change list and decide the credibility test.

L114  · dsimp only [safeguardExperiment]; decide

For consistency, expand the enabled comparison and decide rejection of incompatible demands.

L115  · dsimp only [safeguardExperiment]; decide

For reflexivity, expand the two tests and decide existence of a failed forecast.

L116  · dsimp only [safeguardExperiment]; decide

For grounds, expand the licensed size-10 list and decide its test success.

L117  · apply decide_eq_true

Convert the choice experiment's Boolean result into its underlying capacity proposition.

L118    exact Nat.le_trans scope (by change 3 ≤ 12; decide)

Use scope and the computed 3 ≤ 12 bound to prove that capacity proposition.

L120theorem safeguardDisabled (principle : CoreCommitment) (selected : Candidate) :

The disabled safeguard fails for every principle and selected design, without a scope premise.

L121    safeguardExperiment principle false selected = false := by

State failure as exact equality of the computed experiment to false.

L122  cases principle <;> simp only [safeguardExperiment, Bool.false_eq_true, ↓reduceIte] <;> decide

Split principles, reduce the disabled branches and decide all five finite results.

L124theorem governanceValueProcedure (principle : CoreCommitment) :

For each principle, verify the actual governance value procedure.

L125    ValueProcedure (governancePosition principle) := by

The target is ValueProcedure for that same governancePosition.

L126  refine ⟨by simp [governancePosition], ?_, ?_, ?_⟩

Construct nonempty reasons and leave compatibility, objective/constraints and response obligations.

L127  · refine ⟨.evolvable, (modelsSingleton _ _).2 (by change 3 ≤ 3; decide),

Choose evolvable as a starting-theory witness, proving its singleton scope membership.

L128      (by change 3 ≤ 3; decide), rfl, ?_⟩

Prove its application limit and selection identity; leave its reason validity.

L129    intro reason member

Introduce any reason belonging to the position's reason list.

L130    cases List.mem_singleton.mp member

Singleton membership identifies it with the actual relevance reason.

L131    exact adoptionReasonRelevant principle .evolvable (by change 3 ≤ 3; decide)

Apply the proved relevance theorem at evolvable's complexity bound 3 ≤ 3.

L132  · intro selected _ scope _

For an arbitrary design under the procedure premises, retain its scope proof.

L133    exact ⟨safeguardEnabled principle selected scope, scope⟩

Supply enabled experiment success and the same scope as objective and constraint satisfaction.

L134  · intro selected _ _

Introduce an arbitrary criticism case under the response premises.

L135    exact ⟨criticismFor principle, rfl, by cases principle <;> decide⟩

Provide the fixed criticism response, its exact stored identity and nonemptiness by finite case analysis.

L137theorem governanceGrounded (principle : CoreCommitment) :

governanceGrounded gives grounds for the value commitment of every represented principle.

L138    valueSpecification (governancePosition principle) :=

The conclusion is valueSpecification for the exact governance position.

L139  grounds012Singleton _ (governanceValueProcedure principle)

Wrap its verified ValueProcedure in the singleton adopted Core 0.1.2 grounds construction.

L141/- Factual relevance, rationale experiments and value adoption are separate.

Comment separates factual relevance, rationale experiments and value adoption.

L142Swapping a reason or altering the input makes the finite rationale fail. -/

Comment introduces failure cases from swapped reasons or altered inputs.

L143theorem governanceRationaleLimits :

governanceRationaleLimits exhibits actual failures and distinguishes support from adoption.

L144    ¬ ReasonRelevant .consistency (reasonFor .generation) .evolvable ∧

A generation reason is irrelevant to consistency because the constructors mismatch.

L145    ¬ ReasonRelevant .reflexivity (.ownMethodCounterexample 21 10) .evolvable ∧

A claimed self-counterexample at size 10 fails because the old forecast agrees there.

L146    ¬ ReasonRelevant .generation (.plannedChange 9 .addition) .evolvable ∧

An unsupported release-9 addition plan fails the generation reason requirements.

L147    ¬ valueScope .maximal ∧

maximal lies outside the complexity-at-most-3 value scope.

L148    (∀ principle, safeguardExperiment principle false .evolvable = false) ∧

Every disabled safeguard experiment fails at evolvable.

L149    (∀ principle, (governancePosition principle).commitment .presentSimple) := by

Nevertheless every governance commitment is adopted at presentSimple too.

L150  refine ⟨by change ¬ False; decide, by decide, by decide, by change ¬ (30 ≤ 3); decide,

Compute the three irrelevant-reason cases and maximal's 30 > 3 scope failure.

L151    fun principle => safeguardDisabled principle .evolvable, fun _ => rfl⟩

Use safeguardDisabled for every principle, and reflexive adoption identity for the final universal claim.

L153/- This additional value priority is a real selection between the same designs.

Comment frames the additional value priority as a genuine selection between the same designs.

L154Both scopes retain all necessary domain conditions and no cost exception.

Comment points to the common context's necessary conditions and absence of cost exception; the limits field below explicitly tests continuation and credibility.

L155The present-simple stance values less abstraction now without claiming that it

Comment says the simple position values lower present abstraction and begins its capability qualification.

L156has the better successor-maintainer capability. The other stance values that capability. -/

Comment denies superior successor capability for the simple stance and assigns that objective to the other stance.

L157def selectionObjective (adopted : Candidate) (outcome : Nat × Nat) : Prop :=

selectionObjective maps an adopted design and complexity/work pair to its chosen objective proposition.

L158  match adopted with

The objective changes with the explicitly adopted candidate.

L159  | .presentSimple => outcome.1 ≤ 1

presentSimple values present abstraction complexity at most 1.

L160  | .evolvable => outcome.2 ≤ 6

evolvable values design-revision work at most 6.

L161  | .maximal => outcome.1 ≤ 1

The maximal branch also uses complexity at most 1; no successful procedure for maximal is proved below.

L163def selectionPosition (adopted : Candidate) : ValuePosition Candidate where

Build a separate selection ValuePosition parameterized by the adopted candidate.

L164  Position := Candidate

Its alternative positions are the actual Candidate designs.

L165  Outcome := Nat × Nat

Outcomes are natural-number pairs of complexity and revision work.

L166  adopted := adopted

Store the supplied adopted candidate directly.

L167  selected := id

A world's selected position is itself, via the identity function.

L168  outcome _ candidate := (abstractionComplexity candidate, changeWork candidate .designRevision)

Measure the chosen position's complexity and actual designRevision work.

L169  objective := selectionObjective adopted

Use the objective indexed by the adopted design.

L170  constraints _ candidate := abstractionComplexity candidate ≤ currentContinuing.limits.capacity .understanding

Constrain the position's complexity by the actual understanding capacity.

L171  starting := singleton (fun candidate => candidate = adopted)

The starting theory requires the world to equal the adopted design.

L172  reasons := [fun _ candidate =>

There is one reason function; it ignores the world argument and examines the position.

L173    abstractionComplexity candidate = (if adopted = .presentSimple then 1 else 3) ∧

Require complexity 1 for presentSimple adoption, otherwise complexity 3.

L174    changeWork candidate .designRevision = (if adopted = .presentSimple then 17 else 6)]

Require revision work 17 for presentSimple adoption, otherwise 6.

L175  limits _ := Continuing currentContinuing.activity ∧

The procedure's limits require the current activity to continue.

L176    credible currentContinuing.evidence .designRevision

They also require designRevision to be credible in the actual evidence.

L177  relevantCriticism _ := True

Every candidate is treated as relevant criticism.

L178  response _ := some (if adopted = .presentSimple then

Every criticism receives a response selected by whether presentSimple was adopted.

L179    "The successor lacks the private-layout path; this choice does not claim evolution priority and must be reconsidered if that value is adopted."

The simple response admits the successor's missing private-layout path and denies claiming evolution priority.

L180    else "The six-step design-revision path does not establish every change is cheap or every forecast is correct.")

The evolvable response limits the six-step result and denies general cheap-change or forecast correctness.

L182theorem selectionValueProcedure (adopted : Candidate)

Verify the selection value procedure for an adopted candidate.

L183    (ordinary : adopted = .presentSimple ∨ adopted = .evolvable) :

Assume adoption is one of the two ordinary designs.

L184    ValueProcedure (selectionPosition adopted) := by

The conclusion is the actual ValueProcedure for that adoption.

L185  rcases ordinary with rfl | rfl

Split and substitute presentSimple and evolvable adoptions.

L186  · refine ⟨by simp [selectionPosition], ?_, ?_, ?_⟩

For presentSimple, prove nonempty reasons and leave the three substantive procedure obligations.

L187    · refine ⟨.presentSimple, (modelsSingleton _ _).2 rfl, ?_, rfl, ?_⟩

Choose presentSimple itself as compatible witness and reduce its selection identity reflexively.

L188      · change Continuing currentContinuing.activity ∧ credible currentContinuing.evidence .designRevision

Expose the witness limit as actual continuation and credible designRevision.

L189        decide

Compute those fixed-context facts.

L190      · intro reason member

Introduce a reason from the singleton simple-position list.

L191        cases List.mem_singleton.mp member

Replace that reason by its unique member.

L192        decide

Compute simple design complexity 1 and revision work 17.

L193    · intro selected _ _ allReasons

Introduce arbitrary procedure premises, retaining allReasons for simple adoption.

L194      have actual := allReasons _ (List.mem_singleton.mpr rfl)

Extract the actual singleton reason from allReasons.

L195      change abstractionComplexity .presentSimple = 1 ∧ changeWork .presentSimple .designRevision = 17 at actual

Expose that reason as the concrete equalities complexity 1 and work 17 at adopted presentSimple.

L196      change abstractionComplexity .presentSimple ≤ 1 ∧

Expose the simple objective as complexity at most 1.

L197        abstractionComplexity .presentSimple ≤ currentContinuing.limits.capacity .understanding

The second conjunct is the same design's understanding-capacity constraint.

L198      exact ⟨by rw [actual.1]; exact Nat.le_refl _, by rw [actual.1]; decide⟩

Rewrite with the actual complexity equality, using reflexive ≤ for the objective and computation for capacity.

L199    · intro selected _ _

For arbitrary relevant criticism, enter the simple response obligation.

L200      refine ⟨_, rfl, ?_⟩

Choose the stored response and its reflexive equality; leave nonemptiness.

L201      simp

Simplify the fixed response to prove it is nonempty.

L202  · refine ⟨by simp [selectionPosition], ?_, ?_, ?_⟩

For evolvable, prove nonempty reasons and leave the same three procedure obligations.

L203    · refine ⟨.evolvable, (modelsSingleton _ _).2 rfl, ?_, rfl, ?_⟩

Choose evolvable itself as compatible witness with reflexive selection identity.

L204      · change Continuing currentContinuing.activity ∧ credible currentContinuing.evidence .designRevision

Expose the evolvable witness's continuation and credible-revision limits.

L205        decide

Compute those limits in currentContinuing.

L206      · intro reason member

Introduce a reason from evolvable's singleton reason list.

L207        cases List.mem_singleton.mp member

Identify it with the unique actual reason.

L208        decide

Compute evolvable complexity 3 and revision work 6.

L209    · intro selected _ _ allReasons

Introduce procedure premises for evolvable, retaining allReasons.

L210      have actual := allReasons _ (List.mem_singleton.mpr rfl)

Extract the unique substantive reason from that premise.

L211      change abstractionComplexity .evolvable = 3 ∧ changeWork .evolvable .designRevision = 6 at actual

Expose complexity 3 and designRevision work 6 for the adopted evolvable position.

L212      change changeWork .evolvable .designRevision ≤ 6 ∧

Expose the evolvable objective as work at most 6.

L213        abstractionComplexity .evolvable ≤ currentContinuing.limits.capacity .understanding

Retain the actual understanding-capacity constraint on the same design.

L214      exact ⟨by rw [actual.2]; exact Nat.le_refl _, by rw [actual.1]; decide⟩

Use work equality for the objective and complexity equality for the capacity check.

L215    · intro selected _ _

For any relevant criticism, enter the evolvable response obligation.

L216      refine ⟨_, rfl, ?_⟩

Choose the stored evolvable response, leaving its nonemptiness.

L217      simp

Simplify the response string to prove nonemptiness.

L219theorem selectionGrounded (adopted : Candidate)

selectionGrounded packages value grounds for the adopted selection.

L220    (ordinary : adopted = .presentSimple ∨ adopted = .evolvable) :

The two-ordinary-design assumption remains explicit.

L221    valueSpecification (selectionPosition adopted) :=

The conclusion concerns exactly selectionPosition adopted.

L222  grounds012Singleton _ (selectionValueProcedure adopted ordinary)

Use the proved selection procedure as the discharged singleton value facet.

L224end CoreReader.Engineering

Close namespace CoreReader.Engineering; no further mathematical claim is asserted.