PROMY:SEED — Generic Prompt Template#

Created:

2026-03-29

Origin:

First successful PROMY:SEED run on e7He

Status:

Draft — tested on one model, to be refined with experience

When to Use#

Use this prompt after a FORGE session has produced a model with axioms, theorems, and/or structural properties that exist only inside a FORGE llog and need to be extracted into clean standalone files in the model directory.

The Prompt#

Copy and adapt the following. Replace all {{placeholders}} with the actual values for your model. Do NOT skip the checking checklist — it is the only guarantee that the extraction is correct.

PROMY:SEED {{MODEL_NAME}}

**Source:** The FORGE session llog at
``{{LLOG_PATH}}``
contains all {{MODEL_NAME}} axioms, theorems, and structural
properties. These must be extracted into clean, standalone .rst
files in ``source/matheology/model/{{MODEL_DIR}}/``.

**Inventory to extract ({{TOTAL_COUNT}} statements):**

AXIOMS ({{AXIOM_COUNT}} total):

{{FOR EACH AXIOM:}}
- {{ID}} --- {{NAME}} (llog line ~{{LINE}}, label ``{{LABEL}}``)

THEOREMS ({{THEOREM_COUNT}} total):

{{FOR EACH THEOREM:}}
- {{ID}} --- {{NAME}} (llog line ~{{LINE}}, label ``{{LABEL}}``)

STRUCTURAL PROPERTIES ({{SP_COUNT}} total, may be 0):

{{FOR EACH SP:}}
- {{ID}} --- {{NAME}} (llog line ~{{LINE}}, label ``{{LABEL}}``
  or "no label" if none exists)

**Extraction rules:**

1. Copy each axiom/theorem/property VERBATIM from the llog
   source. Do not paraphrase, simplify, reword, or "improve"
   any statement. The formal ``.. math::`` blocks must be
   character-for-character identical to the llog source. The
   prose descriptions must be word-for-word identical.

2. Preserve all existing ``.. _{{model}}-*:`` labels exactly
   as they appear in the llog. These labels may already be
   referenced by content files across the site. Changing a
   label breaks links.

3. Add labels to any statements that lack them, following the
   naming convention established by the existing labels
   (e.g., ``{{model}}-sp1``, ``{{model}}-sp2``).

4. Organize into files:

   - ``axioms.rst`` --- all axioms, grouped by logical
     category (e.g., prerequisites then stage axioms, or
     by axiom group as defined in the model)
   - ``theorems.rst`` --- all theorems + structural properties
   - ``models.rst`` --- submodel architecture table (every
     model has submodels; document them including reserved
     slots)
   - ``logics.rst`` --- all formal disciplines used, with
     links to the WisdomBase sheets and Iron Maiden test
     coverage. "Standard logics" is never acceptable ---
     spell out exactly which logics and why.
   - ``aa.rst`` --- Any Aims tracking (POST convention).
     Sections: Operational Aims (structural tasks,
     directive fixes, label cleanup) and Adversarial Aims
     (untested theorems, formalization gaps, attack
     surfaces). Populate with all open issues discovered
     during SEED.
   - ``llog.rst`` --- local pointer to relevant llogs in
     HELL. Links to the FORGE session(s) that produced
     the model and the PROMY session(s) that extracted it.

5. Each file gets a proper RST title and uses a consistent
   heading hierarchy: ``=`` for the file title, ``-`` for
   section groups, ``~`` for individual axiom/theorem entries.

6. Include StayC verdicts if present in the llog as a summary
   table at the end of each file.

7. Add a provenance note at the top of each file:
   "Extracted from FORGE session {{SESSION_ID}} by
   PROMY:SEED on {{DATE}}. See {{LLOG_DOC_LINK}}."

8. Add a ``vvnow`` annotation near the top of each file that
   carries formal content (axioms.rst, theorems.rst,
   predicates.rst, symbols.rst). The format is an RST comment
   with NO colon::

     .. vvnow dv_{{AUDITOR}}_{{STAYC}}_{{DATE}}

   CRITICAL: NO colon after ``vvnow``. ``.. vvnow value`` is a
   valid RST comment (invisible in output, grep-able for tooling).
   ``.. vvnow:: value`` (double colon) creates an unknown Sphinx
   directive and causes build warnings. ``.. vvnow: value``
   (single colon) also works but adds unnecessary punctuation.

9. Write the PROMY llog to
   ``hell/llog/promy/promy_{{model}}_{{date}}.rst``
   recording: the full prompt, the inventory, the
   checking checklist results, and any discrepancies.
   Mark as ``:orphan:``.

**Checking checklist (MUST complete before accepting):**

- [ ] Count axioms in output: exactly {{AXIOM_COUNT}}
- [ ] Count theorems in output: exactly {{THEOREM_COUNT}}
- [ ] Count structural properties: exactly {{SP_COUNT}}
- [ ] Total statements: exactly {{TOTAL_COUNT}}
- [ ] Every ``.. math::`` block is character-identical to
      llog source
- [ ] Every existing label is character-identical to llog
- [ ] No labels were added beyond those in the inventory
      (except for statements that lacked labels)
- [ ] No labels were removed or renamed
- [ ] No prose was reworded, simplified, or "improved"
- [ ] ``make html`` produces zero new warnings from these
      files
- [ ] All existing ``:ref:`` cross-references from other
      files still resolve
- [ ] Zero duplicate label warnings

**What NOT to do:**

- Do NOT rewrite or improve the mathematical notation
- Do NOT add explanatory text not present in the source
- Do NOT reorganize internal order beyond the grouping
  specified above
- Do NOT merge derivation sketches into theorem statements
- Do NOT touch the llog source file (append-only)

After extraction, report:
1. Exact count of statements extracted per file
2. Any discrepancies found between inventory and llog content
3. The checking checklist with all items checked or
   explained

How to Prepare the Inventory#

Before running the prompt, you must build the inventory. This is the most important preparation step — getting the inventory wrong means extracting the wrong content.

  1. Find all labels in the llog:

    grep '^\.\. _{{model}}-' {{LLOG_PATH}}

    This gives you every labeled statement and its line number.

  2. Count by type:

    • Axiom labels typically match {{model}}-m*-ax* or {{model}}-m*

    • Theorem labels typically match {{model}}-th*

    • Structural property labels typically match {{model}}-sp*

    • Some statements may lack labels (note these for step 3 in the extraction rules)

  3. Read each labeled section to get the name, check the math block exists, and note the approximate line number.

  4. Cross-check with StayC tables in the llog — these often list all statements and can catch ones you missed.

  5. Check for late additions. Theorems added in later TEMPER rounds (e.g., th6, th7 in e7He) may be hundreds or thousands of lines after the initial statement block. Search for NEW THEOREM or NEW AXIOM patterns.

Lessons from the First Run (e7He)#

  1. Late theorems are easy to miss. th6 and th7 were defined ~3000 lines after th1–th5 in the e7He llog, in a different TEMPER round. The inventory step MUST search the entire llog, not just the initial STRIKE block.

  2. Structural properties often lack labels. sp1–sp3 had no .. _e7he-sp*: labels in the llog. The extraction added them. This is the one case where new labels are created.

  3. Duplicate labels are a risk but not a problem. The same labels exist in both the llog and the extracted files. Sphinx silently resolves to one (typically the first found). This is acceptable during the transition period. The labels in the llog should be removed during the future llog migration (AA-LLogMigration-a1).

  4. Derivation sketches belong with the theorem. th6 and th7 had extensive derivation sketches, case analyses, and VVN annotations. All of this was extracted verbatim. Do not separate the derivation from the theorem statement.

  5. The checking checklist catches errors. Do not skip it. The count check alone caught a potential off-by-one in development.