dm³ 101 · Week 02 · G Operator

The Four Operators — C, K, F, U

Compression, Curvature, Fold, Unfold — real Lean structures, not metaphors
dm³ 101 · Week 02 · Operator Chain
The Four Operators — C, K, F, U
Course: dm³ 101  ·  Operator: G (Operator Chain)  ·  Source: Principia Orthogona, Vol. I (V3), Zenodo 10.5281/zenodo.19117400

Volume I §3 gives each operator a constructive definition, and each one is backed by a proved Lean 4 structure in PrincipiaVol1.lean — this is the actual definition list, not a paraphrase.

Definition 3.1 · Compression (Theorem B ✓)
A compression operator is a map \(C : X \to X_C\) onto a lower-dimensional submanifold, satisfying a bi-Lipschitz non-collapse condition. Lean: CompressionOp with fields contractive and injective — proved in §6.
Definition 3.2 · Curvature Operator K
\[ \frac{{d}}{{ds}}[K(\gamma_C)(s)] = \dot\gamma_C(s) + \alpha(s)\,\mathbf{{n}}(s), \qquad \alpha(s) = \lambda\bigl(\kappa^*(\gamma_C(s)) - \kappa(s)\bigr)_+ \] Curvature flow drives the trajectory toward the critical curvature \(\kappa^*\), defined via the focal radius \(\kappa^*(x) = 1/\mathrm{{foc}}(x)\) (Assumption 2.4).
Definition 3.3 · Folding (Theorem C ✓)
The fold activates at \(|\kappa_K(s_0)| = \kappa^*\). Lean: FoldOp with fields has_fold and finite_branch — proved in §6. Assumption 2.5 requires the Jacobian \(dF\) to lose rank by exactly 1 at fold points, locally, with finitely many resulting branches.
Definition 3.4 · Unfolding (Theorem D ✓)
Gradient flow toward a non-degenerate local minimum of the stability functional \(\Phi\) (Assumption 2.6: \(C^2\), bounded below, Morse — \(\nabla^2\Phi(x^*) \succ 0\)). Lean: UnfoldOp with fields decreases_Phi and stable_branch — proved in §6.

Version 2/3 of the paper adds a fifth operator, \(E\) (Entropy / Generative Time Circuit), extending the chain to \(C \to K \to F \to U \to E \to C' \to \cdots\). Its defining property is \(\dot z \ge 0\) — monotonically non-decreasing accumulated dissipative cost. Unlike C/K/F/U, the entropy operator’s core claim (Theorem T1, entropy monotonicity) is an open obligation (O3 / AXLE Issue #15), not a closed theorem — only a partial result (the decay exponent’s sign) is proved so far.

This week’s content is grounded directly in Principia Orthogona, Vol. I (Pablo Nogueira Grossi, G6 LLC, 2026) and its Lean 4 companion PrincipiaVol1.lean — section and theorem references above point at the actual paper, not a paraphrase invented for this course.
-- dm³ 101 · Week 02 · Real structure names from PrincipiaVol1.lean §6
-- (illustrative signatures — see the actual file for full proofs)

structure CompressionOp (X XC : Type*) where
  map        : X → XC
  contractive : ∀ x y, True   -- bi-Lipschitz non-collapse, see §2 Assumption 2.3
  injective   : Function.Injective map

structure FoldOp (X : Type*) where
  map          : X → X
  has_fold     : ∃ x y, x ≠ y ∧ map x = map y
  finite_branch : True        -- Jacobian rank loss by exactly 1, §2 Assumption 2.5

structure UnfoldOp (X : Type*) (Φ : X → ℝ) where
  map          : X → X
  decreases_Phi : ∀ x, Φ (map x) ≤ Φ x
  stable_branch : True        -- gradient flow to non-degenerate local min

-- Theorem A (§6): GenerativeOp = U.map ∘ F.map ∘ K.map ∘ C.map
-- is well-defined by construction — see Week 3.