definition theorem design

This note is Lenticulum’s own contribution, not the paper’s. AutoBayes has one -valued energy. We keep two, and adapt the chain rule accordingly. Requested design constraint; here is the construction and its proof obligations.

Sources: original to this vault (design and analysis; no single paper).

Theory (CT-ML wiki): Lax Functor · Bayesian Inversion · Statistical Game · Bayesian Lens · Variational Free Energy · Lens

1. What the paper does, and what it costs

Definition 20 types the energy as

and Definition 22 composes it by addition:

That composition law is precisely the statement that is a commutative monoid and is monoid-valued. Fine — but addition is a lossy projection. The moment you add, you can no longer say:

  • which factor contributed how much (per-factor loss attribution);
  • in which coordinates a factor is wrong (the residual direction, not just its size);
  • what the Jacobian of the residual is — and therefore no Gauss–Newton step, no Fisher metric, no implicit function theorem.

The last one is fatal for us, because Definition 27 explicitly says the default semantics is gradient descent with respect to the Fisher information metric, and because implicit inference is root-finding on a vector residual. Both need the vector.

2. Energy spaces

Definition (energy space). An energy space is a pair of a real topological vector space in which barycentres of the relevant measures exist, together with a closed convex cone with . induces the partial order . Energies take values in .

The direct sum is , with unit .

is the terminal-ish example. with (no order) or (componentwise) are the ones we use. The cone exists so that “energy is non-negative” still means something and so that monotonicity of scalarisations is expressible.

Definition (scalarisation). A scalarisation of is a map with , , and monotone for . It is linear if (the dual cone), and convex otherwise.

Two scalarisations do all the work:

reading
, anyprecision / temperature weighting; -VAE; the ‘s of ImplicitREDDiff
least squares on a residual; a precision matrix

3. The multivariate statistical game

Definition (multivariate statistical game). A multivariate statistical game over an energy space consists of

  • a Inversions and Bayesian Lenses ,
  • a vector energy ,
  • a vector entropy ,
  • a scalarisation ,

with vector loss and scalar loss .

Note the entropy is promoted to as well. It must be: otherwise is a type error. In practice is usually for a fixed — the entropy is scalar but has to be told which coordinate it regularises. That is not busywork: it is what lets you regularise one block of a factor and not another.

Recovering the paper: take , , .

4. The adapted chain rule

Definition (composition). For over and over , the composite is over , with

The addition of Definition 22 has become a direct sum. That is the entire change. The entropy law is unchanged in shape — still averaged under the downstream inversion, still evaluated at the pushforward prior — it just lands in a summand instead of being added in.

Theorem (multivariate chain rule).

Proof. Expand, using linearity of and that the tuple’s components are independent:

which is the claim.

Compare Theorem 23: same recursion, with replaced by a pair. It is not a weaker theorem — it is the same theorem before the projection.

Graded by the graph

Iterating, a graph of factors has

The total energy of a factor graph is a vector indexed by its factors, and within each factor by that factor’s own residual coordinates. Per-factor loss attribution is not a feature bolted on for logging; it is what the composite loss is, before you collapse it.

Proposition. Let as above.

  1. If is linear, then : the scalar chain rule of Theorem 23 holds exactly, and scalarisation is a strict morphism of games.
  2. If is convex, then , with

Proof. by definition of and the theorem above, while Theorem 23 gives . Subtract; the terms cancel; linearity gives equality and Jensen gives the inequality.

The only place the two chain rules can disagree is versus — i.e. the expectation over the downstream inversion. Nowhere else. That is a tight and checkable statement.

The gap, computed

For on the Jensen gap is exactly a variance:

So the multivariate composite is the squared mean residual and the scalar composite is the mean squared residual; the difference is the posterior variance of the upstream factor’s loss. This is a genuine bias/variance decomposition of the composite objective, and the variance term is a first-class diagnostic: how much does the downstream posterior disagree with itself about what the upstream factor should be doing?

This mirrors Remark 26 exactly

AutoBayes measures the laxness of the tensor by mutual information. We measure the laxness of scalarisation by a variance. Both are “the amount of structure destroyed by a projection, quantified”. Report them; do not hide them.

6. The gradient, adapted

For a parameterized multivariate game the derivative of is not a gradient but a Jacobian

and the scalar gradient is obtained by pulling back along the scalarisation’s differential:

For this is the familiar .

Composite. By the multivariate chain rule, and keeping only the terms Definition 29 keeps:

  • — moves the sampling distribution;
  • — moves the pushforward prior.

Definition 29 is the block-diagonal part. The laxness of the gradient assignment is unchanged by going multivariate; it is orthogonal to the scalarisation question. Good — the two approximations do not interact.

Why the Jacobian is the point

Once you have rather than only , you get for free:

  1. Gauss–Newton / Levenberg–Marquardt. , positive semidefinite by construction, no Hessian needed. alone cannot produce it — scalarising early destroys the metric, irrecoverably.
  2. The Fisher metric of Definition 27. When is the vector of per-component log-density contributions, its Jacobian is the score and . The natural gradient of the Bayesian learning rule is therefore available compositionally, from data the multivariate energy already carries. This is the strongest single argument for the design.
  3. The implicit function theorem. For a residual factor split by polarity into , which needs the square Jacobian block of the vector residual. A scalar energy cannot even express the shape requirement .
  4. Post-hoc reweighting. can be changed without recomposing the graph: -annealing, precision scheduling, curriculum weights, Pareto fronts. With the scalar energy each is a different graph.

7. Interface consequences

energyspace(f)              # -> AbstractEnergySpace, the E_f of this factor
energy(f, x, ps, st)        # -> element of K_f          (the vector 𝐥)
entropy(f, π, y, ps, st)    # -> element of K_f          (the vector 𝐇)
scalarisation(f)            # -> AbstractScalarisation σ_f
scalarise(σ, e)             # -> Real
islinear(σ)                 # -> Bool: strict vs lax composition (Prop. §5)

islinear is not decoration: it is the trait that tells the composition machinery whether scalarise ∘ compose == compose ∘ scalarise may be assumed, and therefore whether the scalar loss can be accumulated eagerly (cheap) or must be deferred until the vector loss is assembled (correct). See energy for the implementation and its difficulties.

A scalarisation is not a loss functional

σ : E_c → ℝ takes an energy value. LeCun’s loss functionals take the energy function over the whole answer space, because shaping a surface requires knowing what it does away from the correct answer. Lenticulum has no slot for one, and the consequence — its free energy is LeCun’s “energy loss”, the collapsing one — is Energy-Based Learning §3.

Related: Factors are Parameterized Statistical Games, Composition of Statistical Games, Composition of Gradients, Implicit Learners, energy, Energy-Based Learning