<!– generated-from claims/claims.toml sha256:2f0adfe4fb996bce3bf36cd6b0a20c33d8001c94bac2db5ed7bb3ea501779e68 –> This page is generated from claims/claims.toml and the JSON artifacts under experiments/generated/. It is the HTML knowledge base's retrieval layer; the curated PDF route does not attempt to reproduce these indexes as a linear chapter sequence. For a compact visual summary of notation, terminology distinctions, coverage gaps, and verification state, see the evidence map and verification summary.
| Claim | Chapter | Verification |
|---|
FORMULATION-Y-SPLIT-001 — A load or generator may be represented as a factor attached to a source network while a declared study formulation places a constant-admittance, Norton, or other linearized part in the nodal operator and retains the remainder as an injection, control, limit, or decision relation; the resulting nodal matrix is therefore mode-, state-, and linearization-qualified rather than a unique graph of the source system. | Circuit formulations and the lowering boundary | self-checked |
GRAPH-LOOPY-001 — Network-reduction and microgrid-stability literature uses loopy-Laplacian self-loop terms for grounded or differential-conductance diagonal effects; that matrix-level usage is distinct from the book's ordinary graph-loop convention with a zero signed-incidence column. | Multigraphs for expert modelers | self-checked |
GRAPH-MULTI-001 — The book's finite undirected multigraph is an identified edge-and-flag object in which every edge owns exactly two distinct flags; loops have two flags incident to one vertex, parallel members retain distinct edge identities, and attributes remain typed maps rather than being inferred from adjacency. | Multigraphs for expert modelers | self-checked |
GRAPH-NPORT-001 — Allowing a relation to own an arbitrary finite flag fibre generalizes the two-uniform multigraph to an incidence structure, while an expert mathematical model additionally needs typed flag spaces, relation roles or ordering, and a constitutive relation to represent an n-port factor rather than merely its hypergraph incidence. | Multigraphs for expert modelers | self-checked |
GRAPH-SELF-LOOP-001 — In the book's loopless bus–branch circuit specialization, ordinary edges connect distinct retained circuit nodes; a graph self-loop may remain in the source multigraph or arise from a topology quotient, but it is not interchangeable with an electrical circuit loop or mesh, a grounded shunt, or a diagonal self-admittance term. | Multigraphs for expert modelers | self-checked |
GROUND-SCOPE-001 — Reference, neutral, earth-return, and grounding-asset semantics are distinct model objects; reductions involving them must declare an earth-return class, grounding points, retained observations, and recovery data. | Earth, neutral, and reference model classes | self-checked |
LOAD-BASE-001 — A voltage-dependent load's nominal voltage is an anchor in the load factor's declared terminal coordinate: WYE uses phase-to-neutral voltage and DELTA uses line-to-line voltage; copying one numeric bus voltage into both coordinates without an explicit base conversion changes the normalized load law. | Load models and decision dependence | self-checked |
NUMERICAL-001 — Representation and reduction choices have numerical consequences that must be reported separately from electrical preservation: coordinate scaling changes conditioning without changing an invertible solution set, Jacobian dependency graphs need not equal physical graphs, Schur elimination can create fill-in, and decision certificates require residual/error estimates and margins. | Numerical consequences of representation and reduction | self-checked |
NUMERICAL-004 — A solver termination status is an algorithm report, not an independent solution-validity certificate; any scientific claim based on returned primal values must separately check the relevant numeric finiteness, equations, bounds, residuals, recovery obligations, and optimality level. | Numerical consequences of representation and reduction | self-checked |
NUMERICAL-005 — A complete solved-network feasibility claim requires an independently computed witness covering equation, KCL, power-balance, device-limit, and recovery residual obligations with declared tolerances; solver termination remains separate evidence. | Numerical consequences of representation and reduction | self-checked |
PRESERVE-001 — Equivalence of two power-network models is indexed by a declared joint observation map and admissible input set; matching separate observation ranges or an unconstrained terminal relation alone does not establish equality of joint constrained feasible observable sets. | Preservation contracts | self-checked |
RATING-001 — A power-network rating must identify its constrained asset or terminal, measured quantity and feasible region, duration, ambient/scenario validity, and ownership/provenance before a transformation can claim to preserve it. | Rating and limit semantics | self-checked |
THESIS-001 — Representation adequacy is evaluated relative to declared observations, constraints, and decisions. | Scope and thesis | self-checked |
TOPOLOGY-001 — For a fixed switch state, topological nodes are the connected components of the closed-switch connectivity graph; compiling them into bus–branch buses is a state-conditioned quotient that requires provenance and does not preserve switching decisions by itself. | Node–breaker, bus–breaker, and topology processing | self-checked |
TRANSFORM-SEM-001 — Transformation certificates should distinguish typed structure, constitutive behaviour, decision semantics, and provenance; a structure-changing rewrite may remain exact for a narrower observation family only when its forgotten information, target closure, and recovery or constraint maps are declared. | Transformation semantics and register | self-checked |
| Claim | Chapter | Verification |
|---|
ARCH-BLOCK-001 — For a declared two-bus four-conductor linear factor, the vector-edge, port-factor, block nodal, scalar-support, and realified-coordinate views are related representations of one assembled relation; coordinate expansion and realification do not create physical assets, while factor identity remains separate provenance. | How to read power-network diagrams and equations | self-checked |
ARCH-CONDUCTOR-002 — The five-bus scalar line-identity fixture lifts to fourteen scalar endpoint ports, five terminal junctions, and seven two-port line factors; the lift retains the q/r parallel fibre and its extra cycle dimension while adding no multiconductor, switch, or transformer semantics. | Formal representation frameworks | self-checked |
ARCH-FIVEBUS-XFMR-001 — In the recorded five-bus structural extension, one three-port transformer has acyclic local factor-incidence and star realizations, while eliminating the virtual star point generically yields a terminal clique with cycle rank one; the embedded factor-incidence and star member ranks coincide at five despite carrying different semantics, while the clique member rank is six, without implying additional physical transformer loops. | Five buses through a multi-port lowering | self-checked |
ARCH-PORT-001 — A minimal executable port–factor bundle instantiated from the running network validates typed port-to-junction and port-to-factor incidence, a three-port multiwinding factor, grounding as an explicit factor, and a many-to-many asset/electrical relation Λ. | Formal representation frameworks | self-checked |
ARCH-PORT-002 — The five-bus identified scalar multigraph has a direct structural port–factor lift with five bus junctions, seven two-port scalar line factors, fourteen endpoint ports, and one asset-to-factor relation per identified line; parallel members q and r remain distinct factors despite sharing the same bus pair. | Formal representation frameworks | self-checked |
AU-CARSON-001 — The Australian Carson reproduction regenerates overhead and underground multiconductor primitives from lifted construction inputs, compares them with independent OpenDSS reference matrices, and identifies the CS1035 construction mapping as unresolved rather than presenting it as a faithful reproduction. | Australian construction inputs: Carson and OpenDSSDirect | independently-implemented |
COLLAPSE-002 — The generated Fortescue witness diagonalizes a circulant three-phase impedance matrix and preserves the positive-sequence subspace, while a non-circulant perturbation produces sequence mixing and a positive-subspace residual. | When the general model collapses | self-checked |
FIXTURE-001 — Running-network fixture v0.1.0 passes the current BMOPFTools JSON schema and conformance checks without errors or warnings. | Executable running network | self-checked |
FIXTURE-002 — The v0.1.0 continuous PF and OPF instances terminate locally solved in the recorded environment. | Executable running network | self-checked |
GROUND-SCOPE-002 — On the recorded two-conductor fixture, floating, finite-impedance, and ideal customer-end grounding relations share the same simple bus–branch graph but change neutral voltage, ground-current allocation, and the associated observations. | Earth, neutral, and reference model classes | self-checked |
GROUND-SCOPE-003 — In the scoped E₂ witness, an explicit earth conductor with a finite neutral-to-earth bond has distinct in-service, earth-conductor-outage, and phase-to-earth-fault states; the outage changes earth-current availability and the fault crosses the declared protection-current threshold while the simple bus graph remains fixed. | Earth, neutral, and reference model classes | self-checked |
GROUND-SCOPE-004 — In the explicit-earth witness, a declared inverse-time relay curve maps the CT-scaled phase-earth fault current to a 0.2466 s operation, while the neutral-earth fault remains below pickup; a separate declared CT-saturation cap changes the phase-fault trip decision. | Earth, neutral, and reference model classes | self-checked |
IMPEDANCE-LADDER-001 — In the deterministic four-wire impedance ladder fixture, phase-to-neutral current and voltage recovery are exact under the declared zero-ground-current map, while the deliberately non-circulant reduced matrix has visible sequence mixing; shunt deletion and positive-sequence use therefore require explicit decision-domain guards. | Four-wire impedance-model ladder | self-checked |
LLM-RETRIEVAL-001 — On its recorded prior corpus and held-out paraphrase set, the pinned compact neural retriever and generic cross-encoder reranker each failed at least one predeclared not-worse-than-hybrid retrieval gate, so neither candidate was promoted into the production route. | Federated scientific knowledge: end-to-end trace | self-checked |
LOAD-CONNECTION-001 — On the recorded balanced three-phase terminal fixture, explicit wye phase-to-neutral and delta phase-to-phase connection maps share the same bus and graph but produce different load-voltage observations: unit-magnitude wye voltages and sqrt(3)-magnitude delta voltages. | Load models and decision dependence | self-checked |
LOAD-CONTINUATION-001 — On the recorded scalar two-bus continuation probe, the damped CP branch first fails to converge at demand scale 1.8 after a converged scale 1.7, while CI, CZ, and the declared ZIP branch remain converged through scale 3.0; this is an iteration-scoped branch diagnostic, not a global collapse theorem. | Load models and decision dependence | independently-implemented |
LOAD-DECISION-001 — On the recorded two-bus fixture, CP, CI, CZ, and a normalized ZIP load law share the same bus–branch graph but produce distinct high-voltage solutions and decision margins: CP violates both the declared voltage and current limits, while CI, CZ, and ZIP satisfy both. | Load models and decision dependence | self-checked |
NUMERICAL-002 — For the pinned running-network fixture, BMOPFTools exports a 20-by-20 passive Ybus with 166 nonzeros; the constant-Z linearized Ybus agrees with it, and realification produces a 40-by-40 current-voltage matrix with 664 nonzeros. The complex matrices have numerical rank 18 at the declared tolerance, with rank-aware effective 2-norm condition about 6.50e8 (1.13e7 after equilibration); the realified embedding preserves support and dimension but is not complex-transpose-symmetric. | Numerical consequences of representation and reduction | self-checked |
NUMERICAL-003 — In the pinned nonlinear two-bus parallel-member witness, retaining two explicit member-current laws produces a 6-by-7 residual Jacobian and 13-by-13 KKT pattern, while the summed-current aggregate produces a 4-by-5 Jacobian and 9-by-9 KKT pattern; symbolic fill changes with elimination order in both formulations. | Numerical consequences of representation and reduction | self-checked |
TR-GRAPH-ACTIVE-001 — For the five-bus fixture, the inventory has identified-member cycle rank 3 and simple-projection cycle rank 2, while the declared spanning tree is radial at both levels; active radiality is therefore a state-specific property, not an inventory-only label. | Cycles, parallelism, and radial structure | self-checked |
TR-KRON-002 — In the declared linear scenario fixture, exact Kron reproduces each fixed-injection boundary relation, an operating-point Ward-style equivalent is exact only at its calibration point, and an explicit scenario objective can select a sparser non-exact target. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-003 — In the declared one-state linear Ward scenario fixture, an internal-injection residual propagates through a recovered-state bound and a boundary-current bound to classify the approximate source-limit decision as certified feasible, ambiguous, or certified violated; the bound is exact for this fixture but is not a general nonlinear error theorem. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-FIVE-001 — In the five-bus scalar fixture, eliminating the pendant bus m through line u by typed Kron reduction reproduces the retained boundary Y-bus obtained by direct deletion of the leaf line, with exact boundary-current recovery for the recorded voltage state. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-FIVE-002 — In the same five-bus fixture, eliminating the non-pendant bus l by typed Kron reduction preserves the recorded boundary current relation, creates Schur-complement fill edges j-m and k-m among the retained buses, and exactly recovers the u-branch current whose deliberately tight declared limit is violated by the recorded state. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-001 — In the running four-conductor midpoint Kron fixture, the eliminated neutral half-section current is exactly recoverable from the retained boundary solution and midpoint recovery; a neutral-current limit must therefore remain in the reduced feasible set, and dropping it admits the recorded boundary point that the source model rejects. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-002 — In the recorded five-conductor midpoint probe, retaining an explicit earth terminal and a midpoint neutral-earth bond yields separately recoverable neutral and earth KCL currents and a neutral-current limit; collapsing earth return into neutral would lose an observed factor relation. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-003 — In the recorded three-segment five-conductor probe with two explicit neutral-earth bonds, each grounding point has separately recoverable neutral and earth KCL currents and bond-current observations; a single collapsed neutral constraint cannot represent both points. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-004 — In the recorded finite grounding-impedance sweep, changing the two explicit neutral-earth impedances changes recovered neutral current and the feasibility classification under one fixed neutral limit, even though the structural reduction and KCL contracts remain unchanged. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-005 — In the recorded local state-dependent grounding probe, shifting an endpoint state changes the nonlinear neutral-earth bond map; reusing the nominal bond map leaves a nonzero shifted-state residual, while recomputation restores the relation and preserves explicit neutral-limit evaluation. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-006 — In the recorded two-point state-dependent grounding chain, shifting the endpoint state changes both nonlinear neutral-earth bond maps; freezing both nominal maps leaves a nonzero chain residual and changes recovered segment-neutral currents, while recomputation restores the local relation. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-007 — In the recorded finite endpoint-state continuation of the two-point nonlinear grounding chain, recomputing the bond maps at five declared states preserves small nonlinear residuals and records changing neutral-limit margins, while the frozen nominal map fails away from the base state. | Kron, Ward, and optimized network equivalents | self-checked |
TR-KRON-NEUTRAL-008 — In the recorded local nonlinear grounding derivative probe, the analytic real Jacobian at the base state gives a smaller shifted-state linearisation error than the frozen nominal bond coefficient, and the Jacobian error decreases over the declared smaller step scales. | Kron, Ward, and optimized network equivalents | self-checked |
TR-NEG-001 — The executable anti-pattern witness rejects or classifies four tempting compositions: a heterogeneous series composite is not a homogeneous physical line, external grounding is not absorbed into a transformer, a three-port transformer is not a two-terminal line, and aggregate BIM/BFM branch balance does not imply member voltage compatibility. | Translation traps: graphs, circuits, and power-system language | self-checked |
TR-PAR-003 — In the recorded two-bus maximum-served-load problem, the naive summed-rating aggregate serves 200 MW while the source and exact lifted formulations each serve 110 MW. | A plausible model gives the wrong answer | self-checked |
TR-PAR-004 — In the recorded two-conductor AC maximum-served-load case, the source, exact lifted, and certified exact-pruned formulations have objective 0.6138908, while a summed-limit aggregate has objective 1.0630833 and violates a 0.6 p.u. member limit. | Multiconductor parallel AC decision case | self-checked |
TR-PAR-AC-JOINT-001 — In the recorded three-member four-wire AC case, member 3 has the fixed recovery Il3=0.10 Il1+0.10 I_l2 and a 0.15 p.u. component limit; the joint support bound is 0.144 p.u., so deleting member-3 limits preserves the locally solved source objective 1.2401762 to 7e-14. An independent damped-Newton continuation and bisection reproduces the source boundary within 1.3e-8 served-fraction units. | Four-wire nominal-pi parallel case | self-checked |
TR-PAR-SINGULAR-001 — For the declared series-only singular four-wire fixture, the full two-end terminal-current map is rank deficient, but the endpoint-voltage-drop coordinate recovers member-2 currents exactly from member-1 currents through the declared diagonal map, with the zero-neutral rows retained as an explicit invariant; this is a guarded reduced-coordinate result, not a pseudoinverse or singular-shunt theorem. | Four-wire nominal-pi parallel case | self-checked |
TR-PAR-STATE-001 — In the recorded finite four-state four-wire AC envelope, rebuilding the member maps and source/pruned formulations at each declared scalar or phase-selective admittance state preserves exact joint limit pruning locally while changing the optimal served value across states. | Four-wire nominal-pi parallel case | independently-implemented |
TR-XFMR-007 — A separate damped finite-difference Newton, continuation, and bisection implementation reproduces all three TR-XFMR-006 tap-conditioned high-voltage branch boundaries without an external optimizer; its largest served-fraction difference from JuMP/Ipopt is 3.14e-10, and both methods select tap 0.95. | Transformer tap AC decision case | independently-implemented |
TR-XFMR-008 — In the recorded 11-terminal WYE/WYE/DELTA tap case, a phase-selective unbalanced second scenario can be handled without collapsing the transformer or its phase identities: exact enumeration of the nine ordered tap pairs preserves branch completeness and exposes the per-phase scenario directions explicitly. | Transformer tap AC decision case | self-checked |
TR-XFMR-009 — For the recorded 11-terminal WYE/WYE/DELTA case, a three-scenario phase-selective tap path can be enumerated exactly over the 3^3 ordered tap triples, with consecutive tap movement charged explicitly and each scenario retaining its own phase directions. | Transformer tap AC decision case | independently-implemented |
TR-XFMR-010 — In the recorded three-scenario tap path, enumerating all 27 ordered tap triples and then applying an explicit at-most-one-movement policy leaves 15 admissible branches; the policy is a decision constraint and must not be inferred from the unconstrained best path. | Transformer tap AC decision case | independently-implemented |
| Claim | Chapter | Verification |
|---|
ARCH-CHORDAL-001 — For a simple bus-level tree with a common m-coordinate block at every bus and a structurally dense two-terminal stamp on every tree edge, the scalar structural-support graph is chordal and leaf-bus block elimination is a zero-fill perfect elimination ordering. | Two topology levels and the nodal projection | self-checked |
ARCH-LOWER-001 — A typed lowering from an identity-bearing n-port source graph to ordinary-edge incidence objects may preserve a declared equation relation while forgetting factor identity unless source fibres and provenance are retained. | From source graphs to views and graph surgery | self-checked |
ARCH-LOWER-002 — A four-winding transformer factor can be compiled pointwise into a complete terminal equation operator while retaining a full non-diagonal reference impedance, mixed winding connection maps, connection-specific shunts, internal grounding, recovery maps, and an explicit finite tap/phase decision domain; this does not by itself provide a source-faithful ordinary-edge realization. | Five buses through a multi-port lowering | self-checked |
ARCH-NODAL-001 — Assembly of typed linear factor stamps into a compound nodal operator is not generally injective: distinct admissible parallel-factor decompositions can produce an identical nodal operator and identical normalized assembly residuals. | Two topology levels and the nodal projection | self-checked |
ARCH-RECOVERY-001 — Source recovery from a compound nodal operator is class-dependent: support-separated single-factor classes can be identifiable, over-parameterized classes can be set-identifiable at the terminal-primitive level, and parallel multiplicity or eliminated internal coordinates can be non-identifiable; a recovery interface must report the status and ambiguity rather than infer asset identity. | Two topology levels and the nodal projection | self-checked |
ARCH-RECOVERY-002 — Auxiliary observations and declarations lift source-recovery ambiguity only through their joint observation map: catalog bounds may produce a compact but non-singleton feasible set, whereas member-current measurements, explicit grounding attribution, or a declared transformer state can make the restricted map injective in a scoped model class. | Two topology levels and the nodal projection | self-checked |
ARCH-RECOVERY-003 — For a matrix-valued multiconductor factor observed through member-current snapshots, full primitive recovery requires voltage snapshots spanning the retained conductor space and coverage of every current coordinate; single-snapshot or phase-selective observations retain reciprocal ambiguity even when the assembled nodal operator is known. | Two topology levels and the nodal projection | self-checked |
ARCH-RECOVERY-004 — For noisy full-rank multiconductor voltage/current snapshots, the pseudoinverse source estimate has a deterministic Frobenius error bound proportional to the noise radius and the voltage-snapshot pseudoinverse norm; nearly dependent excitation therefore enlarges the certified uncertainty set even when the observation map is full rank. | Two topology levels and the nodal projection | self-checked |
ARCH-SUPPORT-001 — Block and scalar nonzero-support graphs of a declared compound nodal operator are simple graphs by construction, while the identified factor-stamp decomposition is separate data and may be a multigraph. | Two topology levels and the nodal projection | self-checked |
COLLAPSE-001 — Under compatible three-phase terminals, cyclic (circulant) series and shunt matrices, balanced boundary data, sequence-compatible grounding, two-terminal factor closure, phase-symmetric decisions, and positive-sequence observations, the general phase-domain relation restricts exactly to the positive-sequence scalar network. | When the general model collapses | self-checked |
COUPLED-CORRIDOR-002 — For two fixed linear reciprocal scalar series sections with a nonsingular joint impedance matrix, AGamma^T ZGamma^{-1} AGamma has an exact six-edge weighted-lattice realization on the four source terminals; source section currents are recovered by ZGamma^{-1} A_Gamma u, while the generated cross edges carry no asset or galvanic interpretation. | A coupled multi-voltage corridor | self-checked |
FORMULATION-NODAL-001 — An ideal voltage source with a queried source current is not representable by a plain nodal-admittance injection without adding an extra current variable or changing the query contract; a modified-nodal or tableau formulation preserves the voltage constraint and current observation. | Circuit formulations and the lowering boundary | self-checked |
FORMULATION-NODAL-002 — Even when a nodal operator can be assembled, it may be singular without a declared reference or shunt, or semantically insufficient for member-level limits: aligned parallel factors can share one aggregate admittance while having different member currents and feasible limits. | Circuit formulations and the lowering boundary | self-checked |
FORMULATION-NODAL-003 — A declared reference or grounding label does not by itself establish nonsingularity of a compound nodal operator: the rank guard must be evaluated on the assembled operator after the declared reference, grounding, and active-state maps are applied. | Circuit formulations and the lowering boundary | self-checked |
GRAPH-CYCLE-001 — The recorded connected five-bus bus–branch multigraph has seven identified lines, incidence rank four, and cycle-space dimension three; collapsing its parallel q/r pair to a simple edge reduces the cycle-space dimension to two, whereas the spanning-tree-plus-chords representation retains all three source dimensions. | A five-bus multigraph: identities, cycles, and tree coordinates | self-checked |
GRAPH-MATRIX-001 — Under the declared convention Auv equals non-loop edge multiplicity off diagonal, Avv equals twice the graph-loop count, and D contains incidence degrees, so D-A equals B B transpose; graph-loop columns vanish from signed incidence while a grounded shunt contributes a distinct diagonal constitutive term. | Multigraphs for expert modelers | self-checked |
GRAPH-PI-COLLAPSE-001 — For a fixed linear two-terminal pi factor with series admittance Ys and endpoint shunts Ya and Yb, identifying both terminals through the common attachment map Tpi=[1,1]^T gives Tpi^T Ypi Tpi=Ya+Y_b, so the series contribution cancels and the exact nodal image is a one-terminal constant-admittance shunt under the declared coordinate and reference assumptions. | Multigraphs for expert modelers | self-checked |
LIT-PAR-001 — For fixed scalar AC pi-line models on common endpoints, dominance of normalized squared member currents for all endpoint voltages certifies a redundant current limit; with apparent-power ratings the shared terminal-voltage magnitude cancels in the comparison, giving a sufficient redundancy test using auxiliary quadratic sets, not the original apparent-power feasible regions. Checking both terminals certifies removal of both directional limits without aggregating members. | A plausible model gives the wrong answer | self-checked |
PRACTICE-DUAL-001 — For min betacp subject to alpha(d-p)<=0 with positive c,d,alpha,beta, dispatch remains p=d while the Lagrange multiplier is betac/alpha and physical marginal cost is alpha/beta times that multiplier; duplicating the unscaled constraint admits nonunique multiplier allocations summing to c. | Building and changing a model you can check | self-checked |
PRACTICE-IMPORT-001 — A numerical round trip of MATPOWER RATE_A=0 can succeed while a faulty decoder replaces its explicit unlimited-rating meaning with a finite zero bound, changing the admissible transfer set. | Building and changing a model you can check | self-checked |
PRACTICE-UPDATE-001 — Opening one arm of a three-arm 1 S resistive star changes the remaining two-terminal equivalent conductance to 1/2 S; deleting the two corresponding edges of the original 1/3 S reduced triangle incorrectly leaves 1/3 S, despite symmetry and zero row sums. | Building and changing a model you can check | self-checked |
TR-COMP-001 — Two exact certified transformations compose when the first target is consumed by the second source; constraint maps apply forward and recovery maps apply in reverse order. | Certificate schema and composition | self-checked |
TR-COORD-001 — A simultaneous permutation of conductor coordinates, terminal pairing, element matrices, and componentwise limits is an exact normalization with an inverse permutation. | Conductor-coordinate normalization | self-checked |
TR-GRAPH-001 — For a loopless identified multigraph and its simple endpoint projection, the multigraph cycle rank exceeds the simple-graph cycle rank by the sum over edge fibres of fibre size minus one; the lost dimensions are line-identity cycles supported on parallel fibres. | Cycles, parallelism, and radial structure | self-checked |
TR-GRAPH-002 — An identified line is a multigraph bridge exactly when its simple endpoint edge is a bridge and its parallel fibre is a singleton; consequently the identified multigraph is a forest exactly when its simple projection is a forest and every edge fibre is a singleton. | Cycles, parallelism, and radial structure | self-checked |
TR-GRAPH-SIMPLIFY-001 — The loopless simple endpoint projection preserves the vertex set, adjacency, connected components, distinct-neighbour sets, and unweighted vertex distances, but it does not preserve identified edge count, incidence degree, cycle-space dimension, bridges, edge connectivity, spanning-tree multiplicity, or member-level state and provenance. | Multigraphs for expert modelers | self-checked |
TR-KRON-001 — Typed multiconductor Kron reduction commutes with invertible coordinate actions that preserve the retained/internal partition when currents transform by the power-dual action; per-port block diagonality is an optional locality restriction, and the affine statement requires fixed internal injections. | Kron, Ward, and optimized network equivalents | self-checked |
TR-PAR-001 — Summed admittance preserves the unconstrained terminal relation of parallel linear branches. | A plausible model gives the wrong answer | self-checked |
TR-PAR-002 — Using the sum of member current ratings can create an outer relaxation of the member-constrained feasible set. | A plausible model gives the wrong answer | self-checked |
TR-PAR-005 — For fixed linear complex terminal-current maps with centered Euclidean norm limits, one normalized constraint implies another if and only if the retained normalized real quadratic form minus the candidate form is positive semidefinite; applying this pairwise test to every aligned conductor and both terminal ends certifies exact candidate-limit pruning while retaining both member models. | Multiconductor parallel AC decision case | self-checked |
TR-PAR-006 — For nonsingular fixed series admittances on common multiconductor endpoint coordinates, candidate component currents recover as Il2=(Yl2/Yl1)Il1, and the exact maximum of candidate component c over all retained component-current discs is sumk abs(Kck) Imax_l1k; in the recorded reciprocal non-proportional three-phase four-wire AC case this certifies all l2 limits redundant, the exact-pruned and source objectives agree at 1.1274329, and a summed-limit aggregate reaches 1.8058181 by violating an l1 limit. | Non-proportional three-phase four-wire parallel case | self-checked |
TR-PAR-007 — For fixed nominal-pi multiconductor members whose retained full two-end terminal-current primitive Ar is nonsingular, all candidate terminal currents recover as Ac*inv(Ar) times the retained terminal-current vector, so exact complex-polydisc row norms certify joint implication across both line ends; in the recorded non-proportional four-wire case, pruning eight member-2 limits preserves the 1.1286205 source objective while a same-size summed-limit model reaches 1.8077114 by violating member 1. | Four-wire nominal-pi parallel case | self-checked |
TR-PAR-JOINT-001 — For fixed series current maps in common endpoint-voltage-drop coordinates, a candidate component-current limit is implied by several retained member limits when its exact recovery row has support bound sumk abs(Kck) Ibar_k no larger than the candidate rating; the guarded witness certifies this joint implication for three retained discs. | Four-wire nominal-pi parallel case | self-checked |
TR-SER-001 — A zero-injection degree-two junction between coordinate-aligned, series-only elements with no pairwise or external mutual coupling has equivalent impedance Zl1 + P' Zl2 P; mutually coupled sections instead contain the cross terms Z12 P + P' Z21. | Degree-two series elimination | self-checked |
TR-SER-002 — Exact terminal-behaviour closure under degree-two elimination does not by itself establish closure within a homogeneous physical line class. | Degree-two series elimination | self-checked |
TR-SER-003 — For a zero-injection degree-two junction whose two series-only source elements declare both pairwise cross-impedance blocks and no external mutual coupling, the exact terminal-behaviour composite has impedance Z1 + Z12 P + P' Z21 + P' Z2 P, with source currents recovered by I1 = Iequivalent and I2 = P Iequivalent. | Degree-two series elimination | self-checked |
TR-XFMR-001 — A transformer winding terminal permutation is an exact typed-factor normalization when its complete terminal-to-coil incidence relation is right-multiplied by the inverse permutation and coil coordinates remain fixed. | Transformer-winding coordinate normalization | self-checked |
TR-XFMR-002 — Complete pairwise multiwinding short-circuit impedances compile exactly into a reference-coordinate impedance matrix ZB, from which every pairwise impedance is recoverable; changing the selected reference winding leaves the external winding admittance invariant, and the classical star/T representation is the three-winding special case. | Multiwinding leakage reference compilation | self-checked |
TR-XFMR-003 — Aligned winding connection-incidence factors compose exactly with a multiwinding leakage admittance as Yterminal=A'(Yw kron I)A; retaining the coil-current map preserves per-coil winding limits and makes terminal-coordinate and leakage-reference changes explicit coordinate actions. | Multiwinding terminal leakage assembly | self-checked |
TR-XFMR-004 — A fixed linear transformer completion with declared voltage transfer T, leakage map B=TA, excitation placement S, and transformer-internal grounding has terminal admittance Ycomplete=B^HYcoilB+S^TY0*S+Yground; the power-dual and component-current recovery maps preserve the declared leakage-path limits, while adjustable transfers must remain parameterized decision factors. | Fixed-linear transformer factor completion | self-checked |
TR-XFMR-005 — A continuous or discrete scalar winding tap compiles exactly as a retained parameterized transformer factor when coefficientxkc(tap)=tap*basecoefficient_xkc and the decision identity and domain are mapped identically; freezing the tap at its start value is generally only an inner restriction, and in the recorded discrete witness it loses the 1.05 optimum and increases the winding-current objective by 671.060 A. | Parameterized transformer tap decisions | self-checked |
TR-XFMR-006 — A retained finite scalar transformer tap factor embeds exactly into unchanged multiconductor AC voltage, KCL, power-balance, voltage-limit, and recovered leakage-current constraints by pointwise evaluation; in the recorded 11-terminal WYE/WYE/DELTA case, direct source and parameterized target subproblems agree at all three taps, select 0.95 with served fraction 1.2305865, and freezing the 1.00 start loses 0.0601126 served fraction (0.090169 MW). | Transformer tap AC decision case | self-checked |
| Claim | Issue |
|---|
ARCH-BLOCK-001 | Extend to mixed terminal counts, multi-terminal factors, and numerical-zero policies. |
ARCH-CHORDAL-001 | Characterize chordality and minimal fill under missing phases, sparse coupling blocks, parallel factors, multi-terminal devices, and meshed bus graphs. |
ARCH-CONDUCTOR-002 | Compare the scalar terminal lift with a full conductor-terminal factor evaluator and state-conditioned topology maps. |
ARCH-DEGENERACY-001 | Specify utility-data remediation policies for duplicate or indistinguishable switch assets. |
ARCH-DEGENERACY-002 | Connect diagnostics to standards-aware import remediation and quantify restricted-coordinate recovery policies. |
ARCH-FIVEBUS-XFMR-001 | Independently review the layer interfaces and extend the witness to evaluated four- and n-winding factors, non-diagonal reference matrices, connection-specific shunts, controls, and decision-preserving edge realizations. |
ARCH-LENS-001 | Exercise the matrix against version-pinned external imports and independently review the cross-community API terminology. |
ARCH-LOWER-001 | Add a full evaluated multiwinding factor lowerer and independently review equation-preservation conditions. |
ARCH-LOWER-002 | Independently review the four-winding equation-preservation conditions and extend the decision family to richer controls and non-diagonal coupled conductor blocks. |
ARCH-NODAL-001 | Classify identifiable and bounded ambiguity families under realistic line, transformer, shunt, catalog, measurement, and state constraints. |
ARCH-PORT-001 | Lift the data witness to evaluated factor relations and independently review the architecture against a non-synthetic asset model. |
ARCH-PORT-002 | Extend the lift to evaluated factor relations and compare its boundary semantics with the simple quotient and line-identity cycle basis. |
ARCH-RECOVERY-001 | Classify realistic catalog, measurement, grounding, transformer, and state-dependent recovery classes beyond the four finite witnesses. |
ARCH-RECOVERY-002 | Extend the augmented-observation criterion to multiconductor current measurements, nonlinear grounding, transformer controls, and partial observability. |
ARCH-RECOVERY-003 | Extend the rank and partial-observation criterion to noisy measurements, nonlinear operating-point data, coupled transformer ports, and experimental design. |
ARCH-RECOVERY-004 | Extend deterministic bounds to noisy partial observations, structured/passive uncertainty sets, nonlinear operating points, and experiment design. |
ARCH-SUPPORT-001 | Extend the support/stamp distinction to frequency-coupled, rectangular realified, Jacobian, and multi-terminal compiled operator families. |
ARCH-SURGERY-001 | Extend the surgery contract to energized islands, protection states, n-terminal factors, and optimization decisions. |
ARCH-SURGERY-002 | Extend port-selective surgery to coupled conductor bundles, grounding factors, and protection/energization states. |
ARCH-VIEW-001 | Add independent technical review of the house visual grammar and compare additional utility and manufacturer diagram conventions. |
AU-CARSON-001 | Recover the raw CS1035 conductor, screen, earth-return, frequency, and ordering provenance before claiming a faithful reconstruction. |
COLLAPSE-001 | Extend the network witness to controls, phase-specific limits, contingencies, and an independent mathematical review before making a global decision-equivalence claim. |
COLLAPSE-002 | Extend the witness to controls, phase-specific limits, contingencies, and independent mathematical review. |
COUPLED-CORRIDOR-001 | Obtain information-model and protection review; define a machine-readable coupling-group schema and test partial-overlap import round trips. |
COUPLED-CORRIDOR-002 | Independently review the sign/orientation convention; extend the result to block-valued full-pi and singular tableau targets; and separately test limit, state, protection, and optimization-decision preservation. |
DATA-XWALK-001 | The running-fixture contract is checked against pinned documentation profiles; external package imports and file-level round-trip provenance/rating checks remain open. |
FIXTURE-001 | Add an independent fixture reviewer. |
FIXTURE-002 | Re-run with an independent solver where possible. |
FORMULATION-NODAL-001 | Add independent review and extend the witness to controlled, dynamic, and multi-terminal power-network factors. |
FORMULATION-NODAL-002 | Extend the failure-family witness to multiconductor, grounded, state-dependent, and nonlinear formulations with independent review. |
FORMULATION-NODAL-003 | Extend the rank guard to frequency-dependent, singular-shunt, dynamic, and state-dependent compound operators with independent review. |
FORMULATION-Y-SPLIT-001 | Obtain independent review of the source-factor versus study-operator distinction and extend the witness to a generator control and a non-OpenDSS formulation. |
GRAPH-CYCLE-001 | Lift the executable incidence and cycle objects to conductor-terminal graphs, state-conditioned topology decisions, and compiled multi-terminal factors. |
GRAPH-LOOPY-001 | Review whether the book should add a dedicated loopy-Laplacian notation for grounded diagonal terms in future editions. |
GRAPH-MATRIX-001 | Obtain expert review and extend the executable witness to complex block stamps, transformer ratios, and coupled multi-terminal factors without calling the resulting operator a universal graph Laplacian. |
GRAPH-MULTI-001 | Obtain expert graph-theory review of the flag terminology and its relationship to the book's engineering specializations. |
GRAPH-NPORT-001 | Review the incidence/hypergraph/factor-graph terminology across mathematical modeling, circuit, and graph-theory communities and add evaluated n-port examples beyond the existing transformer witnesses. |
GRAPH-PI-COLLAPSE-001 | Extend and independently review the block-coordinate result for multiphase pi factors, transformer maps, singular primitives, and retained branch-current or rating queries. |
GRAPH-SELF-LOOP-001 | Obtain independent terminology review across graph theory, circuit topology, and power-system modeling communities. |
GROUND-SCOPE-001 | Extend the explicit-earth witness to relay curves, CT saturation, richer maintenance decisions, and independent reproduction. |
GROUND-SCOPE-002 | Extend the explicit-earth comparison to relay curves, CT saturation, richer maintenance decisions, and independent reproduction. |
GROUND-SCOPE-003 | Extend to relay curves, CT saturation, richer maintenance decisions, and independent reproduction. |
GROUND-SCOPE-004 | Replace the illustrative functions with standards-aligned relay/CT models and quantify uncertainty and coordination margins. |
IMPEDANCE-LADDER-001 | Reproduce authored overhead-line and underground-cable cases with geometry or linecode provenance, balanced and unbalanced load rows, grounding variants, and an external solver cross-check. |
LIT-PAR-001 | Establish necessary and sufficient redundancy tests for arbitrary multiconductor limits and for state- or decision-dependent line models. |
LLM-RETRIEVAL-001 | Rerun both pinned candidates on the current corpus and evaluate domain-adapted alternatives before making a current or general neural-retrieval comparison. |
LOAD-BASE-001 | Extend the definition and executable guardrail to arbitrary unbalanced terminal maps, nonstandard connection families, explicit unit provenance, and independently reviewed importer crosswalks. |
LOAD-CONNECTION-001 | Extend connection-map evidence to unbalanced multiconductor loads, explicit grounding, phase-specific ratings, and network-level decision solves. |
LOAD-CONTINUATION-001 | Replace the iteration-failure boundary with a mathematically continued nose curve, add independent solver continuation, and extend to multiconductor/network-level decisions. |
LOAD-DECISION-001 | Add multiconductor connection maps and continuation to collapse points; the declared scalar CP/CI/CZ/ZIP fixture now has separately varying reactive coefficients and an independent reproduction. |
NUMERICAL-001 | Extend the current five-bus structural witness to a pinned running-network benchmark with solver-exported Ybus/Jacobian sparsity, ordering-dependent fill, and recovered decision-margin checks. |
NUMERICAL-002 | Add an independent KKT/Jacobian export and compare ordering-dependent fill and decision margins across source and reduced views. |
NUMERICAL-003 | The public BMOPFTools checked-KKT callback now runs through DiffOpt on a minimal parameterized OPF and agrees with finite difference; a native JuMP/MOI Jacobian structure is now recorded, while solver-private KKT rows, ordering, and factorization statistics remain outside the public boundary. |
NUMERICAL-004 | Extend the initial bus-result contract to equation residuals, device limits, power balance, objective and global-optimality evidence, and independent solver reproduction. |
NUMERICAL-005 | Extend the witness schema with model-specific equation coverage, scaling/backward-error metadata, and independent recomputation adapters. |
PRACTICE-ADAPTER-001 | Compare the contract against additional utility, CIM/CGMES, OpenDSS, and solver-native adapters with external domain review. |
PRACTICE-ARCH-001 | Compare the implementation contract with an independently reviewed package boundary and broader source-data adapters. |
PRACTICE-DUAL-001 | No AC-OPF locational-price, generic solver dual convention, nonlinear sensitivity or uniqueness guarantee is established. |
PRACTICE-IMPEDANCE-001 | Exercise the contract on source-backed overhead and underground construction records and obtain independent power-engineering review. |
PRACTICE-IMPORT-001 | Independent review and complete versioned importer/exporter coverage remain outside the field-level teaching witness. |
PRACTICE-UPDATE-001 | This disproves one update rule; it neither rules out source-aware incremental updates nor establishes general nonlinear, multiconductor or constrained update correctness. |
PRESERVE-001 | Obtain independent review of the observation-indexed equivalence vocabulary and connect it to additional solver interfaces. |
RATING-001 | Map selected utility and software rating fields into the typed limit record. |
TOPOLOGY-001 | Add a generated node–breaker fixture with open, closed, and unknown switch states. |
TR-COMP-001 | Prove associativity modulo certificate serialization and strengthen compatibility checks beyond object identity. |
TR-COORD-001 | Add an independent mathematical reviewer and extend coordinate actions to general input/output tensors. |
TR-GRAPH-001 | Extend the executable invariant checks to conductor-terminal incidence and state-indexed multi-terminal factors. |
TR-GRAPH-002 | Add active-state radiality certificates with open/closed switches, outages, and multi-terminal compilation choices. |
TR-GRAPH-ACTIVE-001 | Extend the active-state witness to switching, outages, and energized-state uncertainty on the canonical multiconductor fixture. |
TR-GRAPH-SIMPLIFY-001 | Obtain independent proof review and add property-based checks over randomized finite multigraphs and application-specific weighted-query contracts. |
TR-KRON-001 | The 2026-08-15 automated independent re-derivation verified dense partition actions, reciprocity distinctions, and the fixed-injection scope but is not human peer review; extend the fixture to randomized and terminal-permutation campaigns and obtain a named mathematical review. |
TR-KRON-002 | Replace the illustrative target-selection family with a source-faithful Opti-KRON implementation and extend observations to voltage, constraints, decisions, and topology guards. |
TR-KRON-003 | Extend the chain to a nonlinear AC decision model, parameter uncertainty, and independent error analysis before treating it as a general certification theorem. |
TR-KRON-FIVE-001 | Extend the direct fixture check to non-pendant eliminations, retained branch limits, shunts, and multiconductor internal states. |
TR-KRON-FIVE-002 | Extend the fill-in witness to multiconductor blocks, retained branch limits, shunts, and ordering-dependent numerical factorization diagnostics. |
TR-KRON-NEUTRAL-001 | Extend the neutral-current recovery contract from the linear shunt probe to nonlinear loads, explicit earth-return factors, and general neutral/grounding reductions; the series and shunt probes have independent reproductions. |
TR-KRON-NEUTRAL-002 | Extend to nonlinear earth-return factors, multiple grounding points, protection observations, and independent physical-model review. |
TR-KRON-NEUTRAL-003 | Extend to nonlinear and state-dependent grounding, grounding impedance uncertainty, protection observations, and physical-model review. |
TR-KRON-NEUTRAL-004 | Extend to uncertainty sets, nonlinear/state-dependent grounding, protection observations, and physical-model review. |
TR-KRON-NEUTRAL-005 | Extend to global continuation, multiple nonlinear grounding points, uncertainty sets, protection observations, and physical-model review. |
TR-KRON-NEUTRAL-006 | Extend to global continuation, more nonlinear grounding points, uncertainty sets, protection observations, and physical-model review. |
TR-KRON-NEUTRAL-007 | Extend to adaptive continuation, global branch tracking, uncertainty sets, protection observations, and physical-model review. |
TR-KRON-NEUTRAL-008 | Extend local derivative bounds to adaptive/global continuation, nonlinear multi-point grounding, noisy observations, and physical-model review. |
TR-NEG-001 | Extend the negative cases to nominal-pi cascades, protection boundaries, nonlinear formulations, and independent reproduction. |
TR-PAR-001 | Add an independent mathematical reviewer. |
TR-PAR-002 | Molzahn2018 gives an exact scalar AC constraint-pruning test without asset aggregation; a general multiconductor classification remains open. |
TR-PAR-003 | The multiconductor mechanism is exercised in TR-PAR-004; add an independent reviewer for this linear case. |
TR-PAR-004 | The 2026-08-15 automated independent re-derivation reproduces the closed-form values, relaxation, pruning, and binding-current interpretation but is not human peer review; extend the result to near-proportional/non-proportional members, global nonlinear optimality, and independently reviewed physical cases. |
TR-PAR-005 | Extend from pairwise implications to constraints jointly implied by multiple retained limits, then condition certificates on topology, controls, outages, investments, and non-Euclidean thermal regions. |
TR-PAR-006 | TR-PAR-007 covers nonsingular nominal-pi primitives; the companion certificate now refuses singular and singular-shunted recovery maps. Extend from that refusal boundary to exact singular reductions, several retained members, state-dependent topology and controls, and obtain an independent global optimality bound where required. |
TR-PAR-007 | The certificate now includes singular-shunted refusal and voltage-dependent recomputation probes. Extend from these guards to exact singular reductions, voltage-dependent nonlinear decision models, several retained members, topology and control states, and global AC optimality bounds where required. |
TR-PAR-AC-JOINT-001 | Extend beyond this fixed linear member relation to voltage-dependent shunts, topology/control states, several independently varying retained members, and global nonlinear AC optimality guarantees. |
TR-PAR-JOINT-001 | Extend the joint-support certificate to full nonlinear AC cases with several retained members, state-dependent maps, topology decisions, and global optimality bounds. |
TR-PAR-SINGULAR-001 | Extend the reduced-coordinate treatment to singular shunted primitives, coupled conductor models, and global nonlinear AC decision bounds. |
TR-PAR-STATE-001 | Extend from the finite scalar and phase-selective envelope to topology/control states, independently varying recovery maps, global nonlinear optimality, and external physical-model review. |
TR-SER-001 | The 2026-08-15 automated independent re-derivation found and motivated the repaired coupling guard but is not human peer review; add a named mathematical reviewer for the uncoupled rule and its coupling boundary. |
TR-SER-002 | Formalize sufficient physical line-merge guards for selected line models. |
TR-SER-003 | Add an independent mathematical reviewer; determine model-specific reciprocity and physical line-class closure guards. |
TR-XFMR-001 | Prove which normalized factors can be serialized back into compact vector-group and delta-roll fields without loss. |
TR-XFMR-002 | Add an independent transformer-model review and establish compact serialization contracts that preserve the declared source and compilation references. |
TR-XFMR-003 | Independently review the fixed and parameterized completions and test tap-dependent leakage or excitation models. |
TR-XFMR-004 | Independently review the completion and test phase-angle controls, tap-dependent leakage, and total-current or apparent-power ratings. |
TR-XFMR-005 | The first solver-backed network embedding is TR-XFMR-006; extend the contract to phase-angle, independent per-phase, mechanically coupled, and tap-dependent-loss controls. |
TR-XFMR-006 | TR-XFMR-007 independently reproduces the numerical branch search, and the certificate now includes a finite two-scenario tap-pair switching-cost ledger; extend the network-level contract to unbalanced downstream controls and richer multiwinding decisions. |
TR-XFMR-007 | The finite tap-pair ledger is branch-complete for its declared domain, but the continuous subproblems remain local Ipopt solutions; reproduce the case with an independently assembled transformer primitive or external power-system tool and establish global guarantees where required. |
TR-XFMR-008 | This is a finite local witness, not a global unbalanced OPF guarantee; extend the contract to richer multiwinding controls, topology decisions, and independently assembled physical models. |
TR-XFMR-009 | This remains a finite local path witness, not a global unbalanced multi-period OPF guarantee; extend to richer controls, topology decisions, switching operation limits, and independently assembled physical models. |
TR-XFMR-010 | Extend operation-count, dwell-time, deadband, and switching-cost semantics to richer multiwinding controls and globally certified multi-period OPF models. |
TRANSFORM-CATALOG-001 | Attach executable certificates to the remaining catalogue rows and review rewrite-system termination, critical-pair, and confluence conditions. |
TRANSFORM-SEM-001 | Add independently reviewed formal signatures for closure and composition across larger transformation families. |
VOCAB-BRIDGE-001 | Obtain terminology review from representatives of power engineering, software and network data, mathematical modelling, graph theory, and graph machine learning. |
These retrieval facets are provisional and path-derived. They are navigation aids, not additional verification labels; explicit facet fields can replace them when the claims schema is normalised.
| Claim | Chapter | Type |
|---|
AU-CARSON-001 — The Australian Carson reproduction regenerates overhead and underground multiconductor primitives from lifted construction inputs, compares them with independent OpenDSS reference matrices, and identifies the CS1035 construction mapping as unresolved rather than presenting it as a faithful reproduction. | Australian construction inputs: Carson and OpenDSSDirect | empirical |
COUPLED-CORRIDOR-001 — Physically parallel line sections need not be parallel in the bus multigraph; a source model can retain stable line assets plus oriented section-to-section coupling records, with each connected coupling group compiling into one joint electrical factor before inversion or nodal stamping. | A coupled multi-voltage corridor | proposal |
COUPLED-CORRIDOR-002 — For two fixed linear reciprocal scalar series sections with a nonsingular joint impedance matrix, AGamma^T ZGamma^{-1} AGamma has an exact six-edge weighted-lattice realization on the four source terminals; source section currents are recovered by ZGamma^{-1} A_Gamma u, while the generated cross edges carry no asset or galvanic interpretation. | A coupled multi-voltage corridor | theorem |
FIXTURE-001 — Running-network fixture v0.1.0 passes the current BMOPFTools JSON schema and conformance checks without errors or warnings. | Executable running network | empirical |
FIXTURE-002 — The v0.1.0 continuous PF and OPF instances terminate locally solved in the recorded environment. | Executable running network | empirical |
IMPEDANCE-LADDER-001 — In the deterministic four-wire impedance ladder fixture, phase-to-neutral current and voltage recovery are exact under the declared zero-ground-current map, while the deliberately non-circulant reduced matrix has visible sequence mixing; shunt deletion and positive-sequence use therefore require explicit decision-domain guards. | Four-wire impedance-model ladder | empirical |
LOAD-BASE-001 — A voltage-dependent load's nominal voltage is an anchor in the load factor's declared terminal coordinate: WYE uses phase-to-neutral voltage and DELTA uses line-to-line voltage; copying one numeric bus voltage into both coordinates without an explicit base conversion changes the normalized load law. | Load models and decision dependence | definition |
LOAD-CONNECTION-001 — On the recorded balanced three-phase terminal fixture, explicit wye phase-to-neutral and delta phase-to-phase connection maps share the same bus and graph but produce different load-voltage observations: unit-magnitude wye voltages and sqrt(3)-magnitude delta voltages. | Load models and decision dependence | empirical |
LOAD-CONTINUATION-001 — On the recorded scalar two-bus continuation probe, the damped CP branch first fails to converge at demand scale 1.8 after a converged scale 1.7, while CI, CZ, and the declared ZIP branch remain converged through scale 3.0; this is an iteration-scoped branch diagnostic, not a global collapse theorem. | Load models and decision dependence | empirical |
LOAD-DECISION-001 — On the recorded two-bus fixture, CP, CI, CZ, and a normalized ZIP load law share the same bus–branch graph but produce distinct high-voltage solutions and decision margins: CP violates both the declared voltage and current limits, while CI, CZ, and ZIP satisfy both. | Load models and decision dependence | empirical |
PRACTICE-DUAL-001 — For min betacp subject to alpha(d-p)<=0 with positive c,d,alpha,beta, dispatch remains p=d while the Lagrange multiplier is betac/alpha and physical marginal cost is alpha/beta times that multiplier; duplicating the unscaled constraint admits nonunique multiplier allocations summing to c. | Building and changing a model you can check | theorem |
PRACTICE-IMPORT-001 — A numerical round trip of MATPOWER RATE_A=0 can succeed while a faulty decoder replaces its explicit unlimited-rating meaning with a finite zero bound, changing the admissible transfer set. | Building and changing a model you can check | theorem |
PRACTICE-UPDATE-001 — Opening one arm of a three-arm 1 S resistive star changes the remaining two-terminal equivalent conductance to 1/2 S; deleting the two corresponding edges of the original 1/3 S reduced triangle incorrectly leaves 1/3 S, despite symmetry and zero row sums. | Building and changing a model you can check | theorem |
TR-PAR-001 — Summed admittance preserves the unconstrained terminal relation of parallel linear branches. | A plausible model gives the wrong answer | theorem |
TR-PAR-002 — Using the sum of member current ratings can create an outer relaxation of the member-constrained feasible set. | A plausible model gives the wrong answer | theorem |
TR-PAR-003 — In the recorded two-bus maximum-served-load problem, the naive summed-rating aggregate serves 200 MW while the source and exact lifted formulations each serve 110 MW. | A plausible model gives the wrong answer | empirical |
TR-PAR-004 — In the recorded two-conductor AC maximum-served-load case, the source, exact lifted, and certified exact-pruned formulations have objective 0.6138908, while a summed-limit aggregate has objective 1.0630833 and violates a 0.6 p.u. member limit. | Multiconductor parallel AC decision case | empirical |
TR-PAR-005 — For fixed linear complex terminal-current maps with centered Euclidean norm limits, one normalized constraint implies another if and only if the retained normalized real quadratic form minus the candidate form is positive semidefinite; applying this pairwise test to every aligned conductor and both terminal ends certifies exact candidate-limit pruning while retaining both member models. | Multiconductor parallel AC decision case | theorem |
TR-PAR-006 — For nonsingular fixed series admittances on common multiconductor endpoint coordinates, candidate component currents recover as Il2=(Yl2/Yl1)Il1, and the exact maximum of candidate component c over all retained component-current discs is sumk abs(Kck) Imax_l1k; in the recorded reciprocal non-proportional three-phase four-wire AC case this certifies all l2 limits redundant, the exact-pruned and source objectives agree at 1.1274329, and a summed-limit aggregate reaches 1.8058181 by violating an l1 limit. | Non-proportional three-phase four-wire parallel case | theorem |
TR-PAR-007 — For fixed nominal-pi multiconductor members whose retained full two-end terminal-current primitive Ar is nonsingular, all candidate terminal currents recover as Ac*inv(Ar) times the retained terminal-current vector, so exact complex-polydisc row norms certify joint implication across both line ends; in the recorded non-proportional four-wire case, pruning eight member-2 limits preserves the 1.1286205 source objective while a same-size summed-limit model reaches 1.8077114 by violating member 1. | Four-wire nominal-pi parallel case | theorem |
TR-PAR-AC-JOINT-001 — In the recorded three-member four-wire AC case, member 3 has the fixed recovery Il3=0.10 Il1+0.10 I_l2 and a 0.15 p.u. component limit; the joint support bound is 0.144 p.u., so deleting member-3 limits preserves the locally solved source objective 1.2401762 to 7e-14. An independent damped-Newton continuation and bisection reproduces the source boundary within 1.3e-8 served-fraction units. | Four-wire nominal-pi parallel case | empirical |
TR-PAR-JOINT-001 — For fixed series current maps in common endpoint-voltage-drop coordinates, a candidate component-current limit is implied by several retained member limits when its exact recovery row has support bound sumk abs(Kck) Ibar_k no larger than the candidate rating; the guarded witness certifies this joint implication for three retained discs. | Four-wire nominal-pi parallel case | theorem |
TR-PAR-SINGULAR-001 — For the declared series-only singular four-wire fixture, the full two-end terminal-current map is rank deficient, but the endpoint-voltage-drop coordinate recovers member-2 currents exactly from member-1 currents through the declared diagonal map, with the zero-neutral rows retained as an explicit invariant; this is a guarded reduced-coordinate result, not a pseudoinverse or singular-shunt theorem. | Four-wire nominal-pi parallel case | empirical |
TR-PAR-STATE-001 — In the recorded finite four-state four-wire AC envelope, rebuilding the member maps and source/pruned formulations at each declared scalar or phase-selective admittance state preserves exact joint limit pruning locally while changing the optimal served value across states. | Four-wire nominal-pi parallel case | empirical |
TR-XFMR-001 — A transformer winding terminal permutation is an exact typed-factor normalization when its complete terminal-to-coil incidence relation is right-multiplied by the inverse permutation and coil coordinates remain fixed. | Transformer-winding coordinate normalization | theorem |
TR-XFMR-002 — Complete pairwise multiwinding short-circuit impedances compile exactly into a reference-coordinate impedance matrix ZB, from which every pairwise impedance is recoverable; changing the selected reference winding leaves the external winding admittance invariant, and the classical star/T representation is the three-winding special case. | Multiwinding leakage reference compilation | theorem |
TR-XFMR-003 — Aligned winding connection-incidence factors compose exactly with a multiwinding leakage admittance as Yterminal=A'(Yw kron I)A; retaining the coil-current map preserves per-coil winding limits and makes terminal-coordinate and leakage-reference changes explicit coordinate actions. | Multiwinding terminal leakage assembly | theorem |
TR-XFMR-004 — A fixed linear transformer completion with declared voltage transfer T, leakage map B=TA, excitation placement S, and transformer-internal grounding has terminal admittance Ycomplete=B^HYcoilB+S^TY0*S+Yground; the power-dual and component-current recovery maps preserve the declared leakage-path limits, while adjustable transfers must remain parameterized decision factors. | Fixed-linear transformer factor completion | theorem |
TR-XFMR-005 — A continuous or discrete scalar winding tap compiles exactly as a retained parameterized transformer factor when coefficientxkc(tap)=tap*basecoefficient_xkc and the decision identity and domain are mapped identically; freezing the tap at its start value is generally only an inner restriction, and in the recorded discrete witness it loses the 1.05 optimum and increases the winding-current objective by 671.060 A. | Parameterized transformer tap decisions | theorem |
TR-XFMR-006 — A retained finite scalar transformer tap factor embeds exactly into unchanged multiconductor AC voltage, KCL, power-balance, voltage-limit, and recovered leakage-current constraints by pointwise evaluation; in the recorded 11-terminal WYE/WYE/DELTA case, direct source and parameterized target subproblems agree at all three taps, select 0.95 with served fraction 1.2305865, and freezing the 1.00 start loses 0.0601126 served fraction (0.090169 MW). | Transformer tap AC decision case | theorem |
TR-XFMR-007 — A separate damped finite-difference Newton, continuation, and bisection implementation reproduces all three TR-XFMR-006 tap-conditioned high-voltage branch boundaries without an external optimizer; its largest served-fraction difference from JuMP/Ipopt is 3.14e-10, and both methods select tap 0.95. | Transformer tap AC decision case | empirical |
TR-XFMR-008 — In the recorded 11-terminal WYE/WYE/DELTA tap case, a phase-selective unbalanced second scenario can be handled without collapsing the transformer or its phase identities: exact enumeration of the nine ordered tap pairs preserves branch completeness and exposes the per-phase scenario directions explicitly. | Transformer tap AC decision case | empirical |
TR-XFMR-009 — For the recorded 11-terminal WYE/WYE/DELTA case, a three-scenario phase-selective tap path can be enumerated exactly over the 3^3 ordered tap triples, with consecutive tap movement charged explicitly and each scenario retaining its own phase directions. | Transformer tap AC decision case | empirical |
TR-XFMR-010 — In the recorded three-scenario tap path, enumerating all 27 ordered tap triples and then applying an explicit at-most-one-movement policy leaves 15 admissible branches; the policy is a decision constraint and must not be inferred from the unconstrained best path. | Transformer tap AC decision case | empirical |
| Claim | Chapter | Type |
|---|
ARCH-FIVEBUS-XFMR-001 — In the recorded five-bus structural extension, one three-port transformer has acyclic local factor-incidence and star realizations, while eliminating the virtual star point generically yields a terminal clique with cycle rank one; the embedded factor-incidence and star member ranks coincide at five despite carrying different semantics, while the clique member rank is six, without implying additional physical transformer loops. | Five buses through a multi-port lowering | empirical |
ARCH-LOWER-002 — A four-winding transformer factor can be compiled pointwise into a complete terminal equation operator while retaining a full non-diagonal reference impedance, mixed winding connection maps, connection-specific shunts, internal grounding, recovery maps, and an explicit finite tap/phase decision domain; this does not by itself provide a source-faithful ordinary-edge realization. | Five buses through a multi-port lowering | theorem |
GRAPH-CYCLE-001 — The recorded connected five-bus bus–branch multigraph has seven identified lines, incidence rank four, and cycle-space dimension three; collapsing its parallel q/r pair to a simple edge reduces the cycle-space dimension to two, whereas the spanning-tree-plus-chords representation retains all three source dimensions. | A five-bus multigraph: identities, cycles, and tree coordinates | theorem |
GRAPH-LOOPY-001 — Network-reduction and microgrid-stability literature uses loopy-Laplacian self-loop terms for grounded or differential-conductance diagonal effects; that matrix-level usage is distinct from the book's ordinary graph-loop convention with a zero signed-incidence column. | Multigraphs for expert modelers | definition |
GRAPH-MATRIX-001 — Under the declared convention Auv equals non-loop edge multiplicity off diagonal, Avv equals twice the graph-loop count, and D contains incidence degrees, so D-A equals B B transpose; graph-loop columns vanish from signed incidence while a grounded shunt contributes a distinct diagonal constitutive term. | Multigraphs for expert modelers | theorem |
GRAPH-MULTI-001 — The book's finite undirected multigraph is an identified edge-and-flag object in which every edge owns exactly two distinct flags; loops have two flags incident to one vertex, parallel members retain distinct edge identities, and attributes remain typed maps rather than being inferred from adjacency. | Multigraphs for expert modelers | definition |
GRAPH-NPORT-001 — Allowing a relation to own an arbitrary finite flag fibre generalizes the two-uniform multigraph to an incidence structure, while an expert mathematical model additionally needs typed flag spaces, relation roles or ordering, and a constitutive relation to represent an n-port factor rather than merely its hypergraph incidence. | Multigraphs for expert modelers | definition |
GRAPH-PI-COLLAPSE-001 — For a fixed linear two-terminal pi factor with series admittance Ys and endpoint shunts Ya and Yb, identifying both terminals through the common attachment map Tpi=[1,1]^T gives Tpi^T Ypi Tpi=Ya+Y_b, so the series contribution cancels and the exact nodal image is a one-terminal constant-admittance shunt under the declared coordinate and reference assumptions. | Multigraphs for expert modelers | theorem |
GRAPH-SELF-LOOP-001 — In the book's loopless bus–branch circuit specialization, ordinary edges connect distinct retained circuit nodes; a graph self-loop may remain in the source multigraph or arise from a topology quotient, but it is not interchangeable with an electrical circuit loop or mesh, a grounded shunt, or a diagonal self-admittance term. | Multigraphs for expert modelers | definition |
TR-GRAPH-001 — For a loopless identified multigraph and its simple endpoint projection, the multigraph cycle rank exceeds the simple-graph cycle rank by the sum over edge fibres of fibre size minus one; the lost dimensions are line-identity cycles supported on parallel fibres. | Cycles, parallelism, and radial structure | theorem |
TR-GRAPH-002 — An identified line is a multigraph bridge exactly when its simple endpoint edge is a bridge and its parallel fibre is a singleton; consequently the identified multigraph is a forest exactly when its simple projection is a forest and every edge fibre is a singleton. | Cycles, parallelism, and radial structure | theorem |
TR-GRAPH-ACTIVE-001 — For the five-bus fixture, the inventory has identified-member cycle rank 3 and simple-projection cycle rank 2, while the declared spanning tree is radial at both levels; active radiality is therefore a state-specific property, not an inventory-only label. | Cycles, parallelism, and radial structure | empirical |
TR-PAR-001 — Summed admittance preserves the unconstrained terminal relation of parallel linear branches. | A plausible model gives the wrong answer | theorem |
TR-PAR-002 — Using the sum of member current ratings can create an outer relaxation of the member-constrained feasible set. | A plausible model gives the wrong answer | theorem |
TR-PAR-003 — In the recorded two-bus maximum-served-load problem, the naive summed-rating aggregate serves 200 MW while the source and exact lifted formulations each serve 110 MW. | A plausible model gives the wrong answer | empirical |
TR-PAR-004 — In the recorded two-conductor AC maximum-served-load case, the source, exact lifted, and certified exact-pruned formulations have objective 0.6138908, while a summed-limit aggregate has objective 1.0630833 and violates a 0.6 p.u. member limit. | Multiconductor parallel AC decision case | empirical |
TR-PAR-005 — For fixed linear complex terminal-current maps with centered Euclidean norm limits, one normalized constraint implies another if and only if the retained normalized real quadratic form minus the candidate form is positive semidefinite; applying this pairwise test to every aligned conductor and both terminal ends certifies exact candidate-limit pruning while retaining both member models. | Multiconductor parallel AC decision case | theorem |
TR-PAR-006 — For nonsingular fixed series admittances on common multiconductor endpoint coordinates, candidate component currents recover as Il2=(Yl2/Yl1)Il1, and the exact maximum of candidate component c over all retained component-current discs is sumk abs(Kck) Imax_l1k; in the recorded reciprocal non-proportional three-phase four-wire AC case this certifies all l2 limits redundant, the exact-pruned and source objectives agree at 1.1274329, and a summed-limit aggregate reaches 1.8058181 by violating an l1 limit. | Non-proportional three-phase four-wire parallel case | theorem |
TR-PAR-007 — For fixed nominal-pi multiconductor members whose retained full two-end terminal-current primitive Ar is nonsingular, all candidate terminal currents recover as Ac*inv(Ar) times the retained terminal-current vector, so exact complex-polydisc row norms certify joint implication across both line ends; in the recorded non-proportional four-wire case, pruning eight member-2 limits preserves the 1.1286205 source objective while a same-size summed-limit model reaches 1.8077114 by violating member 1. | Four-wire nominal-pi parallel case | theorem |
TR-PAR-AC-JOINT-001 — In the recorded three-member four-wire AC case, member 3 has the fixed recovery Il3=0.10 Il1+0.10 I_l2 and a 0.15 p.u. component limit; the joint support bound is 0.144 p.u., so deleting member-3 limits preserves the locally solved source objective 1.2401762 to 7e-14. An independent damped-Newton continuation and bisection reproduces the source boundary within 1.3e-8 served-fraction units. | Four-wire nominal-pi parallel case | empirical |
TR-PAR-JOINT-001 — For fixed series current maps in common endpoint-voltage-drop coordinates, a candidate component-current limit is implied by several retained member limits when its exact recovery row has support bound sumk abs(Kck) Ibar_k no larger than the candidate rating; the guarded witness certifies this joint implication for three retained discs. | Four-wire nominal-pi parallel case | theorem |
TR-PAR-SINGULAR-001 — For the declared series-only singular four-wire fixture, the full two-end terminal-current map is rank deficient, but the endpoint-voltage-drop coordinate recovers member-2 currents exactly from member-1 currents through the declared diagonal map, with the zero-neutral rows retained as an explicit invariant; this is a guarded reduced-coordinate result, not a pseudoinverse or singular-shunt theorem. | Four-wire nominal-pi parallel case | empirical |
TR-PAR-STATE-001 — In the recorded finite four-state four-wire AC envelope, rebuilding the member maps and source/pruned formulations at each declared scalar or phase-selective admittance state preserves exact joint limit pruning locally while changing the optimal served value across states. | Four-wire nominal-pi parallel case | empirical |
| Claim | Chapter | Type |
|---|
ARCH-BLOCK-001 — For a declared two-bus four-conductor linear factor, the vector-edge, port-factor, block nodal, scalar-support, and realified-coordinate views are related representations of one assembled relation; coordinate expansion and realification do not create physical assets, while factor identity remains separate provenance. | How to read power-network diagrams and equations | empirical |
ARCH-CHORDAL-001 — For a simple bus-level tree with a common m-coordinate block at every bus and a structurally dense two-terminal stamp on every tree edge, the scalar structural-support graph is chordal and leaf-bus block elimination is a zero-fill perfect elimination ordering. | Two topology levels and the nodal projection | theorem |
ARCH-CONDUCTOR-002 — The five-bus scalar line-identity fixture lifts to fourteen scalar endpoint ports, five terminal junctions, and seven two-port line factors; the lift retains the q/r parallel fibre and its extra cycle dimension while adding no multiconductor, switch, or transformer semantics. | Formal representation frameworks | empirical |
ARCH-DEGENERACY-001 — Duplicate ideal switches with identical terminal sets and state domains have a well-defined electrical connectivity quotient but an unresolved asset-attribution relation; the model should retain both identities and emit a diagnostic rather than invent protection, maintenance, or failure ownership. | From source graphs to views and graph surgery | proposal |
ARCH-DEGENERACY-002 — The book proposes that missing grounding/reference declarations and rank-deficient active-state maps be treated as model-quality diagnostics; a compiler should refuse to infer a reference or invert a singular map without an additional declaration or restricted coordinate query. | From source graphs to views and graph surgery | proposal |
ARCH-FIVEBUS-XFMR-001 — In the recorded five-bus structural extension, one three-port transformer has acyclic local factor-incidence and star realizations, while eliminating the virtual star point generically yields a terminal clique with cycle rank one; the embedded factor-incidence and star member ranks coincide at five despite carrying different semantics, while the clique member rank is six, without implying additional physical transformer loops. | Five buses through a multi-port lowering | empirical |
ARCH-LENS-001 — A layer–lens matrix can attach concrete data, optimization, sparse-matrix, and graph-learning interfaces to different construction stages without treating software packages as representation levels; each attachment must declare preserved and omitted semantics. | Maps between representation frameworks | proposal |
ARCH-LOWER-001 — A typed lowering from an identity-bearing n-port source graph to ordinary-edge incidence objects may preserve a declared equation relation while forgetting factor identity unless source fibres and provenance are retained. | From source graphs to views and graph surgery | theorem |
ARCH-LOWER-002 — A four-winding transformer factor can be compiled pointwise into a complete terminal equation operator while retaining a full non-diagonal reference impedance, mixed winding connection maps, connection-specific shunts, internal grounding, recovery maps, and an explicit finite tap/phase decision domain; this does not by itself provide a source-faithful ordinary-edge realization. | Five buses through a multi-port lowering | theorem |
ARCH-NODAL-001 — Assembly of typed linear factor stamps into a compound nodal operator is not generally injective: distinct admissible parallel-factor decompositions can produce an identical nodal operator and identical normalized assembly residuals. | Two topology levels and the nodal projection | theorem |
ARCH-PORT-001 — A minimal executable port–factor bundle instantiated from the running network validates typed port-to-junction and port-to-factor incidence, a three-port multiwinding factor, grounding as an explicit factor, and a many-to-many asset/electrical relation Λ. | Formal representation frameworks | empirical |
ARCH-PORT-002 — The five-bus identified scalar multigraph has a direct structural port–factor lift with five bus junctions, seven two-port scalar line factors, fourteen endpoint ports, and one asset-to-factor relation per identified line; parallel members q and r remain distinct factors despite sharing the same bus pair. | Formal representation frameworks | empirical |
ARCH-RECOVERY-001 — Source recovery from a compound nodal operator is class-dependent: support-separated single-factor classes can be identifiable, over-parameterized classes can be set-identifiable at the terminal-primitive level, and parallel multiplicity or eliminated internal coordinates can be non-identifiable; a recovery interface must report the status and ambiguity rather than infer asset identity. | Two topology levels and the nodal projection | theorem |
ARCH-RECOVERY-002 — Auxiliary observations and declarations lift source-recovery ambiguity only through their joint observation map: catalog bounds may produce a compact but non-singleton feasible set, whereas member-current measurements, explicit grounding attribution, or a declared transformer state can make the restricted map injective in a scoped model class. | Two topology levels and the nodal projection | theorem |
ARCH-RECOVERY-003 — For a matrix-valued multiconductor factor observed through member-current snapshots, full primitive recovery requires voltage snapshots spanning the retained conductor space and coverage of every current coordinate; single-snapshot or phase-selective observations retain reciprocal ambiguity even when the assembled nodal operator is known. | Two topology levels and the nodal projection | theorem |
ARCH-RECOVERY-004 — For noisy full-rank multiconductor voltage/current snapshots, the pseudoinverse source estimate has a deterministic Frobenius error bound proportional to the noise radius and the voltage-snapshot pseudoinverse norm; nearly dependent excitation therefore enlarges the certified uncertainty set even when the observation map is full rank. | Two topology levels and the nodal projection | theorem |
ARCH-SUPPORT-001 — Block and scalar nonzero-support graphs of a declared compound nodal operator are simple graphs by construction, while the identified factor-stamp decomposition is separate data and may be a multigraph. | Two topology levels and the nodal projection | theorem |
ARCH-SURGERY-001 — The book proposes that state-conditioned graph surgery return state-indexed graphs or graph families with diagnostics and provenance; for many unknown switches, a three-valued certain-connected/certain-separated/undetermined summary should be available instead of silently collapsing to one active graph. | From source graphs to views and graph surgery | proposal |
ARCH-SURGERY-002 — The book proposes that an n-terminal surgery retain port-coordinate identity and return port-specific active and isolated sets; it cannot be inferred by replacing an n-port factor with implicit pairwise edges. | From source graphs to views and graph surgery | proposal |
ARCH-VIEW-001 — The book proposes that a power-network visualisation declare its object level, preserved and forgotten semantics, identity fibres, and reverse-map status; single-line, multi-line, port-factor, node-breaker, nodal-support, and reduced views are distinct typed projections. | From source graphs to views and graph surgery | proposal |
COLLAPSE-001 — Under compatible three-phase terminals, cyclic (circulant) series and shunt matrices, balanced boundary data, sequence-compatible grounding, two-terminal factor closure, phase-symmetric decisions, and positive-sequence observations, the general phase-domain relation restricts exactly to the positive-sequence scalar network. | When the general model collapses | theorem |
COLLAPSE-002 — The generated Fortescue witness diagonalizes a circulant three-phase impedance matrix and preserves the positive-sequence subspace, while a non-circulant perturbation produces sequence mixing and a positive-subspace residual. | When the general model collapses | empirical |
DATA-XWALK-001 — CIM/CGMES, PowerModelsDistribution, OpenDSS, and MATPOWER provide distinct partial correspondences to the book's asset, terminal, topology, factor, state, and rating objects; successful import is not by itself semantic or decision equivalence. | Data-model crosswalk | practice |
FORMULATION-NODAL-001 — An ideal voltage source with a queried source current is not representable by a plain nodal-admittance injection without adding an extra current variable or changing the query contract; a modified-nodal or tableau formulation preserves the voltage constraint and current observation. | Circuit formulations and the lowering boundary | theorem |
FORMULATION-NODAL-002 — Even when a nodal operator can be assembled, it may be singular without a declared reference or shunt, or semantically insufficient for member-level limits: aligned parallel factors can share one aggregate admittance while having different member currents and feasible limits. | Circuit formulations and the lowering boundary | theorem |
FORMULATION-NODAL-003 — A declared reference or grounding label does not by itself establish nonsingularity of a compound nodal operator: the rank guard must be evaluated on the assembled operator after the declared reference, grounding, and active-state maps are applied. | Circuit formulations and the lowering boundary | theorem |
FORMULATION-Y-SPLIT-001 — A load or generator may be represented as a factor attached to a source network while a declared study formulation places a constant-admittance, Norton, or other linearized part in the nodal operator and retains the remainder as an injection, control, limit, or decision relation; the resulting nodal matrix is therefore mode-, state-, and linearization-qualified rather than a unique graph of the source system. | Circuit formulations and the lowering boundary | definition |
GRAPH-LOOPY-001 — Network-reduction and microgrid-stability literature uses loopy-Laplacian self-loop terms for grounded or differential-conductance diagonal effects; that matrix-level usage is distinct from the book's ordinary graph-loop convention with a zero signed-incidence column. | Multigraphs for expert modelers | definition |
GRAPH-MATRIX-001 — Under the declared convention Auv equals non-loop edge multiplicity off diagonal, Avv equals twice the graph-loop count, and D contains incidence degrees, so D-A equals B B transpose; graph-loop columns vanish from signed incidence while a grounded shunt contributes a distinct diagonal constitutive term. | Multigraphs for expert modelers | theorem |
GRAPH-MULTI-001 — The book's finite undirected multigraph is an identified edge-and-flag object in which every edge owns exactly two distinct flags; loops have two flags incident to one vertex, parallel members retain distinct edge identities, and attributes remain typed maps rather than being inferred from adjacency. | Multigraphs for expert modelers | definition |
GRAPH-NPORT-001 — Allowing a relation to own an arbitrary finite flag fibre generalizes the two-uniform multigraph to an incidence structure, while an expert mathematical model additionally needs typed flag spaces, relation roles or ordering, and a constitutive relation to represent an n-port factor rather than merely its hypergraph incidence. | Multigraphs for expert modelers | definition |
GRAPH-PI-COLLAPSE-001 — For a fixed linear two-terminal pi factor with series admittance Ys and endpoint shunts Ya and Yb, identifying both terminals through the common attachment map Tpi=[1,1]^T gives Tpi^T Ypi Tpi=Ya+Y_b, so the series contribution cancels and the exact nodal image is a one-terminal constant-admittance shunt under the declared coordinate and reference assumptions. | Multigraphs for expert modelers | theorem |
GRAPH-SELF-LOOP-001 — In the book's loopless bus–branch circuit specialization, ordinary edges connect distinct retained circuit nodes; a graph self-loop may remain in the source multigraph or arise from a topology quotient, but it is not interchangeable with an electrical circuit loop or mesh, a grounded shunt, or a diagonal self-admittance term. | Multigraphs for expert modelers | definition |
GROUND-SCOPE-001 — Reference, neutral, earth-return, and grounding-asset semantics are distinct model objects; reductions involving them must declare an earth-return class, grounding points, retained observations, and recovery data. | Earth, neutral, and reference model classes | definition |
GROUND-SCOPE-002 — On the recorded two-conductor fixture, floating, finite-impedance, and ideal customer-end grounding relations share the same simple bus–branch graph but change neutral voltage, ground-current allocation, and the associated observations. | Earth, neutral, and reference model classes | empirical |
GROUND-SCOPE-003 — In the scoped E₂ witness, an explicit earth conductor with a finite neutral-to-earth bond has distinct in-service, earth-conductor-outage, and phase-to-earth-fault states; the outage changes earth-current availability and the fault crosses the declared protection-current threshold while the simple bus graph remains fixed. | Earth, neutral, and reference model classes | empirical |
GROUND-SCOPE-004 — In the explicit-earth witness, a declared inverse-time relay curve maps the CT-scaled phase-earth fault current to a 0.2466 s operation, while the neutral-earth fault remains below pickup; a separate declared CT-saturation cap changes the phase-fault trip decision. | Earth, neutral, and reference model classes | empirical |
LOAD-BASE-001 — A voltage-dependent load's nominal voltage is an anchor in the load factor's declared terminal coordinate: WYE uses phase-to-neutral voltage and DELTA uses line-to-line voltage; copying one numeric bus voltage into both coordinates without an explicit base conversion changes the normalized load law. | Load models and decision dependence | definition |
LOAD-CONNECTION-001 — On the recorded balanced three-phase terminal fixture, explicit wye phase-to-neutral and delta phase-to-phase connection maps share the same bus and graph but produce different load-voltage observations: unit-magnitude wye voltages and sqrt(3)-magnitude delta voltages. | Load models and decision dependence | empirical |
LOAD-CONTINUATION-001 — On the recorded scalar two-bus continuation probe, the damped CP branch first fails to converge at demand scale 1.8 after a converged scale 1.7, while CI, CZ, and the declared ZIP branch remain converged through scale 3.0; this is an iteration-scoped branch diagnostic, not a global collapse theorem. | Load models and decision dependence | empirical |
LOAD-DECISION-001 — On the recorded two-bus fixture, CP, CI, CZ, and a normalized ZIP load law share the same bus–branch graph but produce distinct high-voltage solutions and decision margins: CP violates both the declared voltage and current limits, while CI, CZ, and ZIP satisfy both. | Load models and decision dependence | empirical |
NUMERICAL-001 — Representation and reduction choices have numerical consequences that must be reported separately from electrical preservation: coordinate scaling changes conditioning without changing an invertible solution set, Jacobian dependency graphs need not equal physical graphs, Schur elimination can create fill-in, and decision certificates require residual/error estimates and margins. | Numerical consequences of representation and reduction | definition |
NUMERICAL-002 — For the pinned running-network fixture, BMOPFTools exports a 20-by-20 passive Ybus with 166 nonzeros; the constant-Z linearized Ybus agrees with it, and realification produces a 40-by-40 current-voltage matrix with 664 nonzeros. The complex matrices have numerical rank 18 at the declared tolerance, with rank-aware effective 2-norm condition about 6.50e8 (1.13e7 after equilibration); the realified embedding preserves support and dimension but is not complex-transpose-symmetric. | Numerical consequences of representation and reduction | empirical |
NUMERICAL-003 — In the pinned nonlinear two-bus parallel-member witness, retaining two explicit member-current laws produces a 6-by-7 residual Jacobian and 13-by-13 KKT pattern, while the summed-current aggregate produces a 4-by-5 Jacobian and 9-by-9 KKT pattern; symbolic fill changes with elimination order in both formulations. | Numerical consequences of representation and reduction | empirical |
NUMERICAL-004 — A solver termination status is an algorithm report, not an independent solution-validity certificate; any scientific claim based on returned primal values must separately check the relevant numeric finiteness, equations, bounds, residuals, recovery obligations, and optimality level. | Numerical consequences of representation and reduction | definition |
NUMERICAL-005 — A complete solved-network feasibility claim requires an independently computed witness covering equation, KCL, power-balance, device-limit, and recovery residual obligations with declared tolerances; solver termination remains separate evidence. | Numerical consequences of representation and reduction | definition |
PRACTICE-ADAPTER-001 — A safe source-to-canonical adapter should publish stable identities, terminal maps, state and control treatment, factor and rating mappings, generated-object provenance, unsupported fields, validation findings, and declared recovery checks before downstream graph transformations are trusted. | From source data to a canonical network model | practice |
PRACTICE-IMPEDANCE-001 — A safe impedance adapter should retain conductor order and terminal maps, units and frequency, geometry or linecode provenance, earth-return assumptions, matrix diagnostics, shunt placement, and the limits and decisions that use the resulting coordinates. | From conductor geometry to impedance fidelity | practice |
PRESERVE-001 — Equivalence of two power-network models is indexed by a declared joint observation map and admissible input set; matching separate observation ranges or an unconstrained terminal relation alone does not establish equality of joint constrained feasible observable sets. | Preservation contracts | definition |
RATING-001 — A power-network rating must identify its constrained asset or terminal, measured quantity and feasible region, duration, ambient/scenario validity, and ownership/provenance before a transformation can claim to preserve it. | Rating and limit semantics | definition |
THESIS-001 — Representation adequacy is evaluated relative to declared observations, constraints, and decisions. | Scope and thesis | definition |
TOPOLOGY-001 — For a fixed switch state, topological nodes are the connected components of the closed-switch connectivity graph; compiling them into bus–branch buses is a state-conditioned quotient that requires provenance and does not preserve switching decisions by itself. | Node–breaker, bus–breaker, and topology processing | definition |
TR-GRAPH-001 — For a loopless identified multigraph and its simple endpoint projection, the multigraph cycle rank exceeds the simple-graph cycle rank by the sum over edge fibres of fibre size minus one; the lost dimensions are line-identity cycles supported on parallel fibres. | Cycles, parallelism, and radial structure | theorem |
TR-GRAPH-002 — An identified line is a multigraph bridge exactly when its simple endpoint edge is a bridge and its parallel fibre is a singleton; consequently the identified multigraph is a forest exactly when its simple projection is a forest and every edge fibre is a singleton. | Cycles, parallelism, and radial structure | theorem |
TR-GRAPH-ACTIVE-001 — For the five-bus fixture, the inventory has identified-member cycle rank 3 and simple-projection cycle rank 2, while the declared spanning tree is radial at both levels; active radiality is therefore a state-specific property, not an inventory-only label. | Cycles, parallelism, and radial structure | empirical |
TR-GRAPH-SIMPLIFY-001 — The loopless simple endpoint projection preserves the vertex set, adjacency, connected components, distinct-neighbour sets, and unweighted vertex distances, but it does not preserve identified edge count, incidence degree, cycle-space dimension, bridges, edge connectivity, spanning-tree multiplicity, or member-level state and provenance. | Multigraphs for expert modelers | theorem |
TR-NEG-001 — The executable anti-pattern witness rejects or classifies four tempting compositions: a heterogeneous series composite is not a homogeneous physical line, external grounding is not absorbed into a transformer, a three-port transformer is not a two-terminal line, and aggregate BIM/BFM branch balance does not imply member voltage compatibility. | Translation traps: graphs, circuits, and power-system language | empirical |
TRANSFORM-SEM-001 — Transformation certificates should distinguish typed structure, constitutive behaviour, decision semantics, and provenance; a structure-changing rewrite may remain exact for a narrower observation family only when its forgotten information, target closure, and recovery or constraint maps are declared. | Transformation semantics and register | definition |
| Claim | Chapter | Type |
|---|
ARCH-BLOCK-001 — For a declared two-bus four-conductor linear factor, the vector-edge, port-factor, block nodal, scalar-support, and realified-coordinate views are related representations of one assembled relation; coordinate expansion and realification do not create physical assets, while factor identity remains separate provenance. | How to read power-network diagrams and equations | empirical |
ARCH-CHORDAL-001 — For a simple bus-level tree with a common m-coordinate block at every bus and a structurally dense two-terminal stamp on every tree edge, the scalar structural-support graph is chordal and leaf-bus block elimination is a zero-fill perfect elimination ordering. | Two topology levels and the nodal projection | theorem |
ARCH-CONDUCTOR-002 — The five-bus scalar line-identity fixture lifts to fourteen scalar endpoint ports, five terminal junctions, and seven two-port line factors; the lift retains the q/r parallel fibre and its extra cycle dimension while adding no multiconductor, switch, or transformer semantics. | Formal representation frameworks | empirical |
ARCH-DEGENERACY-001 — Duplicate ideal switches with identical terminal sets and state domains have a well-defined electrical connectivity quotient but an unresolved asset-attribution relation; the model should retain both identities and emit a diagnostic rather than invent protection, maintenance, or failure ownership. | From source graphs to views and graph surgery | proposal |
ARCH-DEGENERACY-002 — The book proposes that missing grounding/reference declarations and rank-deficient active-state maps be treated as model-quality diagnostics; a compiler should refuse to infer a reference or invert a singular map without an additional declaration or restricted coordinate query. | From source graphs to views and graph surgery | proposal |
ARCH-FIVEBUS-XFMR-001 — In the recorded five-bus structural extension, one three-port transformer has acyclic local factor-incidence and star realizations, while eliminating the virtual star point generically yields a terminal clique with cycle rank one; the embedded factor-incidence and star member ranks coincide at five despite carrying different semantics, while the clique member rank is six, without implying additional physical transformer loops. | Five buses through a multi-port lowering | empirical |
ARCH-LENS-001 — A layer–lens matrix can attach concrete data, optimization, sparse-matrix, and graph-learning interfaces to different construction stages without treating software packages as representation levels; each attachment must declare preserved and omitted semantics. | Maps between representation frameworks | proposal |
ARCH-LOWER-001 — A typed lowering from an identity-bearing n-port source graph to ordinary-edge incidence objects may preserve a declared equation relation while forgetting factor identity unless source fibres and provenance are retained. | From source graphs to views and graph surgery | theorem |
ARCH-LOWER-002 — A four-winding transformer factor can be compiled pointwise into a complete terminal equation operator while retaining a full non-diagonal reference impedance, mixed winding connection maps, connection-specific shunts, internal grounding, recovery maps, and an explicit finite tap/phase decision domain; this does not by itself provide a source-faithful ordinary-edge realization. | Five buses through a multi-port lowering | theorem |
ARCH-NODAL-001 — Assembly of typed linear factor stamps into a compound nodal operator is not generally injective: distinct admissible parallel-factor decompositions can produce an identical nodal operator and identical normalized assembly residuals. | Two topology levels and the nodal projection | theorem |
ARCH-PORT-001 — A minimal executable port–factor bundle instantiated from the running network validates typed port-to-junction and port-to-factor incidence, a three-port multiwinding factor, grounding as an explicit factor, and a many-to-many asset/electrical relation Λ. | Formal representation frameworks | empirical |
ARCH-PORT-002 — The five-bus identified scalar multigraph has a direct structural port–factor lift with five bus junctions, seven two-port scalar line factors, fourteen endpoint ports, and one asset-to-factor relation per identified line; parallel members q and r remain distinct factors despite sharing the same bus pair. | Formal representation frameworks | empirical |
ARCH-RECOVERY-001 — Source recovery from a compound nodal operator is class-dependent: support-separated single-factor classes can be identifiable, over-parameterized classes can be set-identifiable at the terminal-primitive level, and parallel multiplicity or eliminated internal coordinates can be non-identifiable; a recovery interface must report the status and ambiguity rather than infer asset identity. | Two topology levels and the nodal projection | theorem |
ARCH-RECOVERY-002 — Auxiliary observations and declarations lift source-recovery ambiguity only through their joint observation map: catalog bounds may produce a compact but non-singleton feasible set, whereas member-current measurements, explicit grounding attribution, or a declared transformer state can make the restricted map injective in a scoped model class. | Two topology levels and the nodal projection | theorem |
ARCH-RECOVERY-003 — For a matrix-valued multiconductor factor observed through member-current snapshots, full primitive recovery requires voltage snapshots spanning the retained conductor space and coverage of every current coordinate; single-snapshot or phase-selective observations retain reciprocal ambiguity even when the assembled nodal operator is known. | Two topology levels and the nodal projection | theorem |
ARCH-RECOVERY-004 — For noisy full-rank multiconductor voltage/current snapshots, the pseudoinverse source estimate has a deterministic Frobenius error bound proportional to the noise radius and the voltage-snapshot pseudoinverse norm; nearly dependent excitation therefore enlarges the certified uncertainty set even when the observation map is full rank. | Two topology levels and the nodal projection | theorem |
ARCH-SUPPORT-001 — Block and scalar nonzero-support graphs of a declared compound nodal operator are simple graphs by construction, while the identified factor-stamp decomposition is separate data and may be a multigraph. | Two topology levels and the nodal projection | theorem |
ARCH-SURGERY-001 — The book proposes that state-conditioned graph surgery return state-indexed graphs or graph families with diagnostics and provenance; for many unknown switches, a three-valued certain-connected/certain-separated/undetermined summary should be available instead of silently collapsing to one active graph. | From source graphs to views and graph surgery | proposal |
ARCH-SURGERY-002 — The book proposes that an n-terminal surgery retain port-coordinate identity and return port-specific active and isolated sets; it cannot be inferred by replacing an n-port factor with implicit pairwise edges. | From source graphs to views and graph surgery | proposal |
ARCH-VIEW-001 — The book proposes that a power-network visualisation declare its object level, preserved and forgotten semantics, identity fibres, and reverse-map status; single-line, multi-line, port-factor, node-breaker, nodal-support, and reduced views are distinct typed projections. | From source graphs to views and graph surgery | proposal |
DATA-XWALK-001 — CIM/CGMES, PowerModelsDistribution, OpenDSS, and MATPOWER provide distinct partial correspondences to the book's asset, terminal, topology, factor, state, and rating objects; successful import is not by itself semantic or decision equivalence. | Data-model crosswalk | practice |
FIXTURE-001 — Running-network fixture v0.1.0 passes the current BMOPFTools JSON schema and conformance checks without errors or warnings. | Executable running network | empirical |
FIXTURE-002 — The v0.1.0 continuous PF and OPF instances terminate locally solved in the recorded environment. | Executable running network | empirical |
| Claim | Chapter | Type |
|---|
TR-COMP-001 — Two exact certified transformations compose when the first target is consumed by the second source; constraint maps apply forward and recovery maps apply in reverse order. | Certificate schema and composition | theorem |
TR-COORD-001 — A simultaneous permutation of conductor coordinates, terminal pairing, element matrices, and componentwise limits is an exact normalization with an inverse permutation. | Conductor-coordinate normalization | theorem |
TR-GRAPH-001 — For a loopless identified multigraph and its simple endpoint projection, the multigraph cycle rank exceeds the simple-graph cycle rank by the sum over edge fibres of fibre size minus one; the lost dimensions are line-identity cycles supported on parallel fibres. | Cycles, parallelism, and radial structure | theorem |
TR-GRAPH-002 — An identified line is a multigraph bridge exactly when its simple endpoint edge is a bridge and its parallel fibre is a singleton; consequently the identified multigraph is a forest exactly when its simple projection is a forest and every edge fibre is a singleton. | Cycles, parallelism, and radial structure | theorem |
TR-GRAPH-ACTIVE-001 — For the five-bus fixture, the inventory has identified-member cycle rank 3 and simple-projection cycle rank 2, while the declared spanning tree is radial at both levels; active radiality is therefore a state-specific property, not an inventory-only label. | Cycles, parallelism, and radial structure | empirical |
TR-GRAPH-SIMPLIFY-001 — The loopless simple endpoint projection preserves the vertex set, adjacency, connected components, distinct-neighbour sets, and unweighted vertex distances, but it does not preserve identified edge count, incidence degree, cycle-space dimension, bridges, edge connectivity, spanning-tree multiplicity, or member-level state and provenance. | Multigraphs for expert modelers | theorem |
TR-KRON-001 — Typed multiconductor Kron reduction commutes with invertible coordinate actions that preserve the retained/internal partition when currents transform by the power-dual action; per-port block diagonality is an optional locality restriction, and the affine statement requires fixed internal injections. | Kron, Ward, and optimized network equivalents | theorem |
TR-KRON-002 — In the declared linear scenario fixture, exact Kron reproduces each fixed-injection boundary relation, an operating-point Ward-style equivalent is exact only at its calibration point, and an explicit scenario objective can select a sparser non-exact target. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-003 — In the declared one-state linear Ward scenario fixture, an internal-injection residual propagates through a recovered-state bound and a boundary-current bound to classify the approximate source-limit decision as certified feasible, ambiguous, or certified violated; the bound is exact for this fixture but is not a general nonlinear error theorem. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-FIVE-001 — In the five-bus scalar fixture, eliminating the pendant bus m through line u by typed Kron reduction reproduces the retained boundary Y-bus obtained by direct deletion of the leaf line, with exact boundary-current recovery for the recorded voltage state. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-FIVE-002 — In the same five-bus fixture, eliminating the non-pendant bus l by typed Kron reduction preserves the recorded boundary current relation, creates Schur-complement fill edges j-m and k-m among the retained buses, and exactly recovers the u-branch current whose deliberately tight declared limit is violated by the recorded state. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-001 — In the running four-conductor midpoint Kron fixture, the eliminated neutral half-section current is exactly recoverable from the retained boundary solution and midpoint recovery; a neutral-current limit must therefore remain in the reduced feasible set, and dropping it admits the recorded boundary point that the source model rejects. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-002 — In the recorded five-conductor midpoint probe, retaining an explicit earth terminal and a midpoint neutral-earth bond yields separately recoverable neutral and earth KCL currents and a neutral-current limit; collapsing earth return into neutral would lose an observed factor relation. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-003 — In the recorded three-segment five-conductor probe with two explicit neutral-earth bonds, each grounding point has separately recoverable neutral and earth KCL currents and bond-current observations; a single collapsed neutral constraint cannot represent both points. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-004 — In the recorded finite grounding-impedance sweep, changing the two explicit neutral-earth impedances changes recovered neutral current and the feasibility classification under one fixed neutral limit, even though the structural reduction and KCL contracts remain unchanged. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-005 — In the recorded local state-dependent grounding probe, shifting an endpoint state changes the nonlinear neutral-earth bond map; reusing the nominal bond map leaves a nonzero shifted-state residual, while recomputation restores the relation and preserves explicit neutral-limit evaluation. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-006 — In the recorded two-point state-dependent grounding chain, shifting the endpoint state changes both nonlinear neutral-earth bond maps; freezing both nominal maps leaves a nonzero chain residual and changes recovered segment-neutral currents, while recomputation restores the local relation. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-007 — In the recorded finite endpoint-state continuation of the two-point nonlinear grounding chain, recomputing the bond maps at five declared states preserves small nonlinear residuals and records changing neutral-limit margins, while the frozen nominal map fails away from the base state. | Kron, Ward, and optimized network equivalents | empirical |
TR-KRON-NEUTRAL-008 — In the recorded local nonlinear grounding derivative probe, the analytic real Jacobian at the base state gives a smaller shifted-state linearisation error than the frozen nominal bond coefficient, and the Jacobian error decreases over the declared smaller step scales. | Kron, Ward, and optimized network equivalents | empirical |
TR-NEG-001 — The executable anti-pattern witness rejects or classifies four tempting compositions: a heterogeneous series composite is not a homogeneous physical line, external grounding is not absorbed into a transformer, a three-port transformer is not a two-terminal line, and aggregate BIM/BFM branch balance does not imply member voltage compatibility. | Translation traps: graphs, circuits, and power-system language | empirical |
TR-PAR-001 — Summed admittance preserves the unconstrained terminal relation of parallel linear branches. | A plausible model gives the wrong answer | theorem |
TR-PAR-002 — Using the sum of member current ratings can create an outer relaxation of the member-constrained feasible set. | A plausible model gives the wrong answer | theorem |
TR-PAR-003 — In the recorded two-bus maximum-served-load problem, the naive summed-rating aggregate serves 200 MW while the source and exact lifted formulations each serve 110 MW. | A plausible model gives the wrong answer | empirical |
TR-PAR-004 — In the recorded two-conductor AC maximum-served-load case, the source, exact lifted, and certified exact-pruned formulations have objective 0.6138908, while a summed-limit aggregate has objective 1.0630833 and violates a 0.6 p.u. member limit. | Multiconductor parallel AC decision case | empirical |
TR-PAR-005 — For fixed linear complex terminal-current maps with centered Euclidean norm limits, one normalized constraint implies another if and only if the retained normalized real quadratic form minus the candidate form is positive semidefinite; applying this pairwise test to every aligned conductor and both terminal ends certifies exact candidate-limit pruning while retaining both member models. | Multiconductor parallel AC decision case | theorem |
TR-PAR-006 — For nonsingular fixed series admittances on common multiconductor endpoint coordinates, candidate component currents recover as Il2=(Yl2/Yl1)Il1, and the exact maximum of candidate component c over all retained component-current discs is sumk abs(Kck) Imax_l1k; in the recorded reciprocal non-proportional three-phase four-wire AC case this certifies all l2 limits redundant, the exact-pruned and source objectives agree at 1.1274329, and a summed-limit aggregate reaches 1.8058181 by violating an l1 limit. | Non-proportional three-phase four-wire parallel case | theorem |
TR-PAR-007 — For fixed nominal-pi multiconductor members whose retained full two-end terminal-current primitive Ar is nonsingular, all candidate terminal currents recover as Ac*inv(Ar) times the retained terminal-current vector, so exact complex-polydisc row norms certify joint implication across both line ends; in the recorded non-proportional four-wire case, pruning eight member-2 limits preserves the 1.1286205 source objective while a same-size summed-limit model reaches 1.8077114 by violating member 1. | Four-wire nominal-pi parallel case | theorem |
TR-PAR-AC-JOINT-001 — In the recorded three-member four-wire AC case, member 3 has the fixed recovery Il3=0.10 Il1+0.10 I_l2 and a 0.15 p.u. component limit; the joint support bound is 0.144 p.u., so deleting member-3 limits preserves the locally solved source objective 1.2401762 to 7e-14. An independent damped-Newton continuation and bisection reproduces the source boundary within 1.3e-8 served-fraction units. | Four-wire nominal-pi parallel case | empirical |
TR-PAR-JOINT-001 — For fixed series current maps in common endpoint-voltage-drop coordinates, a candidate component-current limit is implied by several retained member limits when its exact recovery row has support bound sumk abs(Kck) Ibar_k no larger than the candidate rating; the guarded witness certifies this joint implication for three retained discs. | Four-wire nominal-pi parallel case | theorem |
TR-PAR-SINGULAR-001 — For the declared series-only singular four-wire fixture, the full two-end terminal-current map is rank deficient, but the endpoint-voltage-drop coordinate recovers member-2 currents exactly from member-1 currents through the declared diagonal map, with the zero-neutral rows retained as an explicit invariant; this is a guarded reduced-coordinate result, not a pseudoinverse or singular-shunt theorem. | Four-wire nominal-pi parallel case | empirical |
TR-PAR-STATE-001 — In the recorded finite four-state four-wire AC envelope, rebuilding the member maps and source/pruned formulations at each declared scalar or phase-selective admittance state preserves exact joint limit pruning locally while changing the optimal served value across states. | Four-wire nominal-pi parallel case | empirical |
TR-SER-001 — A zero-injection degree-two junction between coordinate-aligned, series-only elements with no pairwise or external mutual coupling has equivalent impedance Zl1 + P' Zl2 P; mutually coupled sections instead contain the cross terms Z12 P + P' Z21. | Degree-two series elimination | theorem |
TR-SER-002 — Exact terminal-behaviour closure under degree-two elimination does not by itself establish closure within a homogeneous physical line class. | Degree-two series elimination | theorem |
TR-SER-003 — For a zero-injection degree-two junction whose two series-only source elements declare both pairwise cross-impedance blocks and no external mutual coupling, the exact terminal-behaviour composite has impedance Z1 + Z12 P + P' Z21 + P' Z2 P, with source currents recovered by I1 = Iequivalent and I2 = P Iequivalent. | Degree-two series elimination | theorem |
TR-XFMR-001 — A transformer winding terminal permutation is an exact typed-factor normalization when its complete terminal-to-coil incidence relation is right-multiplied by the inverse permutation and coil coordinates remain fixed. | Transformer-winding coordinate normalization | theorem |
TR-XFMR-002 — Complete pairwise multiwinding short-circuit impedances compile exactly into a reference-coordinate impedance matrix ZB, from which every pairwise impedance is recoverable; changing the selected reference winding leaves the external winding admittance invariant, and the classical star/T representation is the three-winding special case. | Multiwinding leakage reference compilation | theorem |
TR-XFMR-003 — Aligned winding connection-incidence factors compose exactly with a multiwinding leakage admittance as Yterminal=A'(Yw kron I)A; retaining the coil-current map preserves per-coil winding limits and makes terminal-coordinate and leakage-reference changes explicit coordinate actions. | Multiwinding terminal leakage assembly | theorem |
TR-XFMR-004 — A fixed linear transformer completion with declared voltage transfer T, leakage map B=TA, excitation placement S, and transformer-internal grounding has terminal admittance Ycomplete=B^HYcoilB+S^TY0*S+Yground; the power-dual and component-current recovery maps preserve the declared leakage-path limits, while adjustable transfers must remain parameterized decision factors. | Fixed-linear transformer factor completion | theorem |
TR-XFMR-005 — A continuous or discrete scalar winding tap compiles exactly as a retained parameterized transformer factor when coefficientxkc(tap)=tap*basecoefficient_xkc and the decision identity and domain are mapped identically; freezing the tap at its start value is generally only an inner restriction, and in the recorded discrete witness it loses the 1.05 optimum and increases the winding-current objective by 671.060 A. | Parameterized transformer tap decisions | theorem |
TR-XFMR-006 — A retained finite scalar transformer tap factor embeds exactly into unchanged multiconductor AC voltage, KCL, power-balance, voltage-limit, and recovered leakage-current constraints by pointwise evaluation; in the recorded 11-terminal WYE/WYE/DELTA case, direct source and parameterized target subproblems agree at all three taps, select 0.95 with served fraction 1.2305865, and freezing the 1.00 start loses 0.0601126 served fraction (0.090169 MW). | Transformer tap AC decision case | theorem |
TR-XFMR-007 — A separate damped finite-difference Newton, continuation, and bisection implementation reproduces all three TR-XFMR-006 tap-conditioned high-voltage branch boundaries without an external optimizer; its largest served-fraction difference from JuMP/Ipopt is 3.14e-10, and both methods select tap 0.95. | Transformer tap AC decision case | empirical |
TR-XFMR-008 — In the recorded 11-terminal WYE/WYE/DELTA tap case, a phase-selective unbalanced second scenario can be handled without collapsing the transformer or its phase identities: exact enumeration of the nine ordered tap pairs preserves branch completeness and exposes the per-phase scenario directions explicitly. | Transformer tap AC decision case | empirical |
TR-XFMR-009 — For the recorded 11-terminal WYE/WYE/DELTA case, a three-scenario phase-selective tap path can be enumerated exactly over the 3^3 ordered tap triples, with consecutive tap movement charged explicitly and each scenario retaining its own phase directions. | Transformer tap AC decision case | empirical |
TR-XFMR-010 — In the recorded three-scenario tap path, enumerating all 27 ordered tap triples and then applying an explicit at-most-one-movement policy leaves 15 admissible branches; the policy is a decision constraint and must not be inferred from the unconstrained best path. | Transformer tap AC decision case | empirical |
TRANSFORM-CATALOG-001 — The guarded-normalization catalogue treats coordinate normalization, series elimination, parallel bundling, switch contraction, multiwinding compilation, and rooted-tree views as distinct rule families whose acceptance depends on declared closure, recovery, constraint, and provenance guards. | Guarded normalization rules | proposal |
| Artifact | Evidence summary |
|---|
active-radiality-witness.json | generated evidence |
artifact-manifest.json | generated evidence |
australian-carson-reproduction.json | generated evidence |
balanced-transmission-independent-reproduction.json | COLLAPSE-001 — generated evidence |
balanced-transmission-witness.json | COLLAPSE-001 — generated evidence |
block-structure-bridge-witness.json | ARCH-BLOCK-001 — two-bus four-conductor fixed linear factor with full complex series matrix and endpoint shunts |
certified-approximation-witness.json | TR-KRON-003 — kronwardscenariofixturev0.1.0 |
circuit-formulation-witness.json | FORMULATION-NODAL-001 — ideal voltage source, floating linear network, and aligned parallel members with source-level current limits |
clean-package-matrix.json | PKG-CLEAN-001 — generated evidence |
compiled-views-surgery-witness.json | ARCH-VIEWS-SURGERY-001 — finite typed source graph with one three-port factor, duplicate ideal switches, four-wire phase-only switching, and one state-conditioned zone surgery |
conductor-terminal-lift-witness.json | ARCH-CONDUCTOR-001 — running-network v0.1.0 conductor-terminal incidence with line, switch, and three-winding factor compilation |
connection-map-independent-reproduction.json | LOAD-CONNECTION-001 — generated evidence |
coordinate-normalization-certificate.json | TR-COORD-001 — generated evidence |
coordinate-series-composition-certificate.json | TR-COMP-001 — generated evidence |
coupled-corridor-lattice-witness.json | COUPLED-CORRIDOR-002 — two reciprocal fixed-linear scalar series sections on four retained terminal-voltage coordinates |
data-model-crosswalk-witness.json | DATA-XWALK-001 — data/running-network/v0.1.0.json |
degree-two-series-certificate.json | TR-SER-001 — generated evidence |
explicit-earth-independent-reproduction.json | GROUND-SCOPE-004 — generated evidence |
explicit-earth-kron-independent-reproduction.json | TR-KRON-NEUTRAL-002 — generated evidence |
explicit-earth-kron-witness.json | TR-KRON-NEUTRAL-002 — synthetic five-conductor linear series midpoint with ordered (a,b,c,n,e) terminals and a fixed midpoint neutral-earth bond |
five-bus-active-radiality-witness.json | TR-GRAPH-ACTIVE-001 — experiments/generated/five-bus-cycle-space-analysis.json |
five-bus-conductor-terminal-lift-witness.json | ARCH-CONDUCTOR-002 — five-bus cycle-space scalar line identities lifted to scalar terminal junctions and two-port factors |
five-bus-cycle-space-analysis.json | GRAPH-CYCLE-001 — connected loopless scalar series bus-branch multigraph |
five-bus-figure-manifest.json | generated evidence |
five-bus-port-factor-witness.json | ARCH-PORT-002 — experiments/generated/five-bus-cycle-space-analysis.json |
five-bus-transformer-lowering-witness.json | ARCH-FIVEBUS-XFMR-001 — five-bus scalar line topology plus a structural three-port transformer extension attached at j, l, and m |
five-bus-typed-kron-witness.json | TR-KRON-FIVE-001 — experiments/generated/five-bus-cycle-space-analysis.json |
fixture-coverage-matrix.json | PKG-FIXTURE-001 — generated evidence |
four-winding-lowering-witness.json | ARCH-LOWER-002 — fixed-frequency four-winding factor with a full non-diagonal reference matrix, mixed WYE/DELTA ports, connection-specific shunts, internal grounding, and finite pointwise tap/phase states |
four-wire-impedance-model-ladder.json | IMPEDANCE-LADDER-001 — deterministic four-wire matrix fixture |
four-wire-parallel-ac-certificate.json | TR-PAR-006 — generated evidence |
grounding-impedance-sweep-independent-reproduction.json | TR-KRON-NEUTRAL-004 — generated evidence |
grounding-impedance-sweep-witness.json | TR-KRON-NEUTRAL-004 — generated evidence |
guarded-parallel-reduction-witness.json | TR-PAR-GUARDED-001 — series-only singular terminal map, jointly retained current discs, and state-dependent admittance maps |
hierarchy-boundary-witness.json | ARCH-BOUNDARY-001 — running-network hierarchy, typed boundary refinement, open-system gluing, and state-conditioned switch maps |
kron-ward-scenario-comparison.json | TR-KRON-002 — kronwardscenariofixturev0.1.0 |
layer-lens-api-witness.json | ARCH-LENS-001 — five construction stages crossed with identity, connectivity, behaviour, decision, and software lenses |
load-continuation-independent-reproduction.json | LOAD-CONTINUATION-001 — generated evidence |
load-grounding-witnesses.json | generated evidence |
load-model-independent-reproduction.json | LOAD-DECISION-001 — generated evidence |
multiconductor-parallel-ac-certificate.json | TR-PAR-004 — generated evidence |
multiconductor-recovery-witness.json | ARCH-RECOVERY-MULTI-001 — two reciprocal two-conductor parallel factors with linear voltage/current observations |
multiwinding-leakage-compilation-certificate.json | TR-XFMR-002 — generated evidence |
multiwinding-terminal-assembly-certificate.json | TR-XFMR-003 — generated evidence |
multiwinding-terminal-lift-witness.json | ARCH-CONDUCTOR-MULTI-001 — serialized three-winding fixed-linear transformer contract lifted to ordered terminal ports |
multiwinding-typed-kron-witness.json | TR-KRON-MULTI-001 — serialized three-winding terminal admittance with DELTA terminal block eliminated |
narrow-circuit-transformations-witness.json | generated evidence |
neutral-kron-independent-reproduction.json | TR-KRON-NEUTRAL-001 — data/running-network/v0.1.0.json |
nodal-recovery-guards-witness.json | ARCH-RECOVERY-GUARDS-001 — finite nodal operators with declared catalog bounds, member observations, grounding metadata, and scalar state maps |
nodal-source-recovery-witness.json | ARCH-RECOVERY-001 — finite compound nodal operators with declared support, elimination, and parameter classes |
node-breaker-state-witness.json | TOPO-NB-001 — four-connectivity-node node-breaker fixture with two switch assets and state-conditioned bus compilation |
noisy-multiconductor-recovery-witness.json | ARCH-RECOVERY-NOISE-001 — two-conductor matrix primitive observed through noisy full-rank voltage/current snapshots |
nonlinear-grounding-local-bound-witness.json | TR-KRON-NEUTRAL-008 — illustrative voltage-dependent scalar neutral-earth bond law |
nonlinear-grounding-probe-independent-reproduction.json | TR-KRON-NEUTRAL-005 — generated evidence |
nonlinear-grounding-probe-witness.json | TR-KRON-NEUTRAL-005 — generated evidence |
nonlinear-kkt-witness.json | NUMERICAL-003 — finite-difference nonlinear AC decision Jacobians and symbolic KKT sparsity for a two-bus parallel-member witness |
nonlinear-two-point-grounding-continuation-independent-reproduction.json | TR-KRON-NEUTRAL-007 — generated evidence |
nonlinear-two-point-grounding-continuation.json | TR-KRON-NEUTRAL-007 — generated evidence |
nonlinear-two-point-grounding-independent-reproduction.json | TR-KRON-NEUTRAL-006 — generated evidence |
nonlinear-two-point-grounding-witness.json | TR-KRON-NEUTRAL-006 — generated evidence |
nonlinear-ward-witness.json | nonlinear_ward_probe_v0.1.0 — scalar constant-power internal state with a base-state Ward approximation |
numerical-structure-witness.json | NUM-STRUCT-001 — five-bus source topology; structural dependency patterns, not numerical Jacobian entries |
parallel-branch-certificate.json | TR-PAR-001 — generated evidence |
parallel-opf-comparison.json | TR-PAR-003 — generated evidence |
pi-four-wire-parallel-ac-certificate.json | TR-PAR-007 — generated evidence |
port-factor-architecture.json | ARCH-PORT-001 — data/running-network/v0.1.0.json |
positive-sequence-collapse-witness.json | COLLAPSE-002 — generated evidence |
provenance.json | generated evidence |
public-api-manifest.json | generated evidence |
running-network-cycle-space-witness.json | GRAPH-CYCLE-RUNNING-001 — identified scalar line projection of the running multiconductor fixture |
running-network-radiality-witness.json | TOPO-RUNNING-001 — running-network v0.1.0 bus/member graph with switch and line-outage variants plus conductor-terminal provenance |
running-network-typed-kron-witness.json | TR-KRON-001 — data/running-network/v0.1.0.json |
semantic-evaluator-matrix.json | PKG-SEMANTIC-001 — generated evidence |
solver-diagnostics-crosswalk.json | NUM-SOLVER-CROSSWALK-001 — package-level BMOPFTools Ybus/Jacobian plus finite-difference nonlinear KKT diagnostics |
state-space-unit-witness.json | ARCH-STATE-UNIT-001 — data/running-network/v0.1.0.json |
summary.json | generated evidence |
three-member-four-wire-parallel-ac-certificate.json | generated evidence |
three-member-state-envelope-independent-reproduction.json | TR-PAR-STATE-001 — generated evidence |
topology-projection-witness.json | ARCH-TOPOLOGY-001 — two aligned passive reciprocal two-conductor factors and a three-bus two-conductor tree with structurally dense line stamps |
transformer-control-family-witness.json | TR-XFMR-CONTROL-001 — pointwise transformer control compilation with phase, mechanical, automatic, and tap-dependent-loss families |
transformer-factor-completion-certificate.json | TR-XFMR-004 — generated evidence |
transformer-tap-ac-decision-certificate.json | TR-XFMR-006 — generated evidence |
transformer-tap-ac-independent-certificate.json | TR-XFMR-007 — generated evidence |
transformer-tap-decision-certificate.json | TR-XFMR-005 — generated evidence |
transformer-tap-three-scenario-independent-certificate.json | TR-XFMR-009-REPRO — generated evidence |
transformer-winding-normalization-certificate.json | TR-XFMR-001 — generated evidence |
translation-trap-witnesses.json | generated evidence |
typed-kron-certificate.json | TR-KRON-001 — generated evidence |
typed-kron-witness.json | TR-KRON-001 — typedmulticonductorkronfixturev0.1.0 |
view-source-maps.json | generated evidence |
ybus-jacobian-witness.json | NUMERICAL-002 — BMOPFTools passive and constant-Z linearized Ybus for running-network fixture v0.1.0 |