L0 — Physics: the device, the field, and ε

Node — the field/material, where ε lives: Field(A), the trajectory space of the transient field problem (00), the device models (02), and the error model (03); the analog, probabilistic bottom of the tower. Edge up — the electrical abstraction (the ε-crossing): within the envelope, field simulation over the cell and interconnect geometry establishes Contracts(N)'s transfer functions — carried by per-cell enclosures (07), lumping/composition (08), the interconnect capacitance enclosures (09), and screening (10) — and ε is bounded within L0's budgets, modulo E1.

Background

The bottom. Below the netlist there are no bits — only charge, fields, and dopant atoms — and this layer manufactures the digital abstraction out of that material: per-cell contracts certifying that each standard cell computes its Boolean function, within noise margins and delay intervals, under stated operating conditions. The route runs through the governing PDE's well-posedness (00), the reduction from Maxwell's equations to circuit theory (01, 08), the fitted device models carrying the project's deepest empirical axiom (02), validated per-cell numerics (07), the regime decomposition that is the digital abstraction stated as a theorem (06), the error model deciding what survives as probability (03), the envelope outside which none of it holds (04), what the whole tower bottoms out on (05), and the transistor-level cut discipline (06). This is the crunchiest material in the book; the per-chapter Backgrounds assume no physics beyond curiosity.

Statement

Two things, and they are different in kind:

1. A transistor network implements its contract. For each of the ~400 standard cells: geometry → devices → interval device model → a timed assume-guarantee contract (interval Liberty arc + regime classes, 07/06), whose untimed shadow is the cell's Boolean function. Verified once per process, amortised over every design forever.
2. The error model is Poisson, not Gaussian. Continuous perturbations are suppressed below any threshold of interest and are discharged; discrete events are carried.

The L0 / L1 boundary — resolved

There is one physical problem: Maxwell plus carrier transport over the whole die. The layer split is not "L0 = devices, L1 = wires" — it is a split by abstraction target, and both layers solve instances of the same PDE.

                 ONE field problem over the die
                              │
        ┌─────────────────────┴─────────────────────┐
   L0: on cell interiors                     L1: on the complement
   nonlinear (transport)                     linear (electrostatics)
   → terminal I-V → Boolean function         → per-net RC enclosures
        └─────────────────────┬─────────────────────┘
                              │
              L0/08: the LUMPING + COMPOSITION theorem
              "you may glue these two and get a circuit"

L0 owns both instances of the field problem — well-posedness, the quasi-static reduction, device models, the per-cell enclosures, and the linear interconnect enclosures (09, 10) — and, critically, the composition theorem that licenses gluing them into a circuit (08); all of this is the electrical-abstraction edge that lifts into L1. L1 owns the drawn geometry that defines the domain (the coloured image and its extrusion) and reads the circuit back out of it (extraction/LVS).

The four-step factoring

The proof plan, in order of logical dependence (which is not document order — notably it puts the envelope before the per-component work, as a precondition):

1. Existence, circuit-independent. The transient system has global-in-time solutions for any geometry, within the model's validity — established (Gajewski–Gröger). Uniqueness is not required: every downstream claim is an enclosure quantified over all solutions, which converts stationary non-uniqueness (M1) from a blocking assumption into a reachability obligation — see 00. "Within reasonable physical bounds" means model validity, not solution bounds: the theorem is unconditional for the model; the envelope justifies the model. [00, 01]
2. Coarse invariance, near-circuit-independent. Every solution stays in a broad safe set: bounded potentials (maximum principle) and carrier densities, no runaway — a theorem within the model, since the omitted terms (impact ionisation, electrothermal coupling) are exactly where the feedback dangers live. Excluding those is 04's envelope, whose side conditions are computable but not all structural (thermal is workload-conditional). The safe set is honest-broad: it contains U, 0, 1, transitioning, metastable, and the latched states — which step 3 must show unreachable, not assume absent. [07, 00, 02]
3. Fine regime decomposition, per component. Pin regions "0" / "1" / "transitioning", with "transitioning" a family parameterised by slew — the component's behaviour is an assume-guarantee contract on trajectory classes (an interval Liberty arc with an explicit domain): guaranteed output class given input classes, load, and a bounded local disturbance budget. Established numerically with rigorous enclosures, once per library cell. The disturbance budget's discharge is nonlocal (L1's screening) and must cover Miller feedthrough through the component. [02, 03, 05]
4. Composition = combinatorics + side conditions. Components plug together by finite checking: each edge's load / slew / coupling within the contracts' domains (not vacuous — the shipped design fails these, F2). Cuts are licensed only at restoring, near-unidirectional boundaries (channel-connected components), so every bistable loop is internal to a component. Three globals do not factor through pins — supply, clock, temperature — and need their own aggregate arguments. Conclusion: the network emulates a state machine, except at Poisson fault events and unresolved synchroniser reads, which are carried as P1/P2, never proved away. [04, 06]

The overall deliverable, restated: every solution of the field problem lies within the enclosure that the lumped semantics predicts, established by component contracts + PDE bounds + an abstract composition argument.

Subcomponents

On the existence question. For the linear electrostatic problem it is classical — Lax–Milgram on H¹ with bounded measurable coefficients — and not open at all. For the device problem (drift–diffusion) existence is established but uniqueness is not known in general, and the non-uniqueness is physically real: latch-up and snapback are second solution branches. See 00 and 02. The industry's answer is to not solve the PDE at all, which relocates the question into an empirical claim about compact models.

Interfaces

Consumes: cell layouts and the material stack (L1's geometry), an interval device model (E1). Exports: per-cell timed contracts — interval Liberty arcs with explicit domains (07) — and their Boolean shadows (06); the composition licence (08, 06); a per-cycle upset rate λ and the noise margin NM (03). The timed contracts are what L1's STA composes; omitting them from this list was the seam mismatch the 2026-07 review caught.

Axioms introduced

E1 (the tower's one physical axiom) and P2 (SEU). Formerly also E2, P3 and X2 — all discharged or rerouted in the reassessment (Axioms): 07 is E2's discharge route, 03 P3's, and X2's check moved to L1's G2 with its empirical residue (the upset radius) into P2.

Effort

1–3 years — the swing is exactly the per-cell cost that 07's first experiment prices. Dominated by 07 and 08. The Boolean-function-per-cell result is the load-bearing output; the error model is smaller but needs probabilistic machinery nothing else in the project requires.

Reading

von Neumann, Probabilistic Logics and the Synthesis of Reliable Organisms from Unreliable Components (1956). Bryant on switch-level (MOSSIM). Melham, Higher Order Logic and Hardware Verification. Markowich, The Stationary Semiconductor Device Equations.