Structured Preparation
Exercise SP-109
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
A degree-d polynomial is held as a coefficient row c(0),...,c(d) in the Bernstein basis, so that its value at t is sum_{r=0}^{d} c(r) B_{d,r}(t). One de Casteljau step with parameter s replaces the row c by the row with entries (1-s) c(i) + s c(i+1). Let L_u denote the operation that reads the left edge of the de Casteljau triangle built with parameter u (its i-th output is the result of i de Casteljau steps at u applied to c, read at position 0). Prove that evaluating the L_u-transformed coefficients at parameter t reproduces the original polynomial at the rescaled parameter u*t: sum_r (L_u c)(r) B_{d,r}(t) = sum_r c(r) B_{d,r}(u t).
Hint: mathematical route
Left de Casteljau subdivision at u reparametrises a Bernstein polynomial to u*t exactly, proved by a semiconjugacy of the linear step operator iterated d times.
- The de Casteljau step is a linear operator and the left restriction is its iterated left edge.
- The scaled step factors as T_{u t} = (1-t)Id + t T_u, verified entrywise.
- Hence L_u is a semiconjugacy T_{u t} -> T_t, which iterates to the d-th powers.
- Reading the triangle apex gives the Bernstein-sum reparametrisation to u*t.
Reference solution
Model the Bernstein state as an infinite coefficient row acted on by the linear 'de Casteljau step' operator T_s := (1-s) * Id + s * Shift, where Shift sends c(i) to c(i+1). The i-th left-edge output is (T_u^i c)(0), so L_u c = (i -> (T_u^i c)(0)). Step 1 (parameter composition): a single step at a scaled parameter factors as T_{u t} = (1-t) * Id + t * T_u. This is checked entrywise: ((1-t)Id + t T_u) c (i) = (1-t) c(i) + t[(1-u)c(i) + u c(i+1)] = (1 - u t) c(i) + u t c(i+1) = T_{u t} c (i). Step 2 (semiconjugacy): consequently L_u intertwines the step at scaled parameter with the step at t: L_u (T_{u t} c) = T_t (L_u c). This is the operator identity that says applying one scaled step then taking the left edge equals taking the left edge then applying one unscaled step. Step 3 (iterate the semiconjugacy d times): because L_u is a semiconjugacy from T_{u t} to T_t, it intertwines their d-th iterates: L_u (T_{u t}^d c) = T_t^d (L_u c). Reading position 0 of both sides gives (T_t^d (L_u c))(0) = (T_{u t}^d c)(0). Step 4 (translate to Bernstein sums): the left-edge-at-0 of a d-fold de Casteljau triangle equals the Bernstein sum, i.e. (T_s^d c)(0) = sum_{r=0}^{d} c(r) B_{d,r}(s). Applying this with the row L_u c and parameter t on the left, and with c and parameter u t on the right, yields exactly sum_r (L_u c)(r) B_{d,r}(t) = sum_r c(r) B_{d,r}(u t). This is the exact affine-restriction law: left de Casteljau subdivision reparametrises the curve to [0,u].
Assessment rubric
- Represents the de Casteljau step as the linear operator T_s=(1-s)Id+s Shift and identifies L_u as the left edge (T_u^i c)(0). (1 weight)
- Proves the parameter-composition identity T_{u t}=(1-t)Id + t T_u entrywise. (1 weight)
- Derives the semiconjugacy L_u T_{u t} = T_t L_u and iterates it d times, then reads position 0. (1 weight)
- Converts via (T_s^d c)(0)=sum_r c(r)B_{d,r}(s) to the Bernstein-sum identity, concluding the u*t reparametrisation. (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/HermiteBernstein.lean
lines 219-282: casteljauStep t = t . coefficientShift + (1-t) . 1; casteljauStep_mul_parameter : casteljauStep (u*t) = (1-t).1 + t.casteljauStep u; leftRestriction u c i = casteljau i c u 0; leftRestriction_step : leftRestriction u (casteljauStep (u*t) c) = casteljauStep t (leftRestriction u c); casteljau_leftRestriction via Function.Semiconj.iterate_right; leftRestriction_eval : sum_r leftRestriction u c r * basis d r t = sum_r c r * basis d r (u*t)
Source SHA-256:661618d9c10826491ee293c7c411ac2d55056426739f4bbfd3e7c410c05e4bff· MIT (repository LICENSE)
Contract: 54c870333f179ea1d4fcab903a21343998683ea0b1620bd8f4e60da8af992f31
Item digest: 3a814cf53b0df4df2ad559be465c6234a73ffca971366dae638536dbc21981d0
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 4. This is not measured graph distance or model difficulty.