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.
CompressionOp with fields contractive and injective — proved in §6.
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.
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.
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.