ifc-0061

4.2 The Lie algebroid of creative moves

A Lie algebroid consists of a vector bundle

\[ \pi :A\longrightarrow M, \]

a Lie bracket \([\cdot ,\cdot ]_A\) on sections, and an anchor

\[ \rho :A\longrightarrow TM \]

satisfying, for sections \(s,t\) and \(f\in C^\infty (M)\),

\[ [s,ft]_A=f[s,t]_A+\rho (s)(f)t, \qquad \rho ([s,t]_A)=[\rho (s),\rho (t)], \]

the Leibniz rule and anchor–bracket compatibility [ Mackenzie , 2005 ] . At a theory state \(x\in M\), the fiber \(A_x\) contains locally available, typed skill directions. For a compiled section \(s_m\), execution produces the infinitesimal theory motion

\[ \dot x=\rho (s_m(x)). \]

When this vector field integrates over an interval, it produces a finite rollout \(x\mapsto \Phi _m^t(x)\). The rollout may edit a conjecture set, add a candidate interface, select an experiment, compare two mechanisms, or update a status-bearing extension dossier.

The three pieces have different semantics:

Base \(M\).

The maintained semantic states of the current theory.

Fiber \(A_x\).

Skills available locally at state \(x\), including their type, permissions, and provenance requirements.

Anchor \(\rho \).

The observable change in the theory state induced by executing a skill direction.

The vector-space structure in each fiber is a modeling commitment, not a property of skill names. It is justified only when local coefficients and linear combinations have an operational semantics—for example as mixtures, rates, or a declared continuous relaxation. Otherwise the Lie algebroid is a local surrogate for the compiled effects, and the compiler must record which discrete executions realize the sections being compared.

This is richer than placing independent coordinates on a prompt. Availability can vary with the state: a proof skill may become legal only after the necessary definitions exist; a simulator intervention may be available only where its mechanism is exposed; and a proposed analogy may be inadmissible until its source and target types have been registered.

The two-level optimization loop. The object-level loop executes an anchored skill on a theory state. The meta-level loop uses probe and validation records to revise the typed Markdown controller; locked admission remains outside this revision loop.
Figure 4.1 The two-level optimization loop. The object-level loop executes an anchored skill on a theory state. The meta-level loop uses probe and validation records to revise the typed Markdown controller; locked admission remains outside this revision loop.