.

diff --git a/document/TM-2026.html b/document/TM-2026.html
index ab24c5b..ad7f455 100644 (file)
--- a/document/TM-2026.html
+++ b/document/TM-2026.html
@@ -1257,41 +1257,48 @@
         This follows from the fact that the extension function is performing the exact operations that were performed when we generated the difference table. The extension function is merely formalizing the rules used for generating the table. As a consequence, the result tape after the <em>N</em>th call is identical to row <em>N</em> of the table.
       </p>
 
-      <h3>Lemma: Evaluating call <RT·math>\omega</RT·math> (the <RT·math>\omega</RT·math>th call) requires an initial tape  initialized with components 0 through  <RT·math>\omega</RT·math> of row 0 of the finite difference table.</h3>
+
+<h3>Lemma: Evaluating call <RT·math>\omega</RT·math> requires an initial tape populated with components 0 through <RT·math>\omega</RT·math> of row 0</h3>
 
       <p>
-        Define the <RT·term>extent</RT·term> refer to the maximum index for accessing a component of a vector, the extent is often denoted as <RT·math>\omega</RT·math>. Performing extensions to calculate the function value at call <RT·math>\omega</RT·math> will make use of the initial tape up to index <RT·math>\omega</RT·math>, or as many nonzero values as are available up to that extent.
+        Let the <RT·term>extent</RT·term> refer to the maximum index for accessing a component of a vector; the extent is often denoted as <RT·math>\omega</RT·math>. Performing extensions to calculate the function value at call <RT·math>\omega</RT·math> will make use of the initial tape up to index <RT·math>\omega</RT·math>, or as many nonzero values as are available up to that extent.
       </p>
 
       <p>
-        This can be proven by induction on the step index, <RT·math>k</RT·math>.
+        To make this precise, let us define the <RT·term>difference vector</RT·term> at call <RT·math>k</RT·math> as <RT·math>D_k</RT·math>. The components of this vector are <RT·math>D_{k, 0}, D_{k, 1}, \ldots, D_{k, m}</RT·math>, where <RT·math>m</RT·math> is the maximum available difference. The first component, <RT·math>D_{k, 0}</RT·math>, is the function value itself. The component <RT·math>D_{k, 1}</RT·math> is the first difference, and so on.
+      </p>
+      
+      <p>
+        The extension operation follows a simple recurrence relation for any component <RT·math>j</RT·math>: <RT·math>D_{k+1, j} = D_{k, j} + D_{k, j+1}</RT·math>.
       </p>
 
       <p>
-        <strong>Base Case (k=0):</strong> To generate the value at index 0, <RT·math>f(t_0)</RT·math>, the machine performs zero extensions. It requires the initial tape to have an extent of at least 0, accessing only the value at index 0, which is the function value itself.
+        We can now prove by induction on the call index <RT·math>k</RT·math> that computing <RT·math>D_{k, 0}</RT·math> requires exactly the components <RT·math>D_{0, 0}</RT·math> through <RT·math>D_{0, k}</RT·math> from the initial tape <RT·math>D_0</RT·math>.
       </p>
 
       <p>
-        <strong>Inductive Hypothesis:</strong> Assume that generating the value at step index <RT·math>k</RT·math> requires the initial tape to have an extent of <RT·math>k</RT·math>, consuming indices 0 through <RT·math>k</RT·math>: <RT·math>f(t_0), \Delta^1(t_0), \ldots, \Delta^k(t_0)</RT·math>.
+        <strong>Base Case (k=0):</strong> To generate the value at call 0, <RT·math>D_{0, 0}</RT·math>, the machine performs zero extensions. It accesses only the value at index 0 of the initial tape. The required extent is 0.
       </p>
 
       <p>
-        <strong>Inductive Step:</strong> Consider the requirement for the value at step index <RT·math>k+1</RT·math>. By the definition of the forward difference, <RT·math>f(t_{k+1}) = f(t_k) + \Delta^1(t_k)</RT·math>. 
+        <strong>Inductive Hypothesis:</strong> Assume that generating the value at call <RT·math>k</RT·math>, which is <RT·math>D_{k, 0}</RT·math>, requires the initial tape components <RT·math>D_{0, 0}</RT·math> through <RT·math>D_{0, k}</RT·math>.
+      </p>
+
+      <p>
+        <strong>Inductive Step:</strong> Consider the requirement for the value at call <RT·math>k+1</RT·math>, which is <RT·math>D_{k+1, 0}</RT·math>. By the extension rule, <RT·math>D_{k+1, 0} = D_{k, 0} + D_{k, 1}</RT·math>.
       </p>
       <ul>
-        <li>By the inductive hypothesis, computing <RT·math>f(t_k)</RT·math> consumes the initial sequence up to extent <RT·math>k</RT·math>, covering indices 0 through <RT·math>k</RT·math>.</li>
-        <li>The term <RT·math>\Delta^1(t_k)</RT·math> is the value at index <RT·math>k</RT·math> of the first difference sequence. Applying the same inductive logic, computing it consumes its initial sequence up to extent <RT·math>k</RT·math>. Because the initial sequence for the first difference begins at index 1 of the main tape, it requires indices 1 through <RT·math>k+1</RT·math> from row 0.</li>
+        <li>By the inductive hypothesis, computing <RT·math>D_{k, 0}</RT·math> depends on the initial tape components <RT·math>D_{0, 0}</RT·math> through <RT·math>D_{0, k}</RT·math>.</li>
+        <li>The term <RT·math>D_{k, 1}</RT·math> represents the result of applying <RT·math>k</RT·math> extensions starting from the initial first difference, <RT·math>D_{0, 1}</RT·math>. Applying the exact same inductive reasoning to this shifted starting position, computing <RT·math>D_{k, 1}</RT·math> requires <RT·math>k+1</RT·math> components starting from index 1. Therefore, it depends on the components <RT·math>D_{0, 1}</RT·math> through <RT·math>D_{0, k+1}</RT·math> of the initial tape.</li>
       </ul>
       <p>
-        The union of the dependencies for <RT·math>f(t_k)</RT·math> and <RT·math>\Delta^1(t_k)</RT·math> spans from index 0 to index <RT·math>k+1</RT·math>. Thus, generating the value at step index <RT·math>k+1</RT·math> requires the initial tape to have an extent of exactly <RT·math>k+1</RT·math>. The lemma holds.
+        The union of the dependencies for <RT·math>D_{k, 0}</RT·math> and <RT·math>D_{k, 1}</RT·math> spans from index 0 to index <RT·math>k+1</RT·math>. Thus, generating the value at call <RT·math>k+1</RT·math> requires the initial tape to have an extent of exactly <RT·math>k+1</RT·math>. The lemma holds.
       </p>
 
       <p>
-        Consequently, on a finite tape with no constant difference, each extension reduces the extent of the logical state by one. If a programmer intends to call the extension function to reach step index 4, the initial tape must have an extent of 4, meaning it holds 5 values. The first result tape will have an extent of 3, the second an extent of 2, the third an extent of 1, and the final call will leave an extent of 0: the requested answer.
+        This proof applies regardless of whether the finite difference table is infinitely deep or truncated. If a person evaluates a tenth degree polynomial but only programs the machine to perform two calls, the initial tape only needs an extent of 2, utilizing components 0, 1, and 2. Each extension consumes one cell of state. If a programmer intends to execute the extension function to reach call <RT·math>\omega</RT·math>, the initial tape must have an extent of <RT·math>\omega</RT·math>, meaning it holds <RT·math>\omega + 1</RT·math> values.
       </p>
 
-
-
       <h3>Lemma, a polynomial function degree N will always be defined with a N + 1 column first row </h3>
 
       <h3>A N+1 column first row means the table came from an N degree polynomial</h3>