8. Appendix

8.1. Source index

File	Purpose
ontologies/formulas/formulas-ontology.json	Chain declaration of the FormulaTerm inductive type, the Operator class, and the v1 catalog (add, mul, pow, etc.)
kernel/src/esl/lexer.rs	Lexer; tokenises + - * / ^ and the unary-minus rules described in chapter 5 §5.3
kernel/src/esl/parser.rs	formula(...) Pratt parser; lowers the math sublanguage to Value::CtorApp literals
kernel/src/esl/compile.rs	Lowers Value::CtorApp to chain-bound Value::Json carrying the canonical tagged-dict shape
kernel/src/validation/	The validator’s inductive-value rule (chapter 3 §3.4); the App-spine arity check (chapter 4 §4.3)
crates/runtime-substrate/src/mirror_generator.rs	Closure walker; emits per-ctor decoder/encoder code for FormulaTerm and other inductives
crates/eigenius-julia/src/mirror_gen.rs	Julia-specific mirror generator; emits decode_FormulaTerm and per-ctor structs
julia/institutions/symbolics/EigeniusSymbolics/src/EigeniusSymbolics.jl	formula_to_num walker — the most thorough per-handler example
julia/institutions/intervals/EigeniusIntervals/src/EigeniusIntervals.jl	formula_to_interval walker
julia/institutions/diffeq/EigeniusDiffEq/src/EigeniusDiffEq.jl	formula_to_value walker; ODE RHS interpretation
julia/institutions/jump/EigeniusJuMPHiGHS/src/EigeniusJuMPHiGHS.jl	formula_to_jump walker; smart-pow rule
julia/comorphisms/symbolics-to-intervals.eigon.json, catalyst-to-diffeq.eigon.json, symbolics-to-jump.eigon.json	The three v1 cross-institution comorphisms; identity transformations on FormulaTerm

8.2. Worked-example references

The kinase-institutions notebook is the canonical end-to-end exercise of the formula language across institutions:

• notebooks/examples/kinase-institutions.json — twelve cells exercising FormulaTerm in DiffEq RHS, JuMP objective, OptimisesTo claims, and comorphism dispatch through both ESL and EigenQL surfaces.
• notebooks/examples/kinase-institutions-setup.sh — installs the five institutions and three comorphisms.

The per-institution Julia tutorials (under platform/julia-institutions/) each exercise FormulaTerm in their own institution’s vocabulary:

• Symbolics — most thorough, exercises validator + AutoOnLoad + OnDemand + Decidable
• IntervalArithmetic — substrate plumbing slow-walk
• Catalyst
• DiffEq
• JuMP-HiGHS

8.3. Related design documents

• D32 — Chain-Mirrored EigenTT Inductives — the canonical specification for the formula language.
• D14 — Institution Realisation — institution model; §4 covers ExportFormat / ImportFormat / Comorphism shapes.
• D19 — Inductive Types — the inductive-types-on-the-chain mechanism formulas:FormulaTerm is declared with.
• D27 — Julia institutions — the v1 Julia institution suite that consumes FormulaTerm.
• D29 — Mirror Generator — closure walker; emits the per-ctor decoder/encoder code that walks FormulaTerm values.

8.4. Cross-language guides

• ESL user guide — surface syntax for ontologies and programs; formula(...) shows up in §5 Expressions.
• EigenQL user guide — surface syntax for queries; FIBER param coercion across FormulaTerm-speaking institutions in §7.
• Platform §11 — Runtime substrate — hosting layer for the institutions that consume FormulaTerm.

8.5. Phase status

The formula language is currently complete through Phase 19f.3:

• Phase 19f.1 — formulas:FormulaTerm chain declaration; v1 operator catalog; validator’s inductive-value rule.
• Phase 19f.2 — ctor-call literals on the ESL surface (App(...), OpRef(...), Var(...), LitFloat(...)); typed inline authoring without raw eigen.load(JSON.stringify(...)) workarounds.
• Phase 19f.3 — Pratt-parsed formula(...) sublanguage in ESL; lexer-level unary-minus refactor.
• Phase 19h.1 — Catalyst → DiffEq comorphism (identity on OdeProblem).
• Phase 19f.1 — Symbolics → JuMP comorphism (identity on OptimisationProblem).
• Phase 19d.2 — Symbolics → IntervalArithmetic comorphism (identity on FormulaTerm).
• Phase 19i — Comorphism chain reinsertion (D14 §9.3); both ESL program-invoke (Exp::InstitutionInvoke) and EigenQL FIBER ... INTO surfaces.

Next: structured-clause cross-institution flows under the Curry–Howard reading from chapter 2 §2.2; medium-term as application demand grows.

---

Return to README.