Linear Algebra
Exercise LA-003
local source supported. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- the environment assigns a rational to every symbol name
- coefficients are symbolic expressions over the rationals
- evaluation is relative to a fixed environment
Question
A stencil coefficient is written in a small symbolic language whose expressions are built from rational constants, named symbols, and the operations addition, multiplication, and negation. Given an environment that assigns a rational number to each symbol name, the coefficient is turned into a concrete rational number by a single evaluation map. State how this map treats each of the five kinds of expression, and state precisely which algebraic structure the evaluation preserves (that is, which equalities relate the value of a compound expression to the values of its parts).
Hint: mathematical route
Evaluation interprets rational constants, assigned symbols, addition, multiplication and negation compositionally. It preserves these operations into Rat without identifying raw expression trees modulo ring laws.
- Rational constants evaluate to themselves, symbols to the fixed environment's values; rat(0) and rat(1) give rational zero and one.
- Evaluation commutes with add, mul and neg as rational operations. This interprets raw constructor syntax; it does not assert that the syntax carrier itself satisfies ring equations.
Reference solution
Fix an environment env:String->Rat and write ev for evalWith env. The five recursive clauses are ev(rat(q))=q, ev(symbol(s))=env(s), ev(add(a,b))=ev(a)+ev(b), ev(mul(a,b))=ev(a)*ev(b), and ev(neg(a))=-ev(a). In particular the constant expressions rat(0) and rat(1) evaluate to rational 0 and 1. Every rational q is attained by rat(q), so this fixed-environment interpretation is surjective.
These equations say exactly that evaluation preserves the specified expression constructors as rational operations: it is an interpretation, or homomorphism of the corresponding operation-signature term algebra. They do not make the raw inductive Coeff syntax a ring or a rational algebra under those constructors. For example, add(rat(0),rat(0)) and rat(0) are different syntax trees even though both evaluate to zero. Ring laws such as x+0=x hold for the evaluated rational values, not as literal equality of these trees. To speak of a ring homomorphism one would first need an appropriate semantic quotient or another separately defined ring of expressions satisfying the ring laws; the raw source definition supplies neither that quotient nor such a ring instance. A symbolic rewrite is justified when its evaluations agree under the environments in scope, not merely because an arbitrary syntactic identity has been asserted. The five displayed equations are the exact preserved structure requested here.
Assessment rubric
- States constant and symbol evaluation exactly: ev(rat(q))=q and ev(symbol(s))=env(s), with env fixed. (1 weight)
- States all three recursive preservation identities for add, mul and neg, including the correct rational operations on evaluated subexpressions. (1 weight)
- Identifies precisely this constructor-preserving interpretation and 0/1 preservation. Distinguishes raw syntax from rational ring equality instead of claiming an unqualified ring/algebra homomorphism from constructor syntax. If surjectivity is claimed, justifies it using rat(q); no quotient construction is required. (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/Core.lean
declarations Coeff.evalWith (lines 175-181) and the evalWith_rat/evalWith_symbol/evalWith_add/evalWith_mul/evalWith_neg simp lemmas (lines 183-196)
Source SHA-256:c7e76d91c7fcfd844177f99c0399a3465a7d8360d3a522acb5d4c4e2f8277894· MIT (repository LICENSE)
Contract: f030c8cd7686f69b91de68108cc38a8bde1ebec892ae26f18513169c6ed5c285
Item digest: 9cf3d03948eddb4134368e2d31a81f2605928c2acee82aaae66e8f7bd5302a77
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 2. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "33122c5bd9eba24d73f1abe0de97a9f05e8a48e6e2bdcb636e8e2ac68388a5e9", "predecessor_key": "qcb-core-la-003", "repair_record": "shared/repairs/la-003-syntax-semantics-repair.json", "repair_record_digest": "1bf531ffaa22350d6c4a2d855728a260eca2b6d1c2ba88e7e94cc12a426c1c11", "review_record": "reports/textbook-v1/repairs/la-003-syntax-semantics-repair-review.json", "review_digest": "19a9943a100bea461bdfdc6eb862c9ef0652e2d045e1ecd4e8892c9e9f096ba0" }