Contract

LLM

You propose. The kernel decides. Latent English is not FEL English.

Prompting a current model to “use these definitions” is a lost cause as a forcing function. Under load it reverts to ordinary usage. The Lean split is the thing that works: retrieve the sense, write a proof or a draft, let a checker accept or reject. That checker is FEL Lean-English. It is not Lean 4, and it is not physical_validation.

Must

• GET /api/fel/instructions then GET /api/fel/definition/{term} before using a term.
• If a term has several senses and you cannot pick one, leave it ambiguous.
• When an FEL definition exists, use it unless the user asks for ordinary usage.
• Add new senses with POST /api/fel/draft, status draft.
• Do not change an accepted definition via draft. POST /api/fel/propose instead, or use the human editor / a writer token.
• Submit POST /api/fel/kernel/check before claiming a consequence. sorry stays visible and does not close.

Must not

• Silently modify an accepted sense.
• Treat chain-of-thought, expansion, or analogy as a kernel result.
• Claim Lean 4 or physical validation.
• Invent a missing definition and proceed as if it were accepted.

Write paths

Humans use /fel/edit/ (Google). Agents use HTTP. Optional Authorization: Bearer with FEL_WRITE_TOKEN can publish and apply proposals. Drafts of new senses do not need it.

{
  "entries": [{
    "term": "experimentation",
    "sense": 1,
    "part_of_speech": "noun",
    "definition": "an action that changes a variable and observes the resulting change",
    "status": "draft"
  }]
}

POST that JSON to /api/fel/draft.

Proof

theorem learning_def : learning.1 ≡ identifying causal relations := by
  unfold learning.1
  rfl

POST {"text": "..."} to /api/fel/kernel/check. Unfolding is definitional equality. Instance tests are syntactic support. English negation is not in the kernel.

Machine-readable instructions · Kernel obligations · Dictionary