Principia Orthogona · dm³ Series · Course 1 of 3

dm³ 101 — Foundations

Contact Geometry, the Cajueiro Seed, and the Operator Chain

The first course in the dm³ sequence. Students build from topology to contact manifolds, derive the n-bonacci ladder from first principles, and arrive at the embodiment threshold τ = 2. No prior differential geometry required — only curiosity and the willingness to follow a seed to its canopy.

16 Weeks Prerequisite: Calculus I Zenodo Paper × 2 AXLE Intro Leads to dm³ 102

Weeks

Operator phases

Zenodo papers

n-bonacci rungs

τ=2

Embodiment threshold

dm³ 101 — 16-Week Journey

C = Compress · K = Threshold · F = Fold · U = Unfold · ● = milestone

Seed / Cajueiro

Topology Primer

Contact Forms

●

Paper 1 · Zenodo

LAW3M ODE

Lyapunov / ε₀

r★ Whitney Fold

●

Paper 2 · GitHub

π · φ · Fibonacci

W10

η · Δ · Σ · Ω

W11

Operator Chain G

W12

Fixed Point

W13

AXLE Setup

W14

First Proof

W15

Cajueiro Cycle

W16

τ=2

Complete Circuit

Coperator

Weeks 1 – 4 · Compression Phase

Perceiving Structure — From Topology to Contact Geometry

Before a student can use the operator chain, they must see it. Phase C of 101 compresses the necessary mathematical vocabulary into four weeks: sets and maps, smooth manifolds, differential forms, and the contact structure α = dz − r²dθ on ℝ³. The Cajueiro seed is the frame: everything visible was once invisible and compressed.

Topology primer Differential forms ch1-seed.html Zenodo Paper 1

01week

The Cajueiro Principle — We Perceive the Unfolding First

ch1-seed.html · Operator C · No prerequisites

StudyChapter

Study

Read ch1-seed.html — the cajueiro as model of scientific unfolding
Observe: what is visible first in any system you already know?
Vocabulary: operator, compression, observable, threshold, seed

Write

One-page reflection: describe a system you know well in cajueiro terms (seed → canopy)
Post to GitHub as your first README entry

LLM Prompt 1.1

"Explain the cajueiro principle to me as if I have never studied mathematics. What does it mean that we always perceive the unfolding before the seed?"

02week

Topology Primer — Sets, Maps, and Continuity

Foundations · Operator C · Level: pre-calculus comfort

MathematicsStudy

Mathematics

Open and closed sets; continuous maps; homeomorphisms
Manifold definition: locally ℝⁿ, globally interesting
Tangent vectors and tangent bundle TM

dm³ Connection

ℝ³ with coordinates (r, θ, z) as the ambient manifold for dm³
What does "the limit cycle Γ lives in ℝ³" mean concretely?
Sketch Γ: a closed curve at r=1

03week

Contact Structures — The Geometry of Constraint

α = dz − r²dθ · contact form · Legendrian submanifolds

Mathematics

Differential 1-forms; the form α = dz − r²dθ on ℝ³
Contact condition: α ∧ dα ≠ 0 everywhere
Legendrian submanifolds: curves tangent to ker(α)
Reeb vector field R_α: the flow along the contact structure

dm³ Connection

The LAW3M limit cycle Γ is Legendrian in (ℝ³, α)
Why this matters: dynamics constrained by contact form ↔ G preserving α
Draw α as a field of planes in ℝ³ — where are they tangent to Γ?

04week

Paper 1 — The Contact Structure of dm³: A Reading Report

Zenodo deposit · 3–4 pages · cite Vol I DOI

ZenodoMilestone

Deliverable

3–4 page PDF: explain the contact structure α = dz − r²dθ in your own words
Include: definition, contact condition, one example (Γ)
Cite: Principia Orthogona Vol I, doi:10.5281/zenodo.20298665

Process

Draft using LLM Prompt 4.1 below
Upload to Zenodo — record your DOI
Add DOI to your GitHub README

LLM Prompt 4.1

"I have studied contact geometry for three weeks. Help me write a clear 3-page report explaining the contact structure α = dz − r²dθ, why the contact condition α ∧ dα ≠ 0 matters, and what a Legendrian curve is. Audience: first-year graduate student."

Koperator

Weeks 5 – 8 · Threshold Phase

Stability — LAW3M, Lyapunov, and the Whitney Fold

Phase K asks: what is stable, and how do we know? The LAW3M ODE is the core dynamical system. Students derive ε₀ = 1/3 from the Lyapunov energy function V = (r−1)²/2, locate the Whitney A₁ fold threshold r★ ≈ 0.776, and learn why det(J) ≈ −0.364 is not the same number as ε₀. Precision here pays off in every course that follows.

LAW3M ODELyapunov stability ε₀ = 1/3r★ ≈ 0.776 GitHub Paper 2

05week

The LAW3M ODE — The Core Dynamical System

ṙ = r(1−r²) + 2(r−1)e^{−z} · θ̇ = 1 · ż = r² − 2(r−1)²e^{−z}

Mathematics

Write down the LAW3M system; identify each term
Limit cycle Γ: r=1, θ̇=1, ż=1 — verify this is a solution
Linearise around r=1: obtain the Jacobian J at Γ
Compute det(J) at the saddle r_s = 2cos(3π/7) ≈ 0.445 → det(J) ≈ −0.364

Key Distinction

det(J) ≈ −0.364 is the Jacobian determinant at the saddle — a property of the unstable fixed point
ε₀ = 1/3 will come from Lyapunov (next week) — a property of the stable cycle
These are different quantities; conflating them is the most common error in dm³ literature

06week

Lyapunov Stability — Deriving ε₀ = 1/3

V = (r−1)²/2 · stability radius · μ = −2

MathematicschMu-lyapunov.html

Mathematics

Lyapunov function V(r) = (r−1)²/2 ≥ 0, V=0 iff r=1
Compute dV/dt along LAW3M trajectories; show dV/dt ≤ 0 for |r−1| < ε₀
Solve for ε₀: the stability radius is ε₀ = 1/3 (Theorem D, Vol II)
Transverse decay rate μ = −2: linearise transversely to Γ

dm³ Connection

ε₀ = 1/3 means: initial conditions within 1/3 of r=1 converge to Γ
μ = −2 is the Lyapunov exponent — third rung of the operator chain
Read chMu-lyapunov.html; cross-reference Vol II, Theorem D

07week

The Whitney A₁ Fold — r★ ≈ 0.776

Inner basin boundary · Whitney fold threshold · distinct from ε₀

Mathematics

Whitney A₁ fold singularity: where the basin boundary has a fold-type geometry
r★ = 0.77594059 ≈ 0.776: numerical inner boundary of the LAW3M basin
Initial conditions with ρ₀ > r★ and within ε₀ of Γ converge to Γ
Initial conditions with ρ₀ < r★ may escape — the fold is a one-way door

Three Numbers to Distinguish

r★ ≈ 0.776 — Whitney fold / inner basin boundary
ε₀ = 1/3 ≈ 0.333 — Lyapunov stability radius from V=(r−1)²/2
det(J) ≈ −0.364 — Jacobian at the saddle r_s ≈ 0.445
None of these equals any other. Know all three by name.

08week

Paper 2 — Stability Analysis of the LAW3M System

GitHub Pages · 4–6 pages · derive ε₀, r★, det(J) clearly

GitHub PagesMilestone

Deliverable

4–6 page technical note: the three stability numbers, derived and distinguished
Must include: Lyapunov derivation of ε₀, Whitney fold description of r★, Jacobian computation of det(J)
Publish on GitHub Pages; link from Zenodo Paper 1

Self-check

Does your paper clearly state ε₀ ≠ det(J)?
Does it state ε₀ comes from Lyapunov, NOT Gronwall?
Does r★ appear with all 8 significant figures: 0.77594059?

Foperator

Weeks 9 – 12 · Fold Phase

The n-Bonacci Ladder — π to Ω

Each rung of the ladder is a root of an n-th degree characteristic polynomial. The sequence π, φ, η, Δ, Σ, Ω converges to τ = 2 — the diameter of the circle the limit cycle traces, the embodiment threshold, the fixed point of G. Students climb all seven rungs.

ch9-phi.htmlchEta-tribonacci.html chDelta-tetranacci.htmlchSigma-pentanacci.html

09week

π and φ — Period and the Golden Ratio

chPI-recurrence.html · ch9-phi.html · rungs 1 and 2

MathematicsChapters

π — Period T★ = 2π

The limit cycle has period T★ = 2π in θ — this is rung 1
Read chPI-recurrence.html: period as the opener of the operator chain
Why 2π? The contact rotation θ̇ = 1 completes one circuit per 2π units of time

φ ≈ 1.618 — Fibonacci

2-term recurrence: a(n) = a(n−1) + a(n−2)
Dominant root of x² − x − 1 = 0: φ = (1+√5)/2
Read ch9-phi.html: φ in spiral geometry, phyllotaxis, dm³ phase weights

10week

η, Δ, Σ, Ω — Tribonacci to Hexabonacci

Rungs 3–6 · convergence to τ = 2

MathematicsChapters

The Four Middle Rungs

η ≈ 1.839: root of x³ − x² − x − 1 = 0 (tribonacci)
Δ ≈ 1.927: root of x⁴ − x³ − x² − x − 1 = 0 (tetranacci)
Σ ≈ 1.966: root of x⁵ polynomial (pentanacci)
Ω ≈ 1.984: root of x⁶ polynomial (hexabonacci)

The Convergence

Gap to τ=2: |φ−2| = 0.382; |η−2| = 0.161; |Δ−2| = 0.073; |Σ−2| = 0.034; |Ω−2| = 0.016
The gap halves (roughly) at each rung — exponential convergence
lim_{k→∞} g_k = 2 = τ: the n-bonacci ladder closes at the embodiment threshold

11week

The Operator Chain G = U ∘ F ∘ K ∘ C

chE-gtct.html · composition · fixed point theorem

Mathematics

The Chain

C: compression operator — maps observables to structure
K: threshold operator — locates the critical transition
F: fold operator — the Whitney-type fold geometry
U: unfolding operator — traces the canopy from the seed
G = U ∘ F ∘ K ∘ C: one complete circuit

Fixed Point

G(x★) = x★: the fixed point is τ = 2, the embodiment threshold
Banach fixed-point theorem applies on the basin of attraction
G⁶ = G∘G∘G∘G∘G∘G: the sixth iterate closes the recurrence cycle (g₃₃ = 33)

12week

The Fixed Point — G(x★) = x★ and the Complete Circuit

ch7-complete-circuit.html · synthesis week

MathematicsChapters

Synthesis

Trace one full G-orbit from a point near r★ to τ=2
Connect the n-bonacci ladder to G: each rung is one application of F
The chain closes: Ω → π. What does this mean geometrically?

Prepare for 101 Final

Write a one-page summary: the three stability numbers, the ladder, the fixed point
This becomes the introduction to your dm³ 101 final paper (Week 16)

Uoperator

Weeks 13 – 16 · Unfolding Phase

AXLE Introduction and the First Complete Proof

Phase U of 101 introduces Lean 4 and the AXLE proof environment. Students verify a single small claim from Phase K — the Lyapunov bound ε₀ = 1/3 — and publish the result. The Cajueiro cycle completes: seed→canopy→new seed.

Lean 4 basicsAXLE repo github.com/TOTOGT/AXLEFinal Paper

13week

Lean 4 and AXLE — Reading the Proof Environment

github.com/TOTOGT/AXLE · chV-axle.html

AXLE

Setup

Install Lean 4 and Mathlib; clone AXLE repo
Read chV-axle.html: the proof architecture overview
Understand: theorem vs axiom vs sorry in AXLE tier system

First Read

Open AXLE/main.lean; locate the Lyapunov stability theorem
Identify every `sorry` — these are the open problems
Read the `gronwall_outer` identifier — it is a Lean name, not a mathematical claim about Gronwall

14week

Your First Lean Proof — Verifying a Tier-A Lemma

chV-sorrys.html · clear one sorry

AXLEMathematics

Task

Choose one Tier-A (simplest) sorry from chV-sorrys.html
Write the Lean 4 proof; get Lean to accept it (no red squiggles)
Commit to your fork of AXLE with a descriptive message

Document

Write 1 page explaining: what was the claim, how you proved it, what Mathlib lemmas you used
This is the core of your Week 16 final paper

15week

The Cajueiro Cycle — Reflecting on a Complete Circuit

Synthesis · connect seed (W1) to canopy (W14)

Reflection

Return to your Week 1 cajueiro reflection — what was the seed?
Map your 14-week trajectory onto the G = U∘F∘K∘C chain
Where in the chain are you now? Where is your paper?

Final Paper Draft

Combine: Week 8 stability paper + Week 14 AXLE proof + this reflection
Title: "One Circuit of the dm³ Operator Chain: Stability, Ladder, and First Proof"
Draft complete; submit for peer review to course partner

16week

τ = 2 — The Complete Circuit · Final Publication

Zenodo DOI · GitHub Pages · ready for dm³ 102

ZenodoMilestone · τ = 2

Deliverables

Final paper: 8–12 pages, Zenodo DOI, CC BY 4.0
AXLE contribution: one cleared sorry committed and documented
GitHub repo: complete with README, all papers linked

Readiness for dm³ 102

You know: α = dz − r²dθ, ε₀ = 1/3 (Lyapunov), r★ ≈ 0.776, det(J) ≈ −0.364
You can distinguish the three stability numbers and state why they differ
You have: 2 published papers, 1 AXLE contribution, 1 GitHub repo

Principia Orthogona · dm³ Series · Course 2 of 3

dm³ 102 — Applications

The Scientists Series · Chaos · Morphogenesis · Fractals · Contact Geometry in Nature

The second course applies the dm³ framework to landmark results in modern mathematics and biology. Lorenz (chaos), Turing (morphogenesis), Mandelbrot (fractals), Poincaré–Einstein (relativity contact structure), and Waddington (epigenetic landscape) — each chapter is a case study in G = U∘F∘K∘C in the wild. The μ-η-Δ arc in Weeks 13–14 anchors the Turing chapter.

16 Weeks Prerequisite: dm³ 101 Scientists Series chapters Turing at W13–14 Leads to dm³ 103

Weeks

Scientist case studies

W13–14

Turing / μ-η-Δ arc

Zenodo papers

AXLE

Tier-B sorrys

dm³ 102 — 16-Week Journey

Highlighted cells = Scientists Series chapters · Gold = μ-η-Δ arc (Turing placement)

Lorenz · Chaos

Strange Attractors

Symmetry Breaking

●

Paper 1 · Chaos

Poincaré · Topology

Einstein · Relativity

Contact + Relativity

●

Paper 2 · P–E

Mandelbrot · Fractals

W10

Waddington · Landscape

W11

Lyapunov Potential

W12

Pattern vs Chaos

W13

Turing · RD Equations

W14

η·Δ

Turing · Contact Geom

W15

Synthesis

W16

τ=2

Final Paper

Coperator

Weeks 1 – 4 · Compression Phase

Chaos Theory — Lorenz and the Strange Attractor

Phase C of 102 compresses chaos theory through the Lorenz system, establishing the contrast that makes Turing's pattern-formation result surprising: chaos and pattern emerge from structurally similar nonlinear systems. The student who understands why Lorenz is chaotic understands why Turing's result is remarkable.

ch-lorenz-chaos.html Strange attractor Sensitive dependence Zenodo Paper 1

01week

Lorenz (1963) — Deterministic Nonperiodic Flow

ch-lorenz-chaos.html · strange attractor · butterfly effect

StudyChapter

Study

Read ch-lorenz-chaos.html in full
The Lorenz system: ẋ = σ(y−x), ẏ = x(ρ−z)−y, ż = xy − βz
The strange attractor: bounded but never periodic, fractal cross-section
Sensitive dependence on initial conditions: why prediction fails

dm³ Connection

Lorenz is NOT a fixed-point attractor — it is a strange attractor
dm³ G converges to a fixed point τ=2; Lorenz orbits never settle
This contrast is the first lesson of 102: not all nonlinear systems have fixed points

02week

Strange Attractors and Fractal Dimension

Hausdorff dimension · Lyapunov spectrum · KAM theory intro

Mathematics

Fractal dimension d_H of the Lorenz attractor ≈ 2.06
Lyapunov exponent spectrum: one positive (chaos), one zero (flow direction), one negative
dm³ has μ = −2 (all negative transverse exponents) — hence convergence, not chaos

Key Contrast Table

Lorenz: Lyapunov exponents (+, 0, −) → chaos
dm³ LAW3M on Γ: exponents (0, −2, ...) → stable limit cycle
The sign of the largest Lyapunov exponent is the chaos/order boundary

03week

Symmetry Breaking — From Order to Chaos and Back

Bifurcation theory · Hopf bifurcation · period-doubling

Mathematics

Bifurcation: a qualitative change in dynamics as a parameter varies
Hopf bifurcation: stable fixed point → limit cycle (as in LAW3M)
Period-doubling route to chaos: Feigenbaum constant δ ≈ 4.669

dm³ Connection

The LAW3M ODE undergoes a Hopf bifurcation producing the limit cycle Γ
Before the bifurcation: stable fixed point. After: stable cycle at r=1
r★ ≈ 0.776 is the post-bifurcation fold — the inner basin boundary

04week

Paper 1 — Chaos vs Order: Lorenz and dm³ Compared

Zenodo · 4–5 pages · Lyapunov exponent comparison

ZenodoMilestone

Deliverable

Compare Lorenz and LAW3M via their Lyapunov exponent spectra
Explain why one produces a strange attractor and one a fixed point
Include: bifurcation diagram, exponent table, one figure

Citations

Lorenz 1963, J. Atmos. Sci. 20:130–141
Principia Orthogona Vol II, doi:10.5281/zenodo.21148424
ch-lorenz-chaos.html (cite URL)

Koperator

Weeks 5 – 8 · Threshold Phase

Poincaré–Einstein — Contact Geometry Meets Relativity

The threshold of 102 is the recognition that contact geometry is not an invention of the dm³ framework — it is the natural language for constrained dynamics, from Poincaré's three-body work to Einstein's spacetime. This phase reads ch-poincare-einstein.html and connects the contact condition to the null-cone structure of special relativity.

ch-poincare-einstein.html Poincaré recurrence Null cone Paper 2

05week

Poincaré — Topology, Three-Body Problem, Recurrence

ch-poincare-einstein.html · Poincaré recurrence theorem · homoclinic orbit

StudyChapter

Study

Poincaré recurrence: almost every trajectory returns arbitrarily close to its start
The three-body problem as the first recognised chaotic system (1890)
Poincaré section: reduce continuous flow to discrete map

dm³ Connection

The dm³ G-orbit returns: G(x★)=x★ is the fixed-point version of recurrence
Poincaré section of LAW3M at θ=0: reduces to a 2D map in (r,z)

06week

Einstein — Spacetime Geometry and the Contact Analogy

Minkowski metric · null cone · contact condition on lightlike hypersurfaces

Mathematics

Minkowski metric: ds² = −c²dt² + dx² + dy² + dz²
Null cone: ds²=0 defines lightlike directions
Contact structure on null hypersurfaces: the restriction of the metric to the null cone has a contact structure

Analogy

LAW3M contact form α = dz − r²dθ: a non-degenerate constraint on ℝ³
Null cone contact structure: a non-degenerate constraint on lightlike surfaces in ℝ³˒¹
Both: the contact condition α ∧ dα ≠ 0 is the non-degeneracy condition

07week

Contact Geometry as Universal Language

Symplectic vs contact · Legendrian submanifolds in physics

Mathematics

Symplectic geometry (even-dim): Hamiltonian mechanics, phase space
Contact geometry (odd-dim): adds time/energy coordinate, thermodynamics, optics
Every symplectic manifold has a contact boundary (Gromov, 1985)

dm³ Placement

ℝ³ is 3-dimensional (odd) → contact, not symplectic
The LAW3M dynamics live in the contact setting by construction
This is why G preserves α: it is a contactomorphism

08week

Paper 2 — Contact Geometry from Poincaré to dm³

GitHub Pages · 5–6 pages

GitHubMilestone

Deliverable

Trace contact geometry from Poincaré's three-body work → Einstein's null cone → LAW3M
Show: same mathematical structure, three historical appearances
Section 3 must state precisely why dm³ uses contact geometry (not symplectic)

Self-check

Do you distinguish symplectic (even-dim) from contact (odd-dim)?
Is the contact condition stated correctly: α ∧ dα ≠ 0?

Foperator

Weeks 9 – 12 · Fold Phase

Fractals, Waddington, and the Edge Between Pattern and Chaos

Mandelbrot showed that the boundary between bounded and unbounded iteration is infinitely complex — a fractal. Waddington showed that development follows valleys in an energy landscape. Both are fold-phase phenomena in dm³ terms: the Whitney fold is the edge between two basins, and every valley in Waddington's landscape is a Lyapunov minimum. Weeks 9–12 prepare the ground for the Turing arc in Weeks 13–14.

ch-mandelbrot-fractals.html chDev-waddington.html Lyapunov landscape

09week

Mandelbrot — The Geometry of Iteration Boundaries

ch-mandelbrot-fractals.html · Mandelbrot set · Julia sets · self-similarity

StudyChapter

Study

Read ch-mandelbrot-fractals.html
Mandelbrot set M: {c ∈ ℂ : |z_n| stays bounded under z↦z²+c}
The boundary ∂M is a fractal of infinite complexity — every zoom reveals new structure
Hausdorff dimension of ∂M = 2 (Shishikura, 1998)

dm³ Connection

The basin boundary of LAW3M (near r★ ≈ 0.776) is the dm³ analogue of ∂M
The Whitney fold at r★ is a smooth fold, not a fractal — this is what the contact structure buys
Contrast: fractal basin boundary (generic nonlinear) vs smooth fold (contact-geometric)

10week

Waddington — The Epigenetic Landscape as Lyapunov Potential

chDev-waddington.html · valleys = attractors · ridges = separatrices

StudyChapter

Study

Waddington (1957): development as a ball rolling down a landscape of valleys
Each valley = one cell fate (attractor); ridges = unstable boundaries (separatrices)
The landscape IS the Lyapunov function V — valleys are minima of V

dm³ Connection

V(r) = (r−1)²/2: the dm³ Lyapunov function has one valley at r=1 (the limit cycle Γ)
r★ ≈ 0.776 is the ridge — below it, the trajectory escapes to a different fate
Cross-reference: this sets up the Turing chapter (W13–14): Turing patterns ARE Waddington valleys in chemical space

11week

The Lyapunov Landscape — Potential Theory for Pattern Formation

Gradient systems · quasi-potential · chemical potential

Mathematics

Gradient system: ẋ = −∇V(x). Trajectories follow steepest descent.
LAW3M is NOT a gradient system (it has rotation) — but V(r)=(r−1)²/2 captures the radial component
Quasi-potential: for non-gradient systems, define V via the stationary Fokker-Planck equation

Preview of Turing

Turing patterns: the uniform state is a local maximum of the chemical "potential"
Turing instability = the uniform state becomes a saddle, and spatial modes are the new valleys
dm³ contact structure selects which spatial modes are Legendrian (stable)

12week

Pattern vs Chaos — The Classification Problem

Synthesis week · preparing the μ-η-Δ arc

Mathematics

Synthesis

Three regimes: fixed point (dm³ G), limit cycle (LAW3M), strange attractor (Lorenz)
Pattern formation (Turing) is a fourth regime: spatial structure from instability
The μ operator (Lyapunov exponent −2) is what distinguishes dm³ from chaos

Prepare for W13–14

Re-read chMu-lyapunov.html and chEta-tribonacci.html from dm³ 101
Write one paragraph: how does Turing instability connect to the μ operator?
This paragraph becomes the introduction to your W13 report

Uoperator

Weeks 13 – 16 · Unfolding Phase · μ-η-Δ Arc

Turing Morphogenesis — Reaction-Diffusion in Contact Geometry

The μ-η-Δ arc is the culmination of 102. Weeks 13–14 work through ch-turing-morphogenesis.html in full: the 1952 paper, the RD equations, the Gierer-Meinhardt model, and the dm³ reading (Turing instability as G-orbit divergence from the uniform state). Week 15 synthesises all five scientists. Week 16 is the final publication.

ch-turing-morphogenesis.html μ = −2 stabilises patterns η weighting AXLE Turing stub Final Paper

13week

Turing (1952) — Reaction-Diffusion and Symmetry Breaking

ch-turing-morphogenesis.html §1–3 · RD equations · Gierer-Meinhardt · dispersion relation

StudyTuring Chapter §1–3μ-η-Δ Arc

Study: §1–2 of Turing chapter

Read §1: the 1952 paper context — post-Bletchley, pattern without blueprint
Read §2: the RD system du/dt = D_u·∇²u + f(u,v); dv/dt = D_v·∇²v + g(u,v)
Turing condition: D_v/D_u ≫ 1 (inhibitor diffuses much faster than activator)
Dispersion relation: critical wavenumber k★² = √(f_u·g_v / D_u·D_v)

Mathematics

Linear stability analysis of uniform steady state (u₀, v₀)
Without diffusion: stable. With diffusion + D_v ≫ D_u: unstable to spatial mode k★
Gierer-Meinhardt model (1972): canonical RD with explicit f, g
Biological confirmation: CIMA reaction (1990); Sheth et al. digit spacing (Science 2012)

LLM Prompt 13.1

"Explain Turing's 1952 morphogenesis result to me: what is the activator-inhibitor mechanism, why does fast inhibitor diffusion cause instability, and what is the critical wavenumber k★? Use the Gierer-Meinhardt model as your example."

14week

Turing in Contact Geometry — §3–5 and the AXLE Stub

ch-turing-morphogenesis.html §3–5 · dm³ reading · Legendrian pattern · G stabilises Turing

MathematicsAXLEμ-η-Δ Arc

Study: §3–5 of Turing chapter

§3: the contact-geometric reading — tissue manifold (M, α), Legendrian submanifold L where pattern develops
§4: dm³ claim — Turing instability selects spatial mode k★; G selects fixed point τ=2. Same phenomenon, different scale.
Analogy: n (n-bonacci index) ↔ k★ (Turing wavenumber); both break symmetry to select a preferred scale
§5: the AXLE stub — three parts, all marked sorry (Tier C)

AXLE Engagement

Open the AXLE Turing stub: turing_instability axiom + G_stabilises_turing_pattern theorem
The theorem uses sorry — it is Tier C (requires μ-operator mechanisation first)
Task: write a 1-page proof sketch for how you would clear the sorry, given the Banach fixed-point theorem on morphogen space

LLM Prompt 14.1

"In the dm³ framework, Turing morphogenesis is read as G-orbit divergence from a uniform state followed by convergence to a patterned fixed point. Explain this analogy precisely: what plays the role of the n-bonacci index n in Turing's system, and why does the μ operator (Lyapunov exponent −2) stabilise the resulting pattern?"

Cross-references from Turing §6 (Curriculum Placement) chDev-waddington.html · chMu-lyapunov.html · ch-lorenz-chaos.html · this page (dm3-102 W13–14)

15week

Five Scientists, One Framework — Synthesis

Lorenz · Poincaré · Mandelbrot · Waddington · Turing through the dm³ lens

Synthesis

Synthesis Task

Build a comparison table: Scientist · System · Attractor type · dm³ analogue
Lorenz: strange attractor ↔ μ > 0 regime (not dm³ but instructive contrast)
Turing: patterned fixed point ↔ G-stabilised Legendrian mode
Waddington: Lyapunov landscape ↔ V(r)=(r−1)²/2

Final Paper Outline

Section 1: Chaos and pattern as two sides of nonlinearity (Lorenz vs Turing)
Section 2: Contact geometry as the unifying language (Poincaré–Einstein bridge)
Section 3: The μ-η-Δ arc — how dm³ stabilises Turing patterns
Section 4: Open problems (the three sorry theorems in AXLE)

16week

Final Paper — dm³ Reads Five Scientists

Zenodo DOI · 8–12 pages · ready for dm³ 103

ZenodoMilestone · τ = 2

Deliverables

Final paper: 8–12 pages, synthesis of all five scientists via dm³
Must include: the Turing / μ-η-Δ connection as the centrepiece argument
Zenodo deposit with DOI; link from dm³ 101 final paper

Readiness for dm³ 103

You can read AXLE sorry stubs and write proof sketches
You have traced contact geometry through five historical case studies
You understand why Turing patterns are Legendrian and G-stable

Principia Orthogona · dm³ Series · Course 3 of 3

dm³ 103 — Mechanisation

AXLE · Lean 4 · Clearing Sorrys · The Full Publication Pipeline

The third course is for those who want to build the proof, not just read it. Students work directly in AXLE, clearing sorry stubs tier by tier — from the simplest algebraic identities (Tier A) to the contact-geometric fixed-point theorems (Tier C). The course ends with a co-authored Zenodo paper contributing new mechanised proofs to the series.

16 Weeks Prerequisite: dm³ 102 Lean 4 + Mathlib Co-authored Zenodo paper AXLE contributor

Weeks

Tier levels (A→C)

≥4

Sorrys cleared

Co-authored paper

DOI

Zenodo contribution

dm³ 103 — 16-Week Journey

A = simplest proofs · B = intermediate · C = contact-geometric · ● = milestone

AXLE Read

Lean 4 Tactics

Mathlib Survey

Tier A Cleared

ε₀ Proof Setup

Lyapunov in Lean

r★ Computation

Tier B Cleared

Contact Forms

W10

G Preserves α

W11

Fixed Point Thm

W12

Tier C Attempt

W13

Paper Draft

W14

Peer Review

W15

Revision

W16

DOI

Zenodo Deposit

Coperator

Weeks 1 – 4 · Compression Phase · Tier A

Reading AXLE — The Sorry Architecture and Lean 4 Fluency

Before clearing any sorry, the student must understand the full AXLE proof architecture. Weeks 1–3 build Lean 4 tactic fluency and survey the Mathlib library. Week 4 clears the first Tier-A sorrys — algebraic identities and basic ODE existence results that require only `ring`, `norm_num`, and `linarith`.

chV-axle.htmlchV-sorrys.html Lean 4 tacticsMathlib.Analysis.ODE

01week

Reading the AXLE Architecture — chV-axle.html in Full

github.com/TOTOGT/AXLE · proof tiers · sorry map

AXLEStudy

Study

Read chV-axle.html completely — every section
Clone AXLE repo; run `lake build` — understand the build system
Map every `sorry` in the repo into: Tier A (algebraic), Tier B (analytic), Tier C (geometric)
The gronwall_outer identifier is a Lean name for an auxiliary lemma — it is NOT a claim that ε₀=1/3 comes from Gronwall

Critical Distinctions

Mathlib.Analysis.ODE.Gronwall: a real Mathlib import used for ODE bounds
gronwall_outer: an AXLE-specific identifier for an outer basin lemma
ε₀ = 1/3 is derived from V=(r−1)²/2, NOT from Gronwall's lemma
These must be stated precisely in any paper using AXLE

02week

Lean 4 Tactics — The Proof Language

ring · norm_num · linarith · simp · exact · apply · intro

Lean 4Tactics

Core Tactics

ring: proves equalities in commutative rings — for algebraic identities
norm_num: proves numerical facts (e.g., 1/3 < 1/2)
linarith: proves linear arithmetic goals
nlinarith: nonlinear arithmetic — needed for quadratic inequalities

Structure Tactics

intro h: introduce a hypothesis
apply lemma: reduce to subgoals via a lemma
exact h: close goal with exact term
simp [lemma1, lemma2]: simplify using lemmas
constructor: split a conjunction

03week

Mathlib Survey — What Is Already Proved

Mathlib.Analysis.ODE · Mathlib.Topology.MetricSpace · Banach fixed point

Mathlib

Key Mathlib Modules

Mathlib.Analysis.ODE.Gronwall: Gronwall inequality for ODE bounds
Mathlib.Analysis.ODE.PicardLindelof: existence and uniqueness for Lipschitz ODEs
Mathlib.Topology.MetricSpace.Contraction: Banach fixed-point theorem
Mathlib.Analysis.SpecialFunctions.Pow: exponential decay estimates

AXLE Import Strategy

Identify which Mathlib lemmas are needed for each Tier-A sorry
Practice: search Mathlib4 docs for "Lyapunov" — what exists?
Gap: Mathlib has no contact geometry library — AXLE must build it

04week

Clear All Tier-A Sorrys — Algebraic and Arithmetic

ring · norm_num · linarith suffice for all Tier A

AXLEMilestone

Task

Clear every sorry marked Tier A in chV-sorrys.html
Each proof: ring / norm_num / linarith in 1–3 lines
Commit each cleared sorry with message: "clear: [lemma name] (Tier A, dm³ 103 W4)"
Open a pull request against TOTOGT/AXLE with all Tier-A clears

Documentation

Write a 2-page summary: which sorrys were cleared, which tactic worked, why
This becomes Section 2 of your final paper (Week 16)

Koperator

Weeks 5 – 8 · Threshold Phase · Tier B

Lyapunov in Lean — Mechanising ε₀ = 1/3 and r★

Tier B is the analytic core: proving ε₀ = 1/3 from V=(r−1)²/2 in Lean 4, and bounding the Whitney fold numerically at r★ ≈ 0.776. These require Mathlib.Analysis.ODE and careful handling of the distinction between the Lyapunov bound, the Gronwall bound, and the Jacobian determinant.

Lyapunov in Lean 4 ε₀ = 1/3 mechanised r★ numerical bound Gronwall vs Lyapunov distinction

05week

Setting Up the Lyapunov Proof in Lean 4

V = (r−1)²/2 · dV/dt ≤ 0 · stability ball

AXLEMathematics

Lean Setup

Define lyapunov_V : ℝ → ℝ := fun r => (r - 1)^2 / 2
State: ∀ r ∈ Ioo (2/3 : ℝ) (4/3), deriv lyapunov_V r * law3m_r r ≤ 0
This encodes dV/dt ≤ 0 along the ṙ component of LAW3M

Key Distinction in Code

The proof uses nlinarith after expanding — it does NOT invoke Gronwall
gronwall_outer is a separate lemma bounding the outer basin — cite it carefully
Write a comment in the proof: "ε₀=1/3 from Lyapunov V, not from Gronwall inequality"

06week

Mechanising ε₀ = 1/3 — The Full Proof

Lyapunov stability theorem in Lean 4 · Theorem D of Vol II

AXLE

The Proof

Theorem: if |r₀ − 1| < 1/3 then the LAW3M trajectory with r(0)=r₀ satisfies |r(t)−1| → 0
Proof strategy: (1) show V decreasing on (2/3, 4/3); (2) V(r₀) < V(2/3); (3) V bounded below by 0; (4) apply LaSalle
Lean: use Mathlib.Analysis.Lyapunov (if available) or build from primitives

If Mathlib has no Lyapunov module

Build a local Lyapunov.lean in AXLE with the key stability theorem
This itself is a contribution — document it in the final paper
Use Picard-Lindelöf for existence, then Gronwall for the bound (outer basin only)

07week

r★ = 0.77594059 — Numerical Verification in Lean

Interval arithmetic · Lean.Numeric · bounding r★

AXLENumerics

Task

r★ is defined as the Whitney fold threshold — a root of a polynomial equation in the LAW3M system
Prove (or verify numerically): r★ ∈ (0.775, 0.776) using interval arithmetic
Lean tool: native_decide or norm_num with rational interval bounds

Documentation Requirement

Any paper using r★ must state: r★ = 0.77594059 (8 significant figures)
State clearly: r★ is the Whitney A₁ fold threshold / inner basin boundary
State clearly: r★ ≠ ε₀ ≠ |det(J)|. Three separate quantities.

08week

Tier B Complete — ε₀ and r★ Mechanised

Pull request to AXLE · peer review by course partner

AXLE PRMilestone

Deliverables

Pull request: all Tier-B sorrys cleared, with proofs
Each proof commented: what tactic, which Mathlib lemma, why this approach
Companion document: 3–4 pages explaining ε₀ and r★ mechanisation

Peer Review

Exchange PRs with course partner — review each other's proofs
Check: does the proof comment distinguish Lyapunov from Gronwall correctly?
Reviewer sign-off required before merging

Foperator

Weeks 9 – 12 · Fold Phase · Tier C Approach

Contact Geometry in Lean — G Preserves α

Tier C is the frontier: proving that G = U∘F∘K∘C preserves the contact form α, and that the fixed point G(x★)=x★ is τ=2. This requires building contact geometry structures in Lean 4 — structures that do not yet exist in Mathlib. Weeks 9–12 build the necessary scaffolding; Week 12 makes the first Tier-C attempt.

Contact forms in Lean ContactManifold type G preserves α Banach on contact bundle

09week

Building ContactManifold in Lean 4

DifferentialForm · α = dz − r²dθ · contact condition

AXLEMathematics

The Type

Define structure ContactManifold (M : Type*) extends SmoothManifold M
Field: α : DifferentialForm 1 M (the contact form)
Condition: contact_cond : ∀ x, α x ∧ (dα) x ≠ 0 (non-degeneracy)
Instance: ℝ³ with α = dz − r²dθ is a ContactManifold

Challenges

Differential forms are not in Mathlib in the most useful form for this
May need to use Mathlib.Geometry.Manifold.DeRhamCohomology
Fallback: define α as a smooth function and state the contact condition axiomatically

10week

G Preserves α — Stating the Contactomorphism Theorem

Contactomorphism · G★(α) = α · pullback

AXLEMathematics

The Theorem Statement

G is a contactomorphism: G★(α) = α (G preserves the contact form)
In Lean: theorem G_contactomorphism : G.pullback α = α
This requires: definition of pullback of a form; smoothness of G; contact condition

Sorry Status

This is Tier C — currently a sorry in AXLE
The proof would require: (1) explicit formula for G on ℝ³; (2) computation of G★(dz − r²dθ)
Week 10 goal: state the theorem cleanly without sorry, even if the proof body is still sorry

11week

The Fixed-Point Theorem — Banach on Contact Bundle

ContactionMap on contact sections · G^n converges

AXLEMathematics

Approach

Banach fixed-point theorem: if G is a contraction on a complete metric space, ∃! fixed point
The metric space: sections of the contact bundle (smooth functions near Γ)
Contraction rate: μ = −2 (the Lyapunov exponent — already mechanised in Tier B)
Fixed point: τ = 2 = the embodiment threshold

Using Mathlib

Mathlib.Topology.MetricSpace.Contraction.contractionMapping
Apply to G restricted to the Lyapunov ball |r−1| < ε₀ = 1/3
The Tier-B result (ε₀ mechanised) feeds directly into Tier C here

12week

Tier-C Attempt — Partial Proof or Proof Sketch

Clear or reduce at least one Tier-C sorry · document what remains

AXLEMilestone

Goal

Attempt: clear G_contactomorphism or G_stabilises_turing_pattern (Turing stub)
Even a partial reduction (sorry → two smaller sorrys) counts as progress
Document exactly where the proof gets stuck — this is the research frontier

If No Tier-C Sorry Is Clearable

Write a detailed proof sketch: exactly what Lean terms and tactics would be needed
Identify the missing Mathlib lemma — this is a potential future contribution
This sketch becomes the open-problems section of your final paper

Uoperator

Weeks 13 – 16 · Unfolding Phase · Publication

Co-Authored Zenodo Paper — Your AXLE Contribution

The final phase is publication. Students write a co-authored technical paper documenting every cleared sorry, every proof technique, and every open problem encountered. The paper is deposited on Zenodo with a DOI under CC BY 4.0, and linked from the AXLE GitHub repo as an official contribution to the series.

Co-authored paperZenodo DOI CC BY 4.0AXLE contributor credit

13week

Paper Draft — Documenting the Proof Journey

IMRaD structure · proof excerpts · open problems

Writing

Paper Structure

Introduction: AXLE, the sorry architecture, this paper's contribution
Methods: Lean 4 tactics used; Mathlib lemmas invoked
Results: Tier-A and Tier-B sorrys cleared (with proof excerpts)
Discussion: Tier-C status, what remains, proof sketches
Open Problems: the frontier — what Mathlib is missing

Precision Requirements

State ε₀ = 1/3 comes from Lyapunov V=(r−1)²/2, NOT Gronwall
State r★ = 0.77594059 with 8 sig figs; define it as Whitney A₁ fold threshold
State det(J) ≈ −0.364 and explain it is the Jacobian at the saddle r_s ≈ 0.445
These three numbers must be clearly distinguished every time they appear

14week

Peer Review — Course Partner Exchange

Technical review · proof correctness · notation consistency

Peer Review

Review Checklist

Are all three stability numbers (ε₀, r★, det(J)) clearly defined and distinguished?
Is every proof excerpt syntactically valid Lean 4?
Is the Gronwall/Lyapunov distinction stated at least once?
Is the dm³ notation used consistently (dm³ with superscript, never dm3)?

Feedback

Write 1-page review; share with author; receive 1-page review in return
Flag any claim that is not backed by a Lean proof or an explicit sorry

15week

Revision and ORCID Registration

Address reviewer comments · ORCID iD · author metadata

Revision

Address all reviewer comments; re-run any affected Lean proofs
Register at orcid.org — get your ORCID iD (free, 5 minutes)
Final paper: PDF, LaTeX source, all .lean files in a zip

Metadata for Zenodo

Title: "Mechanising dm³ Stability: Cleared Sorrys in the AXLE Proof Environment"
Authors: [your name] + Pablo Nogueira Grossi (ORCID: 0009-0000-6496-2186)
License: CC BY 4.0 · Related to: doi:10.5281/zenodo.19117399

16week

Deposit — Your Name on a DOI · AXLE Contributor Credit

doi:10.5281/zenodo.XXXXXXX · github.com/TOTOGT/AXLE

Zenodo DOIMilestone · Complete

Final Deliverables

Zenodo deposit: paper PDF + .lean files + README
Your DOI added to AXLE README as a contribution
GitHub: your fork of AXLE with all PRs merged (or documented as pending)

What You Have Now

A citable Zenodo paper with your name and DOI
Mechanised proofs in a live Lean 4 repo
Precise knowledge of ε₀, r★, det(J), and why they differ
You are an AXLE contributor. The cajueiro grew a new branch.