Code review fixes + 13 middot added to spec

Zerikah fail-safe: empty offerings rejected, not processed (BUILD_KORBAN §5).
Halt monitor hardened: trap_exit, priority max, EXIT handler (Architecture spec).
13 Rules of Rabbi Yishmael added to Architecture §3.4 as Prolog inference predicates —
the engine reasons WITH Torah's hermeneutic methods, not just about their products.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

specs/shorashim_architecture.md

@@ -667,6 +667,106 @@ resolve(Case, Resolution) :-
 %% If no resolution is possible
 resolve(_, teiku).
 
+%% === 13 RULES OF RABBI YISHMAEL (Hermeneutic Inference) ===
+%%
+%% The Torah's own interpretive methods. The engine must reason WITH
+%% these rules, not merely reason about mitzvot derived from them.
+%% Each middah is a Prolog inference predicate that derives new
+%% propositions from existing Torah facts.
+
+%% 1. Kal va'chomer — a fortiori (minor to major)
+%% If a lenient case has restriction X, a stricter case certainly does.
+kal_vachomer(Lenient, Strict, Property) :-
+    has_property(Lenient, Property),
+    stricter_than(Strict, Lenient).
+
+%% 2. Gezerah shavah — verbal analogy
+%% Shared language between two passages implies shared law.
+gezerah_shavah(VerseA, VerseB, SharedLaw) :-
+    verse_contains_word(VerseA, Word),
+    verse_contains_word(VerseB, Word),
+    has_law(VerseA, SharedLaw).
+
+%% 3. Binyan av mi'katuv echad — prototype from one verse
+%% A law stated in one case applies to all similar cases.
+binyan_av(SourceVerse, TargetCase, Law) :-
+    has_law(SourceVerse, Law),
+    similar_case(SourceVerse, TargetCase),
+    \+ explicitly_excluded(TargetCase, Law).
+
+%% 4. Binyan av mi'shnei ketuvim — prototype from two verses
+%% A law common to two cases applies to all similar cases.
+binyan_av_two(VerseA, VerseB, TargetCase, Law) :-
+    has_law(VerseA, Law),
+    has_law(VerseB, Law),
+    similar_case(VerseA, TargetCase),
+    \+ explicitly_excluded(TargetCase, Law).
+
+%% 5. Klal u'frat — general and particular
+%% A general statement followed by a particular limits to the particular.
+klal_ufrat(General, Particular, Scope) :-
+    follows(General, Particular),
+    Scope = limited_to(Particular).
+
+%% 6. Frat u'klal — particular and general
+%% A particular followed by a general expands to the general.
+frat_uklal(Particular, General, Scope) :-
+    follows(Particular, General),
+    Scope = expanded_to(General).
+
+%% 7. Klal u'frat u'klal — general, particular, general
+%% Scope is determined by similarity to the particular.
+klal_frat_klal(General1, Particular, General2, Scope) :-
+    follows(General1, Particular),
+    follows(Particular, General2),
+    Scope = similar_to(Particular).
+
+%% 8. Klal she'hu tzarikh li'frat, u'frat she'hu tzarikh li'klal
+%% General needing particular, particular needing general — mutual dependency.
+klal_tzarikh_frat(General, Particular, Meaning) :-
+    requires_specification(General, Particular),
+    requires_generalization(Particular, General),
+    Meaning = mutual_definition(General, Particular).
+
+%% 9. Davar she'hayah bi'khlal v'yatza min ha'klal l'lamed
+%% Something included in a general rule that is singled out teaches
+%% about the general rule, not only about itself.
+davar_yatza_l_lamed(General, Exception, Teaching) :-
+    member_of(Exception, General),
+    singled_out(Exception, General),
+    Teaching = teaches_about(General, Exception).
+
+%% 10. Davar she'hayah bi'khlal v'yatza lit'on to'an acher
+%% Something singled out to teach a new matter — applies only to itself.
+davar_yatza_toan_acher(General, Exception, NewMatter) :-
+    member_of(Exception, General),
+    singled_out_for(Exception, NewMatter),
+    applies_only_to(NewMatter, Exception).
+
+%% 11. Davar she'hayah bi'khlal v'yatza la'don ba'davar he'chadash
+%% Something singled out for a completely new category — cannot return
+%% to the general rule unless Scripture explicitly returns it.
+davar_yatza_chadash(General, Exception, NewCategory) :-
+    member_of(Exception, General),
+    new_category(Exception, NewCategory),
+    \+ explicitly_returned(Exception, General).
+
+%% 12. Davar ha'lamed me'inyano, v'davar ha'lamed mi'sofo
+%% Meaning derived from context, meaning derived from conclusion.
+davar_lamed_inyan(Passage, ContextMeaning) :-
+    surrounding_context(Passage, Context),
+    implies(Context, ContextMeaning).
+davar_lamed_sofo(Passage, ConclusionMeaning) :-
+    conclusion_of(Passage, Conclusion),
+    implies(Conclusion, ConclusionMeaning).
+
+%% 13. Shnei ketuvim ha'makhchishim zeh et zeh
+%% Two verses that contradict — resolved by a third verse.
+shnei_ketuvim(VerseA, VerseB, VerseC, Resolution) :-
+    contradicts(VerseA, VerseB),
+    resolves_contradiction(VerseC, VerseA, VerseB),
+    Resolution = harmonized(VerseA, VerseB, VerseC).
+
 %% === HALT CONDITIONS ===
 
 %% Check for avodah zarah — misattributed authority
@@ -700,6 +800,15 @@ talmudic_engine/
 │   │   ├── challenge.pl       -- Kushya generation
 │   │   ├── resolve.pl         -- Dialectical resolution
 │   │   └── teiku.pl           -- Unresolved tension handling
+│   ├── middot/
+│   │   ├── middot.pl          -- 13 Rules of Rabbi Yishmael as inference predicates
+│   │   ├── kal_vachomer.pl    -- Rule 1: a fortiori (minor to major)
+│   │   ├── gezerah_shavah.pl  -- Rule 2: verbal analogy
+│   │   ├── binyan_av.pl       -- Rules 3-4: prototype from one/two verses
+│   │   ├── klal_ufrat.pl      -- Rules 5-8: general/particular interactions
+│   │   ├── davar_yatza.pl     -- Rules 9-11: exception teaching rules
+│   │   ├── lamed_inyan.pl     -- Rule 12: meaning from context/conclusion
+│   │   └── shnei_ketuvim.pl   -- Rule 13: contradicting verses resolved by third
 │   ├── halt/
 │   │   ├── avodah_zarah.pl    -- Idolatry detection
 │   │   ├── shfichut_damim.pl  -- Destruction detection