The §5.3 two-tile non-vacuity witness data

{"text": "{\n "readback": "witnessH. This is a constant definition of a function on the one-dimensional Euclidean space $\\\\mathbb{R}^1$ (formally EuclideanSpace \u211d (Fin 1), the space of real 1-tuples with the Euclidean norm): it maps each vector $w \\\\in \\\\mathbb{R}^1$ to\n\n

$$h(w) = 6 \\\\cdot w,$$

\n\ni.e. scalar multiplication of $w$ by the real number $6$. Literally, the declaration fixes the name witnessH to the map $w \\\\mapsto 6w$ from $\\\\mathbb{R}^1$ to $\\\\mathbb{R}^1$; nothing more is asserted (it is a def, not a theorem, and the definition is marked noncomputable). As a map on the single coordinate, if $w = (w_0)$ then $h(w) = (6w_0)$.\n\n**witnessY.** A constant definition of a function assigning to each index $i \\\\in \\\\{0, 1\\\\}$ (the type Fin 2, a two-element index type) a vector in $\\\\mathbb{R}^1$:\n\n

y_i = \\\\begin{cases} (1) & i = 0, \\\\\\\\ (4) & i = 1. \\\\end{cases}

\n\nConcretely $y_0 = 1$ and $y_1 = 4$ in the single coordinate. The construction WithLp.toLp 2 (fun _ => \u2026) builds the Euclidean-space element whose every coordinate (there is exactly one) is the stated real number. Both branches of the if are total, so every index of Fin 2 receives one of these two values with no undefined case.\n\n**witnessF.** A constant definition of a family, indexed by $i \\\\in \\\\{0,1\\\\}$, of real-valued functions on the product space $\\\\mathbb{R}^1 \\\\times \\\\mathbb{R}^1$ (a pair $(w, v)$ with $w$ the parameter-slot vector and $v$ the shared-state-slot vector):\n\n

$$f_i(w, v) = \\\\tfrac{1}{2}\\\\, \\\\lVert v - y_i \\\\rVert^2,$$

\n\nwhere $y_i$ is the target vector defined above ($y_0 = (1)$, $y_1 = (4)$), the norm is the Euclidean norm on $\\\\mathbb{R}^1$ (so $\\\\lVert v - y_i \\\\rVert = |v_0 - (y_i)_0|$), and $\\\\tfrac12$ is the real number $1/2$. Note that the first component $w$ of the argument pair is never read: $f_i$ depends only on the second component $v$.\n\n**witnessAlpha.** A constant definition of a real-valued function on the index set $\\\\{0, 1\\\\}$ giving the reduction weights\n\n

\\\\alpha_i = \\\\begin{cases} \\\\tfrac14 & i = 0, \\\\\\\\ \\\\tfrac34 & i = 1. \\\\end{cases}

\n\nSo $\\\\alpha_0 = 1/4$ and $\\\\alpha_1 = 3/4$ (the latter written in Lean as the division $3/4$, which is the real number $0.75$; both are positive and they sum to $1$, though the declaration itself asserts no such property). The if i = 0 then \u2026 else \u2026 is total over Fin 2, covering both indices.\n\n**witnessW\u2080.** A constant definition fixing a single vector in $\\\\mathbb{R}^1$, the pre-update parameter\n\n

$$w_0 = (2),$$

\n\ni.e. the Euclidean-space element whose (unique) coordinate is the real number $2$, again built by WithLp.toLp 2. No property is asserted; this is purely a named constant.\n\n**witnessVal.** A constant definition of a real-valued function on $\\\\{0,1\\\\}$ giving, for each occurrence $i$, the value of the loss $f_i$ evaluated at the specific point where the parameter slot is $w_0 = (2)$ and the shared-state slot is $h(w_0)$:\n\n

$$\\\\mathrm{val}_i = \\\\tfrac12 \\\\,\\\\lVert h(w_0) - y_i \\\\rVert^2.$$

\n\nConcretely, since $h(w) = 6w$ and $w_0 = (2)$, we have $h(w_0) = (12)$, so\n\n

$$\\\\mathrm{val}_0 = \\\\tfrac12 |12 - 1|^2 = \\\\tfrac{121}{2} = 60.5, \\\\qquad \\\\mathrm{val}_1 = \\\\tfrac12 |12 - 4|^2 = \\\\tfrac{64}{2} = 32.$$

\n\nThe declaration only defines these two numbers; it does not assert any relation to the derivative-certificate field val of FrameDeriv.\n\n**witnessDirect.** A constant definition of a function on $\\\\{0,1\\\\}$ with values in $\\\\mathbb{R}^1$ that is identically zero:\n\n

$$\\\\mathrm{direct}_i = (0) \\\\quad \\\\text{for both } i = 0 \\\\text{ and } i = 1.$$

\n\nThe definition ignores its index argument entirely. (Consistently with witnessF not reading its first argument, this is the zero vector; the declaration itself makes no such claim \u2014 it merely fixes the constant zero function.)\n\n**witnessShared.** A constant definition of a function on $\\\\{0,1\\\\}$ with values in $\\\\mathbb{R}^1$, assigning to each occurrence the vector difference\n\n

$$\\\\mathrm{shared}_i = h(w_0) - y_i.$$

\n\nConcretely, using $h(w_0) = (12)$, $y_0 = (1)$, $y_1 = (4)$:\n\n

$$\\\\mathrm{shared}_0 = (12 - 1) = (11), \\\\qquad \\\\mathrm{shared}_1 = (12 - 4) = (8).$$

\n\nThis is the vector $h(w_0) - y_i$ in the one-coordinate Euclidean space; the declaration defines the two vectors and asserts nothing further (in particular, no gradient or derivative property is claimed by this definition)."\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-VathekWitness.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "readback": "witnessH. This is a constant definition of a function on the one-dimensional Euclidean space $\\\\mathbb{R}^1$ (formally EuclideanSpace \u211d (Fin 1), the space of real 1-tuples with the Euclidean norm): it maps each vector $w \\\\in \\\\mathbb{R}^1$ to\n\n

$$h(w) = 6 \\\\cdot w,$$

\n\ni.e. scalar multiplication of $w$ by the real number $6$. Literally, the declaration fixes the name witnessH to the map $w \\\\mapsto 6w$ from $\\\\mathbb{R}^1$ to $\\\\mathbb{R}^1$; nothing more is asserted (it is a def, not a theorem, and the definition is marked noncomputable). As a map on the single coordinate, if $w = (w_0)$ then $h(w) = (6w_0)$.\n\n**witnessY.** A constant definition of a function assigning to each index $i \\\\in \\\\{0, 1\\\\}$ (the type Fin 2, a two-element index type) a vector in $\\\\mathbb{R}^1$:\n\n

y_i = \\\\begin{cases} (1) & i = 0, \\\\\\\\ (4) & i = 1. \\\\end{cases}

\n\nConcretely $y_0 = 1$ and $y_1 = 4$ in the single coordinate. The construction WithLp.toLp 2 (fun _ => \u2026) builds the Euclidean-space element whose every coordinate (there is exactly one) is the stated real number. Both branches of the if are total, so every index of Fin 2 receives one of these two values with no undefined case.\n\n**witnessF.** A constant definition of a family, indexed by $i \\\\in \\\\{0,1\\\\}$, of real-valued functions on the product space $\\\\mathbb{R}^1 \\\\times \\\\mathbb{R}^1$ (a pair $(w, v)$ with $w$ the parameter-slot vector and $v$ the shared-state-slot vector):\n\n

$$f_i(w, v) = \\\\tfrac{1}{2}\\\\, \\\\lVert v - y_i \\\\rVert^2,$$

\n\nwhere $y_i$ is the target vector defined above ($y_0 = (1)$, $y_1 = (4)$), the norm is the Euclidean norm on $\\\\mathbb{R}^1$ (so $\\\\lVert v - y_i \\\\rVert = |v_0 - (y_i)_0|$), and $\\\\tfrac12$ is the real number $1/2$. Note that the first component $w$ of the argument pair is never read: $f_i$ depends only on the second component $v$.\n\n**witnessAlpha.** A constant definition of a real-valued function on the index set $\\\\{0, 1\\\\}$ giving the reduction weights\n\n

\\\\alpha_i = \\\\begin{cases} \\\\tfrac14 & i = 0, \\\\\\\\ \\\\tfrac34 & i = 1. \\\\end{cases}

\n\nSo $\\\\alpha_0 = 1/4$ and $\\\\alpha_1 = 3/4$ (the latter written in Lean as the division $3/4$, which is the real number $0.75$; both are positive and they sum to $1$, though the declaration itself asserts no such property). The if i = 0 then \u2026 else \u2026 is total over Fin 2, covering both indices.\n\n**witnessW\u2080.** A constant definition fixing a single vector in $\\\\mathbb{R}^1$, the pre-update parameter\n\n

$$w_0 = (2),$$

\n\ni.e. the Euclidean-space element whose (unique) coordinate is the real number $2$, again built by WithLp.toLp 2. No property is asserted; this is purely a named constant.\n\n**witnessVal.** A constant definition of a real-valued function on $\\\\{0,1\\\\}$ giving, for each occurrence $i$, the value of the loss $f_i$ evaluated at the specific point where the parameter slot is $w_0 = (2)$ and the shared-state slot is $h(w_0)$:\n\n

$$\\\\mathrm{val}_i = \\\\tfrac12 \\\\,\\\\lVert h(w_0) - y_i \\\\rVert^2.$$

\n\nConcretely, since $h(w) = 6w$ and $w_0 = (2)$, we have $h(w_0) = (12)$, so\n\n

$$\\\\mathrm{val}_0 = \\\\tfrac12 |12 - 1|^2 = \\\\tfrac{121}{2} = 60.5, \\\\qquad \\\\mathrm{val}_1 = \\\\tfrac12 |12 - 4|^2 = \\\\tfrac{64}{2} = 32.$$

\n\nThe declaration only defines these two numbers; it does not assert any relation to the derivative-certificate field val of FrameDeriv.\n\n**witnessDirect.** A constant definition of a function on $\\\\{0,1\\\\}$ with values in $\\\\mathbb{R}^1$ that is identically zero:\n\n

$$\\\\mathrm{direct}_i = (0) \\\\quad \\\\text{for both } i = 0 \\\\text{ and } i = 1.$$

\n\nThe definition ignores its index argument entirely. (Consistently with witnessF not reading its first argument, this is the zero vector; the declaration itself makes no such claim \u2014 it merely fixes the constant zero function.)\n\n**witnessShared.** A constant definition of a function on $\\\\{0,1\\\\}$ with values in $\\\\mathbb{R}^1$, assigning to each occurrence the vector difference\n\n

$$\\\\mathrm{shared}_i = h(w_0) - y_i.$$

\n\nConcretely, using $h(w_0) = (12)$, $y_0 = (1)$, $y_1 = (4)$:\n\n

$$\\\\mathrm{shared}_0 = (12 - 1) = (11), \\\\qquad \\\\mathrm{shared}_1 = (12 - 4) = (8).$$

\n\nThis is the vector $h(w_0) - y_i$ in the one-coordinate Euclidean space; the declaration defines the two vectors and asserts nothing further (in particular, no gradient or derivative property is claimed by this definition)."\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-VathekWitness"}}}}