TRIZ

Get a canonical TRIZ engineering parameter (1-39). Omit id to list all 39.

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.

Search the curated effects database by required function (e.g. 'convert temperature difference into voltage', 'store heat', 'sense strain') or list by category: physical, chemical, geometric. Effects are classical textbook phenomena; selecting and substantiating one remains a synthesis step, never a lookup verdict.

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. With `certificate: true`, also returns a Lean file that states these separation verdicts about this contradiction and proves them against theory/CategoricalTriz.lean, so Lean can check this one result.

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), 'lean' gives a certificate: a Lean file that encodes the model as finite data and states the kernel's verdicts about it (typing, each harm-loop witness cycle, and the separation verdicts of embedded contradictions), each proved against theory/CategoricalTriz.lean, so Lean can check this one model's verdicts (`certifies` lists them; nothing is extracted). 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

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

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 co

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, a

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 rea

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). 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.

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 flo

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 and budgets; 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. Empty relations are reported without inventing unknown behavior.

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 the Cartesian product of finite behavior/resource alternatives for several stateless holes on fixed wiring. Each complete tuple meets one shared contract; capped search is undecided, impossibility is only within this 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.