ifc-0055

3.10 Differential theory extensions

Let the current and proposed theories be presented by finite sketches \(\mathbb S\) and \(\mathbb S^+\), with a typed extension

\[ J:\mathbb S\longrightarrow \mathbb S^+. \]

Suppose their semantic worlds are described by

\[ F:\mathsf{Weil}_1^{\mathrm{tan}}\longrightarrow \operatorname {End}(\mathcal M) \]

and a proposed extension by

\[ F^+:\mathsf{Weil}_1^{\mathrm{tan}}\longrightarrow \operatorname {End}(\mathcal M^+). \]

The sketch extension induces or is supplied with an appropriate semantic transport \(\bar J:\mathcal M\to \mathcal M^+\). To compare the old and new local geometries, we also need coherent comparison maps

\[ \chi _A: \bar J\, F(A)\Longrightarrow F^+(A)\, \bar J, \qquad A\in \mathsf{Weil}_1^{\mathrm{tan}}. \]
Definition 3.9 Candidate differential theory extension

A candidate differential theory extension consists of a finite sketch map \(J:\mathbb S\to \mathbb S^+\), a semantic transport \(\bar J\), and a monoidally coherent family of comparison maps \(\chi _A\) relating the old and new Weil actions. It becomes an admitted differential theory extension only after the transport claim and the extension’s new consequences pass the registered independent tests of Chapter 2.

For each probe \(A\) and theory state \(X\), the comparison has the form

Commutative diagram illustrating 3.10 Differential theory extensions.

The square is equipped with the 2-cell

\[ \chi _{A,X}:\bar JF(A)X\longrightarrow F^+(A)\bar JX, \]

which measures whether “probe then transport” agrees with “transport then probe.”

If every \(\chi _A\) is invertible, the extension preserves the selected infinitesimal geometry strongly. If not, the discrepancy can reveal genuinely new directions, collapsed distinctions, or a failure to transport old evidence. Such a discrepancy is not automatically an error. Transformational creativity may intentionally change the geometry; the admission record must say which changes are licensed.

. The creative jump is not \(F(A)X\), \(\Theta _{\mathrm{int}}\), or \(\Omega _{\mathrm{cre}}\). Its candidate is a finite package comparison \(\Upsilon \). When the presentation changes, that comparison includes the finite sketch map \(J\), semantic transport \(\bar J\), and an account \(\chi \) of how infinitesimal meaning would change across the jump. The double repair geometry supplies local evidence; \(\Upsilon \) records the global proposal, with a differential theory extension as its presentation-changing case. Only independent admission promotes that proposal to an achieved change.