Fixed lower graphs and common actual margins

Abstract

A finite lower graph determines one positive error margin for every canonical actual factor completion, before any factor is chosen.

Definition 1.1 (graphGapValues).

$$\forall n\in Nat,K\in Nat,d\in Real,\mathrm{graphGapValues}\left(n,K,d\right)=\mathrm{image}\left(\mathrm{filter}\left(\mathrm{univ}\left(\mathrm{MemoryVertex}\left(n\right)\right),(v:\mathrm{MemoryVertex}\left(n\right)\mapsto \mathrm{MemoryEdge}\left(lower,K,d,v,c,\mathrm{memoryShift}\left(v,c\right)\right)\wedge \mathrm{memoryRun}\left(v,c,K\right))\right),(v:\mathrm{MemoryVertex}\left(n\right)\mapsto \mathrm{subtract}\left(\mathrm{memoryValue}\left(v,0\right),\mathrm{multiply}\left(\mathrm{power}\left(chi,\mathrm{subtract}\left(K,1\right)\right),d\right)\right))\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.graphGapValues (✓ std3).

Source. Repository-derived.

Commentary.

MemoryVertex(n) is the original n-letter past, indexed from the most recent letter. graphGapValues includes every allowed high edge of the ambient lower graph, even if that edge is not retained on a bilateral path. Since an edge has target memoryShift(v,c), recording its source vertex records the entire high edge. Its gap is memoryValue(v,0)-chi^(K-1)*d. The edge’s strict guard makes each gap positive. These are real comparisons defining an exact finite mathematical object; no effective decision procedure for arbitrary real budgets is asserted.

Definition 1.2 (graphMargin).

$$\forall n\in Nat,K\in Nat,d\in Real,\mathrm{graphMargin}\left(n,K,d\right)=\mathrm{if}\left(\mathrm{Nonempty}\left(\mathrm{graphGapValues}\left(n,K,d\right)\right),\mathrm{finiteMinimum}\left(\mathrm{graphGapValues}\left(n,K,d\right)\right),0\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.graphMargin (✓ std3).

Source. Repository-derived.

Commentary.

When graphGapValues is nonempty, graphMargin is its attained finite minimum. finiteMinimum denotes Finset.min’ with the nonempty proof supplied by that branch. The zero in the other branch is a placeholder; it is never used as a positive graph margin.

Theorem 1.3 (graph gap minimum).

$$\forall n\in Nat,K\in Nat,d\in Real,\mathrm{Nonempty}\left(\mathrm{graphGapValues}\left(n,K,d\right)\right)\Rightarrow \left(\mathrm{lt}\left(0,\mathrm{graphMargin}\left(n,K,d\right)\right)\wedge \mathrm{IsLeast}\left(\mathrm{toSet}\left(\mathrm{graphGapValues}\left(n,K,d\right)\right),\mathrm{graphMargin}\left(n,K,d\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.graph_gap_minimum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The allowed high-edge set is finite, and every lower-edge gap is strictly positive. Its attained minimum is therefore positive and is exactly epsilon_graph. IsLeast includes membership in the gap set and comparison with every other member; an arbitrary smaller bound is not substituted for the minimum.

Theorem 1.4 (lower graph high gap).

$$\forall n\in Nat,K\in Nat,d\in Real,\forall omega\in Int\to CuLetter,i\in Int,\left(\mathrm{lt}\left(0,K\right)\wedge \left(\mathrm{le}\left(K,n\right)\wedge \left(\mathrm{member}\left(omega,\mathrm{MemoryLanguage}\left(lower,n,K,d\right)\right)\wedge \left(\forall k\in \mathrm{Fin}\left(K\right),\mathrm{apply}\left(omega,\mathrm{subtract}\left(i,\mathrm{toInt}\left(k\right)\right)\right)=c\right)\right)\right)\right)\Rightarrow \left(\mathrm{Nonempty}\left(\mathrm{graphGapValues}\left(n,K,d\right)\right)\wedge \mathrm{le}\left(\mathrm{graphMargin}\left(n,K,d\right),\mathrm{subtract}\left(\mathrm{pastState}\left(omega,i\right),\mathrm{multiply}\left(\mathrm{power}\left(chi,\mathrm{subtract}\left(K,1\right)\right),d\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.lower_graph_high_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

For n at least K and positive K, the unique actual memory path reconstructs the original past word. At a high letter its memoryRun is the original K-letter c-run, so its allowed lower edge contributes to graphGapValues. The zero-seed memory value is at most the bilateral state at that same position. Thus every original high guard is at least tau+epsilon_graph. In particular a graph with no allowed high edge has no high position in any of its bilateral paths.

Definition 1.5 (resetFloor).

$$\forall R\in Return,\mathrm{resetFloor}\left(R\right)=\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(\mathrm{power}\left(rho,m\left(R\right)\right),\mathrm{subtract}\left(\mathrm{hSide}\left(high\right),\mathrm{multiply}\left(chi,\mathrm{aSide}\left(high\right)\right)\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.resetFloor (✓ std3).

Source. Repository-derived.

Commentary.

R=(m(R),1) is the low reset, with paid length 20+6m(R). Its floor B is attained at the auxiliary input A_H. Every actual complete initial state exceeds A_H, and the merged leading u run can only increase the reset output.

Definition 1.6 (fixedGraphActualMargin).

$$\forall n\in Nat,K\in Nat,b\in Real,R\in Return,\mathrm{fixedGraphActualMargin}\left(n,K,b,R\right)=\mathrm{if}\left(\mathrm{Nonempty}\left(\mathrm{graphGapValues}\left(n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right),\mathrm{divide}\left(\min \left(\min \left(\mathrm{subtract}\left(b,\mathrm{actualAutomaticCost}\left(K\right)\right),\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{subtract}\left(\mathrm{resetFloor}\left(R\right),\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\right),\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),chi\right),\mathrm{graphMargin}\left(n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\right),2\right),\mathrm{divide}\left(\min \left(\mathrm{subtract}\left(b,\mathrm{actualAutomaticCost}\left(K\right)\right),\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{subtract}\left(\mathrm{resetFloor}\left(R\right),\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\right),2\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.fixedGraphActualMargin (✓ std3).

Source. Repository-derived.

Commentary.

Here d=(lam-b)/g^2/chi^K and tau=chi^(K-1)d. The three entries are b-C_auto, g^2chi^K*(B-d), and g^2chiepsilon_graph. Taking half their minimum leaves strict room to move every nearest target into its actual color-cell interior, independently of all five ownership flags. If no allowed high edge exists, the graph term is omitted, while the positive reset term is retained as a conservative bound.

Definition 1.7 (CanonicalFactorCompletion).

$$\forall R\in Return,w\in \mathrm{List}\left(CuLetter\right),xs\in \mathrm{List}\left(Return\right),\mathrm{CanonicalFactorCompletion}\left(R,w,xs\right)=\mathrm{if}\left(\mathrm{member}\left(c,w\right),\exists a\in Nat,first\in Return,rest\in \mathrm{List}\left(Return\right),\mathrm{if}\left(\mathrm{getLastOption}\left(w\right)=\mathrm{some}\left(c\right),\mathrm{append}\left(w,\mathrm{singleton}\left(u\right)\right),w\right)=\mathrm{append}\left(\mathrm{replicate}\left(a,u\right),\mathrm{executionWord}\left(\mathrm{cons}\left(first,rest\right)\right)\right)\wedge xs=\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(R\right),a\right),1\right),\mathrm{cons}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(first\right),1\right),r\left(first\right)\right),rest\right)\right),w=\mathrm{replicate}\left(\mathrm{length}\left(w\right),u\right)\wedge xs=\mathrm{singleton}\left(\mathrm{Return}\left(\mathrm{add}\left(m\left(R\right),\mathrm{length}\left(w\right)\right),1\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.CanonicalFactorCompletion (✓ std3).

Source. Repository-derived.

Commentary.

If w contains c, fill its last return with one terminal u exactly when it ends in c. Parse its leading u run and its positive first and rest returns. Merge the leading run into the reset; add one u immediately after the first visible c-run’s return, even if it is low. The construction does not move the extra u to the first high return. An all-u word, including the empty factor, merely extends the reset’s u run. Return(m,r) denotes the original positive-exponent constructor. The predicate uses literal runs and no supply or margin conclusion.

Theorem 1.8 (canonical factor completion unique).

$$\forall R\in Return,w\in \mathrm{List}\left(CuLetter\right),xs\in \mathrm{List}\left(Return\right),ys\in \mathrm{List}\left(Return\right),\left(\mathrm{CanonicalFactorCompletion}\left(R,w,xs\right)\wedge \mathrm{CanonicalFactorCompletion}\left(R,w,ys\right)\right)\Rightarrow xs=ys$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.canonical_factor_completion_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

The unique leading-run and complete-return decomposition determines the literal completion. Uniqueness is independent of errors, scalar state choices and actual supply.

Theorem 1.9 (fixed lower graph actual margin).

$$\forall n\in Nat,K\in Nat,b\in Real,\left(\mathrm{le}\left(2,K\right)\wedge \left(\mathrm{le}\left(K,n\right)\wedge \left(\mathrm{lt}\left(\mathrm{subtract}\left(lam,\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{hSide}\left(high\right)\right)\right),b\right)\wedge \mathrm{lt}\left(b,\mathrm{subtract}\left(lam,\mathrm{multiply}\left(\mathrm{multiply}\left(\mathrm{power}\left(g,2\right),\mathrm{power}\left(chi,K\right)\right),\mathrm{divide}\left(\mathrm{aSide}\left(high\right),\mathrm{subtract}\left(1,\mathrm{multiply}\left(rho,\mathrm{power}\left(chi,K\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\exists R\in Return,r\left(R\right)=1\wedge \left(\mathrm{lt}\left(\max \left(\max \left(\mathrm{xSide}\left(high\right),\mathrm{ySide}\left(high\right)\right),\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right),\mathrm{resetFloor}\left(R\right)\right)\wedge \left(\mathrm{lt}\left(0,\mathrm{fixedGraphActualMargin}\left(n,K,b,R\right)\right)\wedge \left(\left(\mathrm{Nonempty}\left(\mathrm{graphGapValues}\left(n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\Rightarrow \left(\mathrm{lt}\left(0,\mathrm{graphMargin}\left(n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\wedge \mathrm{IsLeast}\left(\mathrm{toSet}\left(\mathrm{graphGapValues}\left(n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right),\mathrm{graphMargin}\left(n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\right)\right)\wedge \left(\forall model\in Model,o\in Ownership,w\in \mathrm{List}\left(CuLetter\right),\left(\exists omega\in Int\to CuLetter,\mathrm{member}\left(omega,\mathrm{MemoryLanguage}\left(lower,n,K,\mathrm{divide}\left(\mathrm{divide}\left(\mathrm{subtract}\left(lam,b\right),\mathrm{power}\left(g,2\right)\right),\mathrm{power}\left(chi,K\right)\right)\right)\right)\wedge \mathrm{Occurs}\left(omega,w\right)\right)\Rightarrow \left(\exists xs\in \mathrm{List}\left(Return\right),\left(\mathrm{CanonicalFactorCompletion}\left(R,w,xs\right)\wedge \left(\mathrm{ActualPairSupply}\left(model,o,\mathrm{subtract}\left(b,\mathrm{fixedGraphActualMargin}\left(n,K,b,R\right)\right),strict,xs\right)\wedge \mathrm{listWeight}\left(xs\right)=\mathrm{add}\left(\mathrm{add}\left(\mathrm{wordWeight}\left(w\right),\mathrm{add}\left(20,\mathrm{multiply}\left(6,m\left(R\right)\right)\right)\right),\mathrm{if}\left(\mathrm{member}\left(c,w\right),\mathrm{if}\left(\mathrm{getLastOption}\left(w\right)=\mathrm{some}\left(c\right),12,6\right),0\right)\right)\right)\right)\wedge \left(\forall ys\in \mathrm{List}\left(Return\right),\left(\mathrm{CanonicalFactorCompletion}\left(R,w,ys\right)\wedge \left(\mathrm{ActualPairSupply}\left(model,o,\mathrm{subtract}\left(b,\mathrm{fixedGraphActualMargin}\left(n,K,b,R\right)\right),strict,ys\right)\wedge \mathrm{listWeight}\left(ys\right)=\mathrm{add}\left(\mathrm{add}\left(\mathrm{wordWeight}\left(w\right),\mathrm{add}\left(20,\mathrm{multiply}\left(6,m\left(R\right)\right)\right)\right),\mathrm{if}\left(\mathrm{member}\left(c,w\right),\mathrm{if}\left(\mathrm{getLastOption}\left(w\right)=\mathrm{some}\left(c\right),12,6\right),0\right)\right)\right)\right)\Rightarrow ys=xs\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.fixed_lower_graph_actual_margin (✓ std3). ∎

Source. Repository-derived.

Commentary.

Fix K at least two, b in the original transition interval, and n at least K. One finite low reset and one positive epsilon_actual are chosen before all factors, either actual model and every ownership assignment. Each graph factor has exactly its canonical completed list, the displayed weight overhead and strict actual errors below b-epsilon_actual. There is no bound on original or completed length, return exponent m, depth or total weight. The empty and all-u cases have overhead 20+6m(R); c-containing factors add six or twelve according to their original last letter.

The reset protects only the first visible return. If that return is high, its actual input exceeds B, so its active cost is at most b-g^2chi^K(B-d); if low, it passes by C_auto. The extra u then makes its completed output dominate the original auxiliary output. Later high returns inherit the graph guard, including the first high return after a low first return. The invariant along their live recurrence is min(B,d+epsilon_graph/chi^(K-1)); multiplying its gap by g^2*chi^K gives exactly the minimum of the reset and graph cost gains. It does not rely on a positive infimum of per-factor strict gaps. With no allowed high edge the auxiliary guard is vacuous, so the reset-only half minimum suffices.

ActualPairSupply uses the same completed execution list on both original literal sources. It reads every departure of the stem, paid anchor when present, and all repeated blocks. Beyond the history length the error is zero, and the full future is the zero-error readout of each original literal tail. The auxiliary bilateral sequence is used only for the occurrence and its quantitative guard. It is not an actual eventually-empty source. A fixed graph’s margin may shrink as n changes; this theorem does not supply a common margin over all memory graphs or identify a global decoder optimum.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.CanonicalFactorCompletion
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.canonical_factor_completion_unique
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.fixedGraphActualMargin
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.fixed_lower_graph_actual_margin
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.graphGapValues
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.graphMargin
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.graph_gap_minimum
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.lower_graph_high_gap
• Truth anchor: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/FixedGraphMargin.resetFloor
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/Completion
• Dependency: D5/S3/ConceptDynamics/Coding/FibonacciFactorCompletion/InteriorRoot