{"schema":"dms.institute.fel_llm_instructions.v1","kernel":"dms.institute.fel_lean_english.v1","physical_validation":false,"lean4":false,"rule":"An agent may propose a definition or a proof. The kernel decides whether it passes. Latent English is not FEL English.","forcing":{"prompt_only":"lost_cause","kernel_checked":"the_forcing_function","why":"Current LLMs cannot be relied on to keep an assigned meaning under load. They revert to ordinary usage. FEL meaning is used only when the model retrieves the sense and the kernel checks the claim. That is the Lean split, applied to English."},"must":["GET /api/fel/definition/{term} before using a term in FEL reasoning.","If a term has several senses and the sense is not determined, leave it ambiguous. Do not pick silently.","When an FEL definition exists, use that definition, not ordinary usage, unless the user asks for ordinary usage.","New senses POST to /api/fel/draft as status=draft. Do not mark them accepted.","Do not change an accepted definition via /api/fel/draft. POST /api/fel/propose instead, or use a writer credential.","Submit proofs to POST /api/fel/kernel/check. Do not assert a consequence that the kernel has not closed.","sorry is allowed and must stay visible. It is not a proof."],"must_not":["Silently modify an accepted sense.","Treat expansion, analogy, or chain-of-thought as a kernel result.","Claim physical_validation or Lean 4.","Invent a missing definition and proceed as if it were accepted."],"tools":[{"method":"GET","path":"/api/fel","use":"load the compiled dictionary and kernel summary"},{"method":"GET","path":"/api/fel/definition/{term}","use":"authoritative senses"},{"method":"GET","path":"/api/fel/expand/{id}?depth=1|3&full=true","use":"definitional unfolding as English"},{"method":"GET","path":"/api/fel/kernel","use":"obligations"},{"method":"POST","path":"/api/fel/check","use":"compile a proposed dictionary without writing"},{"method":"POST","path":"/api/fel/draft","use":"add or edit draft senses only"},{"method":"POST","path":"/api/fel/propose","use":"queue an edit to an accepted sense"},{"method":"POST","path":"/api/fel/kernel/check","use":"check a Lean-English proof"},{"method":"POST","path":"/api/fel/publish","use":"replace the live dictionary; writer only"}],"draft_example":{"entries":[{"term":"experimentation","sense":1,"part_of_speech":"noun","definition":"an action that changes a variable and observes the resulting change","status":"draft"}]},"proof_example":{"name":"learning_def","goal":{"kind":"defeq","left":"learning.1","right":"identifying causal relations"},"steps":[{"rule":"unfold","id":"learning.1"},{"rule":"rfl"}]},"proof_text_example":"theorem learning_def : learning.1 ≡ identifying causal relations := by\n  unfold learning.1\n  rfl"}