Budget and Efficiency Assembly

Abstract

Refinement information, innovation counts, and finite closure-spectrum memory budgets are assembled on the canonical finite carriers.

Theorem 1.1 (Refinement gain, innovation budget, and closure-spectrum telescope).

$$\begin{array}{r}\forall P,F,X,Q:\mathrm{Type},\\ C:\mathbb{N}\to \mathrm{Type},[\mathrm{Fintype}(P)][\mathrm{Fintype}(F)][\mathrm{Fintype}(X)],\\ fintypeC:\forall n:\mathbb{N},[\mathrm{Fintype}(C(n))],\\ p:\mathrm{Prod}(P,F)\to \mathbb{R},hp:(\forall z:\mathrm{Prod}(P,F),0\le p(z))\wedge \sum _{z}p(z)=1,\\ q:\forall n:\mathbb{N},P\to C(n),forget:\forall n:\mathbb{N},C(n+1)\to C(n),\\ hrefine:\forall n:\mathbb{N},q(n)=\mathrm{comp}(\mathrm{forget}(n),q(n+1)),update:X\to X,readout:X\to Q\Rightarrow \\ mass:P\to \mathbb{R}=\mathrm{marginal}(p),\\ h:\mathbb{N}\to \mathbb{R}=funn\mapsto \mathrm{conditionalEntropy}(\mathrm{completionLaw}(mass,q(n),q(n+1))),\\ g:\mathbb{N}\to \mathbb{R}=funn\mapsto \mathrm{refinementGain}(p,q(n+1),\mathrm{forget}(n)),\\ eta:\mathbb{N}\to \mathbb{R}=funn\mapsto \mathrm{if}(h(n)=0,0,g(n)/h(n)),\\ (\forall n:\mathbb{N},(0\le g(n)\wedge g(n)\le h(n)\wedge (0<h(n)\Rightarrow \mathrm{eta}(n)=g(n)/h(n))\wedge (h(n)=0\Rightarrow \mathrm{eta}(n)=0)))\wedge (\mathrm{Summable}(h)\wedge \sum _n^{\infty }h(n)\le H(mass)\wedge \forall epsilon:\mathbb{R},(0<epsilon\Rightarrow \mathrm{ncard}(\{n\in \mathbb{N}\mid epsilon\le h(n)\})\le H(mass)/epsilon))\wedge (\sum _{k\in \mathrm{range}(\mathrm{observationStabilityDepth}(update,readout))}\log (\mathrm{observationClassCount}(update,readout,k+1))-\log (\mathrm{observationClassCount}(update,readout,k))=\log (\mathrm{infiniteObservationClassCount}(update,readout))-\log (\mathrm{Nat}.card(\mathrm{Set}.range(readout)))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Entropy/Observation/BudgetEfficiencyAssembly.budget_efficiency_assembly (✓ std3). ∎

Source. Repository-derived.

Commentary.

The finite past/future law and deterministic fine-to-coarse readout use the canonical predictive-memory and refinement-gain definitions. The first conjunct is the imported exact decomposition and its nonnegativity.

A nonnegative summable innovation sequence with a total budget H obeys the canonical threshold-count bound. The final conjunct applies the finite observation quotient and complete-future quotient to the closure-spectrum log telescope; the endpoint is the realized readout image, not an arbitrary codomain complement.

No new probability law, quotient, or resolution object is declared. The finite/infinite quotient bridge is proved locally from the existing future relations and the pinned quotient-range equivalence.

References

• Truth anchor: D5/S3/Entropy/Observation/BudgetEfficiencyAssembly.budget_efficiency_assembly
• Dependency: D5/S3/ConceptDynamics/Completion/CompletionInformationCost
• Dependency: D5/S3/Entropy/EntropyNonneg
• Dependency: D5/S3/Entropy/Observation/ConditionalChoiceOutcomeChainRule
• Dependency: D5/S3/Entropy/Submodularity/RefinementInformationDecomposition
• Dependency: D5/S3/Observer/Prediction/StableDepthCardinalityBounds
• Dependency: D5/S3/Observer/Separation/FiniteHistoryStability
• Dependency: D5/S3/Observer/Tomography/InnovationCountBound
• Dependency: D5/S3/ObserverMemory/Prediction/ConditionalEntropyStability