Get a canonical TRIZ engineering parameter (1-39). Omit id to list all 39. Entries include alternate labels, interpretation guidance and nearby categories to distinguish where recorded. These historical matrix categories are separate from typed domain quantities.

Get a canonical TRIZ inventive principle (1-40). Omit id to list all 40. Look up principle numbers instead of recalling them from memory.

Look up the canonical contradiction matrix for an improving and worsening engineering parameter. Blank and diagonal cells fail closed; never guess a recommendation.

Multi-parameter contradiction lookup: every (improving x worsening) matrix cell with the principles aggregated by how many cells recommend each (ties broken by mean position). Use when a conflict involves several parameters on either side; per-cell detail is returned so nothing is hidden. All-blank or diagonal-only results fail closed like triz_matrix.

Look up a contradiction-matrix cell and expand its recommended principles and both engineering parameters. Fails closed on blank cells.

List the domain-neutral TRIZ tool catalog, optionally restricted to problem analysis, task modeling, or solution synthesis.

List installed universal and domain knowledge packs, provenance, review status, explicit quantity parameters, shared interface families, multiport/stateful models, directed boundary observations and definition counts. Taxonomy reports selected typing roles, field groups and advisory retain/split assessments of whole named functions; assessment groups can cover more than the selected typing. Fields supply no response contract and counts do not measure independent physical laws. Uses all packs by default. A domain filter includes universal definitions; counts and taxonomy describe all installed packs. These parameters are separate from the canonical 39 matrix parameters; domain mappings never invoke the matrix automatically.

Search effects from all installed knowledge packs by text or exact typed input/output quantity, field and output SI dimension. Filter kind for modeling role, form for definition storage, or assessment for named functions to retain as responses/compounds or split into distinct models. Assessments describe the whole named function; the selected typing may cover only one facet. Unregistered facets are advisory and never become generators or executable recipes. Optional domain filtering includes universal effects; pack and category filters are exact. Results retain named cases, sources, limitations and review status. Composite recipes expose their steps and expand through triz_effect_setup; chain search uses their constituents.

Assign effort/flow causality on declared energy subsystems by bounded propagation and search; report derivative causality and direct algebraic dependency cycles, and export constitutive equation structure. No numeric simulation.

Solve finite declared maintenance actions by exact rational average-cost equations under explicit per-dimension or weighted objectives. Include declared per-state holding costs once per decision step. Return stationary policy, gain, bias, occupancy and availability; box-local availability uses the request acceptable list, not global states. Undeclared probabilities return T3 ranges; unsupported multichain cases and caps are undecided.

Search bounded typed effect chains from declared resources to a required quantity; every wiring diagram passes checkModel. Named configurations are conditional summaries marked requiresExpansion; use triz_effect_setup to expand their model nodes and context inputs. Ranking: length, conditions met, field changes, declaration order. Capped search is undecided. Physical sufficiency is not claimed.

Build a composable function model from registered effect or recipe ids using explicit quantity, SI and carrier-layer declarations. Serial recipes expand to their constituent effects; named configurations expand to actual model nodes and expose context inputs. Use node_declarations[expanded-step/node] for constituent implementations and context_values[expanded-step/input] alongside finite boundary availability. Ordinary declarations correspond to expanded effect steps. Optional parameter bindings supply finite values/levels; boundary availability/acceptance and per-effect behavior, state/initial/transition and resource rows remain caller declarations. Return a checked rewrite and provenance. Missing conditions remain hypotheses.

Insert a selected typed effect chain between existing output/input ports, with explicit replacement of an existing supplier. Return the checked model, added carriers, replayable rewrite and effect citations/conditions. Behavior and resource rows are only caller declarations; physical sufficiency is not inferred.

Return the general identity/fanout catalogue (default), or source:knowledge for registered multiport and stateful model templates. Explicit parameter bindings and implementation declarations configure finite behavior and dynamics; no behavior is inferred from names. effects selects named realizations and their required output observations; mappings explicitly selects directed refinement observations, never unit casts or global aliases. Pass the returned catalogue to triz_component_search.catalogues for bounded configuration discovery. Conditions remain visible hypotheses.

Automatically construct components, chains and multi-input networks from finite typed and reusable domain-independent catalogues, including general, with explicit type bindings. Search component choices and wiring up to instance/component/work bounds; optional whole-model contracts check finite behavior, acceptable values, harms and resources. Complete absence applies only to the declared bounded catalogue; capped search is undecided.

Route a problem stage and optional observable signals to candidate TRIZ tools. Routing is deterministic and returns only tools registered for that stage.

Build a typed function model from an interaction table: components with stable ids, names and roles, and subject/action/object interactions with explicit carrier descriptors and polarities. Generates readable, stable ports and wire ids: each interaction gets its own input port on its object, in:<carrier>:<subject>:<action>, so no input port is fed by two functions (no fan-in, no extensive-fan-in); each subject gets one output port per carrier it sends, out:<carrier>, shared by its functions on that carrier (fan-out: one shared level when intensive, the sum of the demands when extensive); each function is the wire wire:<subject>:<action>:<object>:<carrier>. Each part is percent-escaped (':' as %3A, '%' as %25), so distinct tuples never share an id. Validates the result, runs lints, and returns a bounded completeness report of unrecorded component pairs, isolation and product reach. Ratings and behavior are never inferred. Optional flows reference component and carrier ids from the table.

Substitute one box's declared inner model into its parent through its checked input/output interface. Returns a typed model and fresh box, wire and flow id maps. Preserves inner box costs, feasibility, states and transitions, and standalone inner flows. Parent flow occurrences require explicit routes and checked boundary connections; media need explicit mappings. Inner budgets, weights and contradictions require opt-in global-intersection, global-merge and append-renamed policies. Product-identity changes fail closed. Expand nested boxes one at a time before requesting flat behavior, dynamics or resource verdicts. triz_nine_windows reads a selected box's inner model as its subsystem view.

Check a TRIZ function model written as a typed wiring diagram (boxes with typed ports, wires carrying one carrier and a polarity) and analyse it: harm loops (closed loops containing a harmful or excessive function, with witness cycles), an ideality profile per resource dimension (never summed; a scalar ratio only with explicit weights), separation checks for embedded physical contradictions, and, given compare_to, a componentwise baseline-vs-concept comparison plus an isomorphism check: whether the two models share a wiring shape ignoring every id and label (a bijection preserving roles, port sides, shared carriers, wiring, ratings, and costs; decided:false if the bounded search runs out). With mpv_weights (and compare_to), comparison.mpv compares the two models over the main parameters of value only: the named cost dimensions or 'harmful', componentwise and by the explicit weighted sum, listing the other axes on which they differ; a lost deliverable still decides, and no weight is ever filled in. Each verdict cites the theorem in theory/CategoricalTriz.lean it relies on (basis). Any dangling, mis-directed, or mistyped wire, or an invalid embedded contradiction, fails closed with ok:false. Harm loops and separation read the outer wiring and the model's own contradictions only: when boxes declare an inner model, incompleteHierarchy lists them, the note says their inner loops and contradictions are not analysed, and the isomorphism check carries incompleteHierarchy: true; run triz_expand_hierarchy on each first. Loops are hypotheses about mechanism to substantiate, not findings.

Flow analysis (router entry 16) over the model's declared flows: each an ordered path of the boxes a carrier passes through, in series, which functions do not record (two valves in series both act on the water, not on each other). Per flow: its steps (consecutive boxes, with the functions of the flow's carrier between them; declaredOnly counts the steps no function joins); bottleneck candidates (the performer of an insufficient, excessive, or harmful function that carries the flow's carrier and touches the path: a resistance-like output on the flow, at its position); accumulation candidates (a box where the steps of every flow of the carrier converge, with at least two predecessors and fewer successors, or a last box inside the engineered system, role tool or mediator, that no flow of the carrier continues from); leak candidates (a function on the carrier from a box on the path to an environment or supersystem box off it); loops (a box that recurs on the path, with the cycle between occurrences); and the harm loops that meet the path. Every item is a structural candidate to substantiate, not a finding. Boxes consecutive on a flow are adjacent for triz_transform merge. A model that fails the type-check, flows included, fails closed.

Screen a trimming of one or more boxes by the TRIZ trimming rules: A (object trimmed too, function no longer needed), B (the object performs the function itself), C (another remaining box or supersystem resource has an output of the same carrier). Returns per-function absorbers, orphaned functions that block the trim, harms and costs removed, and one trimming problem per absorber. A carrier match is a necessary condition only; every absorber is a hypothesis to solve and substantiate.

Decide whether a physical contradiction's demands can be met piecewise over a finite space x time x condition x direction x level base (the MATRIZ separation types). Each demand lists admissible values and the cells where it applies (omitted axis = whole axis). Returns per-pair status (compatible: not a physical contradiction; separated: the separating axes; irreducible: overlap on every axis) and the conflict cells where no value satisfies every active demand. With along, also returns the parameter as a function of that axis alone: the admissible values per cell and whether it must change along the axis (with 'time', the checkable part of Principle 15, Dynamics). Each separated pair also gets suggestions, hints and not verdicts: per separating axis, the operations that could build the piecewise system (space: triz_transform segment or take_out; time: standby, or triz_dynamics separation with timed demands, Principle 15; condition: rerate, or a rewrite that changes the field, Principle 28; level: triz_nine_windows, the system operator or its subsystem restriction; direction: segment by port direction), each with the demands' cells on that axis and the looked-up text of the principle it follows.

Export a function model that type-checks: 'dot' gives Graphviz DOT (each box a table: name and «role» in a role-coloured header, input ports left and output ports right with their carriers, open ports in italics; functions as edges between ports, harmful red, insufficient dashed, excessive bold; flows dotted blue; a legend of what occurs; render with dot -Tsvg), 'mermaid' gives a Mermaid flowchart that GitHub, GitLab, and many chat clients render without tools (Mermaid has no ports, so each edge names its out port, in port, and carrier), 'svg' gives a self-contained SVG picture with dot's conventions, laid out by ELK with orthogonal edges, for when Graphviz is not at hand (stdio server only: it needs the optional elkjs package; the hosted server answers ok:false with format-unavailable), 'hypergraph' gives an open hypergraph (ports as carrier-typed vertices, boxes and functions as hyperedges, unwired ports as the interface). A model that fails the type-check is not exported (ok:false with the errors).

Apply one typed model transformation and return the new model. Principle constructions: segment (1: divide a box into parts whose ports partition its ports), take_out (2: separate the ports touching a harmful or excessive function, or isolate the part carrying all useful functions), merge (5: collapse adjacent or identical boxes into one; boxes consecutive on a declared flow are adjacent), standby (11: add an unwired typed absorber for a box's functions), reverse (13: swap a function's performer and object), rerate (16: rate a useful function insufficient or excessive; 23: change the level of a function on a cycle), retarget (22: a harmful function's source feeds a useful function), feedback (23: add a function that closes a loop), interpose (24: route a function through a new mediator box), cheap_copy (26, 27: replace a box by a cheaper copy with the same ports). Also trim (perform a typed-feasible trim, re-attaching each kept function to an absorber; rule B is Principle 25, one absorber for everything is Principle 6) and rewrite (delete and add boxes and wires; no remaining wire may touch a deleted box). Every result type-checks or the call fails closed with ok:false. When the segmented box declares behaviour, segment (and take_out) reports behaviourallyIndependent: whether the box's relation is the product of its projections onto the parts; if so each part gets its projection, else no part gets behaviour and each coupled part is named with a witness: two rows whose mix is not a row. It also suggests the finest partition of the box's ports over which its relation is a product (behavior.finest: parts; cut, the suggested blocks the given parts cut, empty iff the split holds; splitsFurther, when nothing is cut, the parts that hold several blocks; decided:false past the cap). interpose's mediator may declare behavior (rows, or 'identity'). A transformation is a structural move, not evidence that it solves the problem: model the result and compare it with triz_function_model compare_to, or with triz_behavior compare_to when behaviour is declared, passing the boxMap that segment, take_out, or cheap_copy returns as box_map. merge renames the merged ports to '.', so no box_map recovers a merged product box's deliverables: they read as lost and regained. reverse returns undo, a rewrite that restores the original model, added ports included.

Double-pushout rewriting with rules as data. A rule is a span L ← K → R of patterns over the function-model schema (boxes with ports typed by carrier variables, and wires); pass it as rule, or name a built-in evolution-line rule with rule_id: 'mono-bi' (transition to supersystem, mono → bi; apply again for poly), 'feedback' (increasing controllability, self-adjusting with feedback; bind its carrier variable 's' with carriers), or 'working-field' (changing the working field: the matched function re-made on another carrier; bind 'd' with carriers to a carrier other than the matched one; the result's fieldChanges records both carriers' layer and dimension). Each built-in rule cites the evolution-trends.md line it encodes. rule_id 'uneven-development' is a detector, not a rewrite, and takes only the model: the lagging subsystem, a box of the largest harm-loop region that is also on a binding feasibility dimension or limits a deliverable (feasibility finds it unprovidable, or it performs an insufficient function on a product); verdict lagging, none, or undecided (no harm loop, or feasibility undecided). Without match: lists every injective match of L (seed it with at), each verified as a typed homomorphism and marked applicable when the no-identification and no-dangling conditions hold (a deleted box may not lie on a declared flow) and the rule's distinct carrier variables bind different carriers; decided:false if the step budget runs out, complete:false past limit. A rule's forbid holds negative application conditions (Habel–Pennemann): each pattern extends left by id, and a match that extends to an occurrence of one — including any elements the pattern adds — is not applicable; a condition its own step budget cannot decide also refuses the application. With match (a listed match, or your own mapping): checks the match, these conditions, and that a kept box keeps the ports its declared rows name (every port for behavior and transition; the named ports for feasibility), then deletes the image of L \ K, glues R \ K under fresh ids, and returns the new model, which type-checks or the call fails closed; deliverableKeysChanged says a deliverable moved to another port or carrier. A rule application is a structural move, not evidence that it helps: compare the result with triz_function_model compare_to.

Compose declared box behaviour (carrier values, box behavior rows) into the model's external relation: boundary inputs (unwired input ports) to deliverables (product input ports fed by a non-harmful function). The default upstream scope composes boxes that can reach a deliverable and explicitly assumes omitted boxes accept everything; scope whole composes every box, including downstream and disconnected constraints. full_relation returns all rows within the search cap. Feedback loops compose by the relational trace, so every consistent steady state counts, and the steady states are listed. factorisations lists each composed box whose relation is the product of its projections onto two or more groups of ports, with the finest groups, in box order (decided:false past a per-box cap): segment it into them, or unions of them, and each part keeps its projection. The hint describes the declared rows, not a physical split, and changes no verdict. This is steady-state semantics, not dynamics. With compare_to, decide whether the model (a concept, e.g. a triz_transform result) has the baseline's input→deliverable relation; pass segment's or take_out's boxMap as box_map. trim is shorthand: perform the trim as triz_transform does and compare the result with the model. Verdict preserved; changed (a lost deliverable, or a counterexample input with the differing outputs and which relation contains which); or undecided (reason missing-behavior: the boxes that can reach a deliverable and declare no behaviour; reason no-steady-state: neither model has a steady state at any input, so equal empty relations say nothing). With joint_boxes and weakest_spec, select every composed box without behavior and compute one coupled residual over their combined ports. The joint rows are a single relation: independentSafe checks whether independently declaring their per-box projections stays inside the target, factorizes checks whether their product equals the joint relation, and a counterexample explains unsafe coupling. The exact search is bounded by max_states; row_costs are unsupported in this mode. With weakest_spec (and compare_to or trim), give the weakest box specification (residual in Rel) for the one box of the concept that can reach a deliverable and declares no behaviour, against the same target: spec, every row of that box whose composite stays inside the target, with preserves:true when declaring it gives exactly the target (any behaviour that does is contained in it); impossible, when the spec's composite misses part of the target (an uncovered input is given; no behaviour of that box gives the target, and the empty relation, which always stays inside, is never read as preserving) or a deliverable is lost; undecided for three or more unknown boxes when joint_boxes is omitted (several-holes), missing baseline behaviour, an empty target, or past the cap (state-cap). When the box to specify declares producible rows (what it can physically produce), the spec is the residual cut down to them: spec when that still covers the target (producible.infeasible lists the residual rows left out); impossible with reason infeasible when the residual covers the target but its producible rows do not, with requiredInfeasible giving, per missing target pair, the residual rows that deliver it, none producible (every relation that gives the target contains one of each); impossible with reason not-covered when the residual itself does not cover. With exactly two boxes without behaviour (boxes), a pair of relations stays inside the target iff every pair of rows, one of each, does, and the maximal such pairs are the formal concepts of the safe row pairs: spec lists those whose composite covers the target (specs, each declared and re-checked to give exactly the target; every pair that gives the target lies inside one), with weakest:true when there is one and weakest:false when several are incomparable; impossible (not-covered) when none covers, with each maximal pair's uncovered input (pairs); undecided (concept-cap) past the cap on concepts. Producible rows cut each box first; impossible with reason infeasible then means some pair over all rows (wouldGive) would give the target. Fails closed on ill-typed behaviour, an ambiguous or mismatched box_map, inputs whose values differ between the models, and past the state cap. With row_costs in the one-hole mode, cheapestExtension gives an exact least-cost set of safe nonproducible rows to add, using the complete target relation and explicit integer costs, or reports an undecided capped search; it is not-applicable (target-not-covered-by-residual) when the residual itself misses the target, and row_costs fail with invalid-row-costs wherever no one-box residual is computed; the Boolean verdict is unchanged. The verdict holds for the relations as declared; substantiating them, the absorber's or mediator's first, is outside the kernel.

Rank candidate concepts that declare behaviour by the operating situations they admit (references/weakness.md). A situation is a valuation of the concepts' boundary inputs (unwired input ports, matched by box and port id) over their carriers' declared values: the declared input space is weakness.md's list of operating situations. A concept admits a situation when it has a steady state there and every deliverable output there is acceptable (acceptable: per deliverable port, or per carrier for all its deliverables, the values that are, listed or derived from a threshold at_least/below that is a declared level of the carrier; required for every deliverable; derived sets are listed under acceptable in the result). Give each operating condition the same box and port id in every concept (e.g. an environment box with an unwired input); readByOne lists the inputs only one concept reads. Ranked by set inclusion: weakest (admits everything any other admits), maximal, and every pair as equal, first-weaker, second-weaker, or incomparable, with a situation only one admits each way. The admitted count is a secondary figure: it depends on how finely carrier values are declared. priors gives a real prior over the situations (weakness.md: a real prior beats the uniform assumption): per situation input (box and port), or per carrier, a nonnegative weight per declared value (unlisted inputs and values count 1; 0 rules a value out); each concept carries the total prior mass of what it admits (weightedAdmitted, ranked in byWeight), and no inclusion ever moves under weights. joint_prior is the alternative for correlated operating conditions: an explicit complete joint table, a weight for every situation (zero allowed), with no independence assumption; it reports jointAdmittedWeight and jointAdmittedProbability per concept, ranked in byJointPrior, separately from inclusion and counts. Give priors or joint_prior, not both. Fails closed when the concepts deliver different ports, an input several read ranges over different values, or acceptable misses a deliverable or names an undeclared value, or a prior is malformed; undecided on missing behaviour or past the state cap. Filter concepts for adequacy first; for safety, integrity, or authorisation decisions admitting more is the wrong direction.

Rank finite candidate designs jointly over declared metric vectors: which candidates no other matches on every metric and beats on one (the frontier), which are dominated and by whom, and which frontier pairs trade one metric against another. Compare what the kernel already produced — minimal resource vectors from triz_feasibility, lifecycle gain and availability from triz_lifecycle, component counts from triz_synthesize or triz_component_search, declared costs — or any finite comparable numbers. Per-metric direction: minimize (default) or maximize. Incomparable candidates are reported as trade-offs, never resolved (pareto_not_total: the componentwise order is not total), and weights, when given, only order the listing: no weight is ever filled in. The compared numbers are declarations, not measurements this tool takes.

Costed transition rows add exact per-dimension cycle mean ranges, rational potential bounds and rechecked witnesses on closed components; max_cost_work caps these. Bounded dynamics of a function model whose boxes declare state, initial, and transition rows (state, inputs) → (next state, outputs): each such box is a nondeterministic Mealy machine (a lens with a residual is one, with the residual as state); boxes with behavior are stateless. Boxes compose synchronously along the wiring: wires are instantaneous, memory lives only in declared state, and a loop through stateless boxes resolves within a step as in triz_behavior. From the initial states, over the boundary inputs you allow at each time (default: every value), every run is explored breadth first up to horizon steps; the result lists the reachable states, the fixed points among them, and the runs that block (a state with no row for its inputs). unsafe decides escalation: reachable (with a shortest trace), unreachable (the reachable set stopped growing, so at no horizon), or unreachable-within-horizon. safe decides invariance: violated (shortest trace), invariant, or invariant-within-horizon. Without inputs the configurations are finite, so each verdict also carries unbounded, decided at every horizon by continuing the search past the horizon within the same state cap: reachable or violated (with the time and, past the horizon, a shortest trace), unreachable or invariant (with completeAfter), or undecided (cap-exceeded past the horizon, or blocked); the bounded verdict beside it is unchanged. A blocked state meets a target by its state conditions; a port condition there leaves the verdict undecided (reason blocked), never safe. separation takes two to four demands, each a target set with a time window, and decides whether one run visits each within its window (separation in time along a trajectory, Principle 15): realizable with a witness trace, unrealizable (a demand never met, or no single run meets them all), or undecided (a blocked run might meet them all). Without inputs, loops classifies the closed components (no step leaves them) of the reachable graph of the global states of boxes that declare transition, explored without a horizon up to the cap, from the initial states and every state meeting safe's state conditions: bistable (fixed points in two or more closed components), trapped (a closed component every configuration of which meets unsafe: an absorbing trap, with a shortest trace into it), recurrent (a closed component that meets unsafe and also holds a safe configuration: the run can recover but never leaves it, with a shortest trace into it and the safe configuration), oscillating (a cycle and no fixed point, with its period and one cycle); each closed component reports unsafe (it meets the set) and allUnsafe (it lies inside it); classes can coexist, and 'none' means no closed component was found within the cap. Behavior rows are never read as transitions. Every trace is re-checked against the declared rows. Fails closed on ill-typed rows, unknown targets, and past the state cap. Verdicts hold for the rows as declared; continuous dynamics, convergence rates, and control are not modelled.

Monotone co-design feasibility (Censi 2015) from declared box feasibility rows: each row provides a level per output port against the levels it requires per input port and an operating cost, read monotonically (providing less never needs more; more resources never hurt). The product boxes' rows are the demand. An output port feeding several functions meets the largest of their demands on an intensive carrier (the default: one shared level) and their sum on a carrier declared quantity: extensive. Composes the rows along non-harmful functions, including feedback loops, by Kleene's ascent from nothing demanded to the least fixpoint, and returns the minimal resource vectors (fixed costs of every box plus the chosen rows' operating costs), each with its rows and demanded levels. Verdict against the model's budget: feasible; infeasible (reason over-budget, with the binding dimensions every minimal vector exceeds, or unprovidable, naming the port no row can serve); or undecided (missing-feasibility, no-budget, unbudgeted, circular-resource-support). A bounded source-support closure from zero provision must ground a selected affordable witness; steadyState reports the separate balance verdict. With trim and absorb (as triz_behavior takes them), apply the trim and decide the trimmed model; the baseline is solved only to report each absorber's added resources. When carriers declare levels (thresholds reading amounts as declared values), levels reports each feasibility row, of a box that also declares behaviour, whose named amounts read as values no matching behaviour row gives (value-mismatch) or at inputs the behaviour rules out (no-behavior-row). Fails closed on ill-typed or dominated rows, a requirement no non-harmful function supplies, an extensive input fed by several functions (extensive-fan-in: model a merge box), and past the caps. No polynomial bound is claimed. The verdict holds for the rows as declared; the absorber's new harms are not modelled. An infeasible verdict also carries relaxation: over-budget results list the nondominated minimal budget raises that would make the model affordable, each with its row-selection witness (budget_feasible_iff), and the cheapest raise of any single dimension that suffices alone; unprovidable results list the smallest per-port capability raises. Raises advise; the budget stays the caller's declaration.

Check that a coarse function model (few boxes, e.g. with declared behaviour) is an abstraction of a detailed one of the same system (many boxes, e.g. with costs and feasibility) under a typed map: detailed box → coarse box (several may share one; a box left out is outside the abstraction), per box detailed port → coarse port (default: the same id and side), detailed carrier → coarse carrier (default: the same id). A function between two mapped ports is mapped; one between unmapped ports of boxes with the same image is hidden inside that coarse box; one between boxes with different images and an unmapped port is forgotten. Four checks: total (every mapped port's carrier has an image, and every mapped function has an image coarse function with the mapped endpoints, the mapped carrier, and the same polarity class: negative = harmful or excessive, or not), typed (each mapped port lands on a port of the same side whose carrier is its carrier's image, of the same layer; typed_map), wires (every coarse function is the image of a mapped detailed function of its class), harm loops (every coarse harm loop is the image of a detailed one: each harmful or excessive coarse function on it has such a preimage whose object reaches its performer along mapped and hidden functions; cycle_map, with the detailed cycle as witness). Verdict abstraction or not-an-abstraction with the failing checks. Also reports the functions hidden, forgotten, and left out (harms listed apart), the detailed harm loops the coarse model hides or loses, whether reachability among mapped boxes passes to the coarse model (reach_map, when nothing is forgotten), and, where a coarse box with behaviour has one preimage box with feasibility, whether that box's feasibility amounts read through the coarse carriers' levels fall in the coarse behaviour. When either model declares flows, each detailed flow's runs inside the mapped boxes are sent through the map like a merge and matched step by step against the coarse flows of the image carrier (flows.images), and coarse flow steps no detailed step maps to are listed (flows.unbacked); flows do not change the verdict. Fails closed on a model that does not type-check and on map ids that do not exist. Whether the coarse rows are true of their preimages is substantiated outside the kernel.

System operator (9 windows) over function models: for past, present, and future, the subsystem view (restriction to the boxes you name, with crossing functions as its boundary), the system view, and the supersystem view (the tool and mediator boxes, or the boxes you list, collapsed into one black box; hidden harmful functions are listed). Each view reports its boxes, function counts, and harm loops. Present is required. Past and future are snapshots with stable box ids, or transitions: triz_transform operations applied in order (past_to_present needs past and must reach present; present_to_future must reach future if given, or derives it). A transition that fails or does not reach its snapshot fails closed. Each transition is reported as one net rewrite step, its part inside the subsystem (which takes the earlier subsystem view to the later one), whether it stays within the subsystem, and the boundary functions it cuts and adds. When the snapshots declare behaviour or feasibility, each time's system view carries its verdicts (system.verdicts) and each change between times says how they move (changes[].verdicts): behaviour compared as triz_behavior compare_to does, weakness ranked with acceptable, and feasibility, changed only when both sides are decided; a failure there never fails the grid. When the snapshots declare flows, the verdicts carry each flow's triz_flow candidates, and each change lists the flows added, removed, and re-routed and the candidates each flow gains or loses; a transition must reach the snapshot's flows too, and flowsChanged lists the flows it changes. Missing windows are reported as prompts.

Return the domain-neutral TRIZ lookup regressions and cross-domain reasoning cases.

Distinguish a declared subsystem summary from one checked against the complete inner steady-state relation and a single declared resource mode. Verification checks exact behavior over explicit assumptions, nonblocking, levels, demands, budgets and source support using the same bounded closure as flat feasibility. Declared boundary amounts seed support; circular-resource-support and source-support-cap are undecided. max_support_work independently caps support checking; missing data or unsupported modes are undecided. Resource/behavior coupling remains a declared empirical assertion. Caller-supplied checked status is never trusted.

Check nonblocking and acceptable outputs over required operating situations under an explicit scope. Equality of two partial relations does not establish adequacy.

Verify or search a bijection preserving wiring and declared semantic annotations; search continues past incompatible automorphisms and returns undecided on its global budget.

Compose two WHOLE models and check exact equality or directional inclusion under explicit boundary and deliverable value maps. Complete relations are checked; no physical transfer is inferred.

Compose a stateless subsystem into an exact finite boundary relation with an explicit port map, fixed cost, and hidden-harm list. Complete serial maps use the checked symbolic compiler; other declared relations use exact finite projection. Empty relations remain explicit and missing behavior stays unknown.

Evaluate named complete implementations against one whole-model behavior, adequacy, declared-harm and resource contract. Never splice behavior and cost from different modes; provenance remains declared.

Enumerate all compatible absorber endpoints and complete assignments under one finite contract and a shared work budget. Separate per-function successes do not establish joint sufficiency.

Search finite behavior/resource alternatives jointly on fixed wiring. Optimized search uses coupled residuals; symbolic search composes typed joint finite maps across explicit wire permutations and reuses equivalent residual domains before union trace enumeration, with bounded fallback; exhaustive retains the reference search. Every surviving tuple meets one shared engineering contract. Capped search is undecided; impossibility is only within the declared library.

Decide exact finite global compatibility of allowed tuples on overlapping variable contexts, with a witness or complete empty join. Pairwise projection compatibility alone is insufficient; no cohomology is computed.

Compile a finite discrete queue with explicit arrivals, service/storage capacity, schedule and units, then check overflow through existing dynamics. All declared arrival combinations within the schedule are considered.

Check declared consumptive versus shared-level supply constraints for explicit units. Consumptive branches sum; shared intensive requirements use max. No physical law is inferred from labels.

Validate a named rule subset and establish termination when every successful application strictly decreases lexicographic box/wire counts. No global confluence or critical-pair completeness is inferred.

Replay two named structural rewrites in both orders and check whether those occurrences commute. Interference does not prove nonconfluence.

Return an applied trim as explicit deletion/gluing data with its declared absorbers, interface, and checked replay. No Kan-extension claim is made.

Local-only import of supplied BOM, OpenAPI, Quint, Lean or Julia inputs. Prefer modelingtoolkit-json and agents-json exports from instantiated Julia models; raw julia is a partial static fallback. Does not fetch references, execute source or load checkpoints. Returns a draft interaction table and model with embedded unconfirmed provenance; review all ratings and assumptions before analysis. Source-code outlines are partial syntactic references, not verified causal or finite behavior models.

Local-only explicit analyst confirmation of an imported model. Edit the draft first, then confirm every pending id exactly once with decision confirm and optional note. Source locations remain embedded; review asserts the supplied ratings and assumptions, without proving source correctness or physical truth.

Optional project extension: analyse an OTSM Network of Problems (contradiction graph) and its verifier-backed purpose gates. A node may carry a PhysicalContradiction; each is checked by separationCheck (irreducible, separable, no-contradiction, or invalid, which fails closed for that node), and the core-conflict ranking breaks ties on dissolves in favour of irreducible nodes and flags a top node that already separates. Requires a project graph via TRIZ_GRAPH; not part of the neutral skill core.

Optional project extension: inspect the invariant, purpose gate, and separation check of one contradiction node of the project graph.