Formal reconstruction · collisionless linearization, failure of normal modes, one-sided Laplace evolution, retarded initial-data response, complex-contour deformation, collective-field damping, long- and short-wave asymptotics, regularity dependence, velocity-resolved oscillation, causal half-space prescription, dielectric resonance branches, and deferred numerical evaluation
On the Vibrations of the Electronic Plasma
Collective field decay and a persistent longitudinal marginal, with the residue and frequency conditions made explicit
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureA self-consistent electrostatic state, distinct from its explanation.
- inductiveA fixed neutralizing background is not a dynamical ion distribution.
- inductiveThe linear initial-value and stationary nonlinear equations are distinct.
- structureThe selected physical indices, without a proof of either equation.
- structureProof-free selected plasma data and proposition-valued physical relations. In particular, neither the kinetic equation nor the Poisson closure is a stored proof.
- structureThe same selected indices paired with independent source provenance.
- structureThe longitudinal velocity can also be one slice of a three-dimensional distribution, with the two transverse velocities fixed.
- structure
- structure
- structure
- structure
- inductive
- inductive
- inductive
- structure
- inductive
- structure
- structureA selected claim must depend on exactly these source-map steps.
- structureA selected claim must retain exactly these epistemic statuses.
- structureA selected route must name exactly these immediate predecessor routes.
- structure
- structure
- inductive
- structureOne selected spatial Fourier mode, not a complete state of every mode.
- inductive
- structureThe homogeneous Maxwellian and one selected spatial Fourier component. The electron charge is signed; the stationary positive background cancels its equilibrium charge.
- structure
- inductiveLandau's fixed-ion kinetic/Poisson and one-sided initial-value source.
- structure
- structure
- structure
- structure
- structureFinite source-shaped data distinguishing Landau's half-space dielectric, bulk field, contour, attenuation, resonance, and wall-boundary claims.
- structure
- structure
- structureNamed imported-frequency and local-decrement calculations do not by themselves retain Landau's displayed equations (16)-(17).
- structurePositive large-k damping dominance does not fix Landau's source formulas.
- structure
- inductive
- structure
- structure
- structureProof-free semantics for one selected response problem. The two time arguments of `responseDependsOnAt` and `responseKernelSupportsAt` are, respectively, the source time and response time.
- structure
- structure
- structurePredictions made by descriptions in regimes. `predicts` is relational so the signature can represent deterministic values, sets of allowed values, or probabilistic outputs without choosing among them.
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA physically selected, inhabited collisionless kinetic/Poisson solution.
- definitionThe selected branch satisfies its actual collisionless kinetic equation.
- definitionScope, physical roles, and a genuinely collisionless approximation.
- definitionThe selected potential is closed by the actual selected distributions.
- definitionKinetic evolution, Poisson closure, and their independent joint bridge.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected self-consistent plasma state whose explanation is tracked.
- definitionExact proof-free indices selected by the collisionless plasma context.
- definitionThe exact selected collisionless state plus its source derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSource provenance is separate from the common physical endpoint.
- definitionAn exact selected collisionless state structurally explains its closure.
- definition
- definition
- definition
- definition
- definitionAn integrable positive velocity density, not a symbolic occupation label.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition`E = -d phi / dx`; the charge is signed, not its magnitude.
- definitionImmediate predecessor routes. Claims established by their transitive predecessors are inherited by the dependency closure.
- definition
- definition
- definition
- definition
- definition
- definitionTemporary reductio-introduction steps discharged by this inference. Discharge removes only those exact origins from the conclusion's epistemic basis; it does not assert the temporary hypotheses globally.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-mapped claim holds when its declared formula evaluates under the given paper-local semantic interpretation.
- definition
- definition
- definition
- definition
- definitionEvery claim in the supplied identifier list holds.
- definitionA source-mapped step is semantically sound when the interpreted premises imply the interpreted conclusion. Physical principles and imported calculations therefore remain explicit hypotheses of paper-specific certificates rather than acquiring truth from their source-map labels. A reductio hypothesis is different: it introduces a temporary assumption into a subargument and therefore is not required to hold globally. Its later uses remain ordinary premise-sensitive steps, and discharging it into a negated conclusion remains an ordinary semantic obligation.
- definitionEvery step in the supplied identifier list is semantically sound.
- definition
- definition
- definition
- definition
- definition
- definitionThe formula declared for a claim identifier, when that claim is present.
- definition
- definitionEvery source-mapped step whose justification contributes to the claim through declared premise-to-conclusion steps.
- definitionAll justification statuses contributed by the exact source-mapped origins of a claim. This records epistemic provenance; it does not assert any paper claim or discharge any physical assumption.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe declared argument step with the requested identifier, when present.
- definition
- definitionThe premise list and conclusion attached to a declared step identifier.
- definition
- definition
- definition
- definition
- definitionThe complete Lean-side fidelity certificate. The first conjunct is computed from source-map data; the second is supplied by checked route semantics; the third requires each declared independence boundary to have a countermodel.
- definition
- definition
- definition
- definition
- definitionA typed countermodel matrix avoids string-keyed audit rows. Each index selects one proposition-valued separation obligation.
- definition
- definitionEvery route actually declared in the source map has a semantic certificate under the paper-local interpretation.
- definition
- definition
- definitionOne countermodel row retains a weaker proposition while rejecting a stronger upgrade. This is a proposition, not a structure carrying proof fields.
- definition
- definition
- definitionIndependent dependency and epistemic ledgers must review the same actual source claims, including every public conclusion and the selected paper conclusion. Empty, duplicated, nonexistent, or one-sided entries are invalid.
- definitionEvery actually declared source route must have exactly one independently reviewed predecessor row. Correct rows for a selected subset are insufficient.
- definitionThe declared main conclusion must be exposed by at least one public route output, rather than existing only as an unexported source-map claim.
- definition
- definition
- definitionTwo finite lists describe the same dependency set. Duplicate expected entries are rejected so a ledger cannot pass by repeating a label.
- definitionEvery paper-level, claim-level, and step-level source reference is present and has a nonempty work and locator. PaperArgument.auditable separately checks that every claim and step carries at least one source.
- definitionA source reference is usable for review only when both the work and its locator are nonempty.
- definitionStatic fidelity checks that can be evaluated from a paper's source map alone. They do not assert the truth of any physical premise.
- definitionEvery declared output of a named source route holds under the semantic interpretation. This is the proof obligation discharged by paper-specific Lean theorems.
- definition
- definitionA route is fully certified only when both its individual steps and its declared outputs are semantically checked.
- definitionEvery source-mapped inference step in a named route is semantically sound.
- definitionEvery route named in the supplied identifier list is semantically certified.
- definition
- definition
- definition
- definition
- definition
- definitionThe source-mapped route with the requested identifier, when present.
- definition
- definitionThe public semantic interface inherited from predecessor routes. Descendants receive only declared route outputs, not every internal intermediate claim. Outputs still carrying a temporary reductio origin are excluded.
- definitionAll direct and inherited route dependencies. The route-order check separately ensures that the declared graph is acyclic and topologically ordered.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA smooth positive, integrable control of the linearization step. It is not asserted to be Landau's Maxwellian or a self-consistent damping solution.
- definition
- definition
- definition
- definitionThe three actual Cartesian velocity coordinates in equations (1)-(9).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe entire function on pp. 26-27 extends the actual reduced initial datum. Entirety alone supplies neither contour growth estimates nor residues.
- definitionOriginal equation (5), retaining the three-dimensional charge integral.
- definitionOriginal equation (4), at every actual velocity and nonnegative time.
- definitionGaussian normalization is explicit imported mathematics. It is not inferred from the name of the equilibrium distribution.
- definitionEquilibrium parameters alone, independent of initial-value evolution or the half-space boundary problem. Thermal energy is the source's kappa T.
- definitionThe half-line integral is the actual Laplace transform of the marginal. The continuation to the moving pole is a separate mathematical obligation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPage 29 discusses this transverse-velocity integral, not a single three-dimensional velocity slice. Integrability is required separately.
- definition
- definition
- definitionThe numerator in the transverse-integrated equation (8), p. 29.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-domain witness with a genuine normalized three-dimensional Maxwellian. The disturbance is zero, as allowed by arbitrary initial data.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe p. 29 remainder tends to zero. At zero frequency the leading term is constant; nonzero coefficient means persistence, not necessarily oscillation.
- definitionA contour estimate with an explicit positive decay rate. This upper bound alone does not assert that the rate is optimal or that the field is nonzero.
- definitionA normalized estimated mode, not the selected kinetic solution. Equations (16)-(20) specify its approximate rates but do not bound its field error.
- definition
- definitionA normalized positive Maxwellian is present, but its perturbation is zero. The candidate denominator still vanishes at p = -i for k = u = 1.
- definition
- definition
- definition
- definition
- definitionA fixed-velocity free-streaming phase. The following domain and inversion controls are transform diagnostics, not full Maxwellian/Poisson solutions.
- definition
- definition
- definition
- definition
- definition
- definitionLower operational inputs. Equations (8)-(10) are derived downstream, while inversion, integration by parts, and transverse integration retain their exact imported analytic content.
- definition
- definitionA named operational-transform output does not itself retain equations (6)-(10).
- definition
- definitionOriginal p. 26, equation (8): `f_p(v) = (p + i k v_x)^(-1) {g(v) + i k (e/m) phi_p (partial f_0 / partial v_x)}`.
- definitionOriginal p. 26, equation (9): the transformed potential is the initial-data velocity integral divided by the dielectric denominator before the transverse velocity integrations are performed.
- definitionOriginal p. 26, equation (7): `f(v,t) = (1/(2 pi i)) integral f_p(v) exp(p t) dp` along the vertical line `Re(p) = sigma > 0`. The formal reconstruction uses the symmetric truncated-contour limit at positive times. The initial value is supplied separately; the paper does not state an endpoint half-value rule.
- definitionOriginal p. 26, equation (6): `f_p(v) = integral_0^infinity f(v,t) exp(-p t) dt`.
- definitionOriginal p. 26, equation (10): after `u = v_x`, the potential uses the one-dimensional integrals of `g(u)/(p+i k u)` and `(d f_0/du)/(p+i k u)`.
- definitionThe exact output retains genuine integration domains and the initial datum in addition to equations (6)-(10).
- definitionEvery physical future time is represented with its actual coordinate. No negative-time history or injectivity of paper labels is required.
- definition
- definition
- definitionMultiplying equation (4) by the Laplace kernel and integrating. Linearity, the potential transform, and exchanging the velocity/time integrals remain explicit analytic inputs; neither quotient (8) nor (9) is assumed here.
- definitionEach finite inverse contour is parameterized by `p = sigma + i y`, with the orientation `dp = i dy`. The improper limit is separate.
- definition
- definitionThe displayed quotient formulas require nonzero wave number and electron mass; these are explicit source-domain hypotheses rather than totalized- division accidents.
- definitionThe actual equation-(6) integral only samples nonnegative physical times.
- definitionThe inverse contour in equation (7) lies at `Re(p) = sigma > 0`.
- definitionReduced initial data and the reduced equilibrium derivative are actual transverse velocity integrals, not independent functions with matching names.
- definitionLandau initially defines the operational transform only for `Re(p) > 0`.
- definitionSame source problem and coordinate choices, without any evolved output.
- definitionThe integration-by-parts output printed below equation (7). The derivative is that of the actual time signal, with positive-time differentiability and its own Laplace integrability obligation.
- definitionThe time-domain charge moment exists and closes the actual Fourier potential.
- definitionThe transformed equation (5), before solving for the potential.
- definitionTransverse integration turns equation (9) into (10) on the raw right-half-plane domain. Fubini/interchange remains an exact analytic input.
- definitionIntegrability of the actual Cartesian and longitudinal quotient integrands is required on the raw transform domain, not silently inferred from a value returned by Lean's totalized integral.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe initial state is computed from the supplied distribution and Poisson law.
- definition
- definition
- definition
- definition
- definition
- definitionAdmissible operational solutions, with both charge-density moments defined. No independent evolution or uniqueness predicate is supplied by a caller.
- definition
- definition
- definition
- definition
- definition
- definitionThe same charge-density moment fixes the Fourier potential by equation (5).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe contour estimate is imported analysis, not an implication from pole location alone. Its exponent is the real part of the selected field pole.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (45): the small negative-dielectric branch is a purely real monotone exponential approach to the selected bulk field.
- definitionEquation (44): the calculated large-distance field correction retains its `x^(2/3)` prefactor, stretched attenuation, and complex periodic phase.
- definitionEquation (41): the zero-wave-number kernel is fixed by the dielectric.
- definitionEquation (46): the small positive-dielectric branch has both a genuine oscillation wave number and Landau's exponentially small spatial decrement.
- definitionEquation (35) extends the field correction oddly away from the wall; the endpoint is excluded because Landau explicitly notes a discontinuity.
- definitionEquation (39): positive spatial wave number passes below the velocity pole, while negative wave number passes above it.
- definitionEquation (37): Fourier inversion of the physical half-space field correction. Evaluation of the integral remains imported mathematics.
- definitionEquation (25): the remote longitudinal electric field is `E_0 / epsilon`. The selected bulk amplitude is separate from the finite-distance profile.
- definitionEquation (24): `epsilon = 1 - omega_0^2 / omega^2`.
- definitionEquation (26): ideal reflection reverses the normal velocity at the wall.
- definition
- definitionLandau's displayed equations (6)-(10), attached to the selected plasma quantities rather than stored as a free-standing complex-valued formula.
- definitionThe source distinguishes the exact wall field from the near-resonance approximations, which incorrectly give zero at the wall.
- definition
- definitionElectric-field amplitude is obtained by the actual spatial derivative of the selected Fourier potential, with no charge or mass factor.
- definition
- definition
- definition
- definitionThe longitudinal half-space calculation has a positive plasma frequency, positive Debye length, and a nonzero applied electric-field amplitude.
- definition
- definition
- definitionEquations (1)-(5) and (6)-(10) describe the same physical component, initial datum, electron charge, and potential.
- definitionThe source supplies actual transform inputs, temporal response support, a future time, and a regular inverse contour, not an evolution or uniqueness conclusion. The kinetic/Poisson setup supplies the defined time-slice moments.
- definition
- definition
- definition
- definitionEquations (8)-(10) and p. 29 use genuine transverse marginals, including the derivative of the reduced Maxwellian. These integrability conditions exclude a zero value obtained from a nonintegrable Bochner integral.
- definition
- definition
- definition
- definitionLandau's equation-(6)-(10) readout is tied to the selected wave vector, initial perturbation, equilibrium distribution, transformed distribution, transformed potential, and actual integration operations. The abstract paper objects remain distinct from complex-valued source data until these bridges are supplied.
- definition
- definition
- definitionThe same Maxwellian fixes both scales in the initial-value and half-space branches. This condition imposes no initial-value evolution on the latter.
- definitionThe separate nearest-root calculation on p. 29 selects pi rather than 3 pi, 5 pi, and higher phases. Phase congruence alone does not supply this.
- definitionLandau discusses regularity sensitivity and velocity-resolved oscillation adjacently, but the second calculation depends on the initial-value solution, not on the nonsmooth-data branch.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe source calculation supplies transform interpretation and lower integrated equations, not the desired quotient formulas (8)-(10).
- definition
- definitionPage 29: the actual marginal's Laplace formula, a locally analytic numerator, an uncancelled residue, and the contour-inversion remainder. The last two conditions are explicit; a denominator zero by itself proves no nondecay.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionJournal p. 29, equation (19) and the printed definition of xi.
- definitionOriginal p. 28, Eq. (17): Landau's approximate damping decrement is the exponentially small long-wave estimate, with the same selected `ω₀`, `k`, and Debye-Hückel scale `a` as equation (16).
- definitionOriginal p. 28, Eq. (16): the imported Vlasov frequency calculation retains the first long-wave correction to the plasma frequency.
- definitionJournal p. 29, equation (20), with v_th = omega_0 times a.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe `x^(2/3)` source exponent is expressed as a physical positive dimensionless ratio, not as a named stretched-exponential predicate.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionLandau provenance separately requires the actual one-sided formulas.
- definition
- definition
- definition
- definition
- definition
- definitionThe common positive-value branch for Landau's p. 28 long-wave estimates. Here `plasmaFrequency` is the uncorrected `ω₀`, while `longWaveFrequency` below is the estimated `ω` of equation (16). The coarse ka < 1 condition is not the source's stronger ka << 1 qualification or an accuracy bound.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (46)'s positive-dielectric spatial damping decrement.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionJournal pp. 28-29: ka > 1 is a branch selector for the large-k approximation, not a quantified rate or field-error bound.
- definition
- definitionIn Landau's large-wave-number regime the actual decrement dominates.
- definition
- definition
- definition
- definition
- definition
- definitionLandau's actual Fourier wave vector is the shared description. The evolved electron perturbation, equilibrium electron reference, fixed ion background, linear kinetic equation, and electron-density Poisson closure stay separate.
- definitionLandau's selected initial-data problem as a temporal response context.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA precise suppression statement for the actual equation-(17) function. Its technical limit calculation may remain an explicit mathematical input.
- definition
- definitionThe p. 29 phase congruence does not distinguish the first odd phase from higher odd phases. The nearest-root selection is an additional calculation.
- definition
- definition
- definition
- definition
- definitionExplicit auxiliary-function analysis of equation (19). The coefficient four refines the printed logarithmic scaling of this implicit approximate equation; it is not a claim about exact dispersion roots.
- definitionThis context compares two retained frequency estimates. Its validity domain is not a claim of empirical adequacy or exact Vlasov-field accuracy.
- definition
- definition
- definition
- definitionAll wavelength limits vary the actual wave number at fixed Maxwellian parameters. These are the printed estimates, not exact dispersion roots.
- definition
- definition
- definition
- definition
- definition
- definitionReparameterize the approximate modulus equation by a positive xi value. This gives concrete finite-k controls without postulating a global inverse.
- definition
- definition
- definition
- definitionForward uniqueness restricted to one selected initial state and time. This is the appropriate contract when a physical argument does not assert global forward uniqueness over every state represented by the carrier type.
- definitionAt least one forward continuation exists for the selected time and state.
- definitionOne forward continuation exists and every continuation from the same selected state and time is that continuation. This is nonvacuous, unlike uniqueness alone.
- definition
- definition
- definition
- definition
- definition
- definitionThe selected response kernel has no support from a later source time.
- definitionFor the selected problem, dependence holds exactly when stimulus and response occur and the response kernel connects their times.
- definitionEvery declared dependence has a source no later than its response.
- definitionThe selected response relation is physically inhabited by an occurring stimulus, an occurring response, and a dependence between them.
- definitionA nonvacuous retarded response: all response dependence is past-supported and at least one occurring stimulus-response pair realizes that dependence.
- definition
- definition
- definition
- definition
- definition
- definitionThe target's activity is the shared prediction-sector condition, not a second approximation-specific notion of having a prediction.
- definition
- definition
- definition
- definition
- definition
- definitionA selected observable sector.
- definitionA description makes at least one prediction in the selected sector.
- definitionOne description approximates another when every target prediction in the selected sector has an agreeing prediction in the approximating description. The direction is intentional.
- definitionExtensional agreement of two prediction relations on a selected sector. This low-level relation may hold vacuously when the sector or both prediction relations are empty; `EmpiricallyEquivalent` adds a common prediction.
- definition
- definition
- definitionBuild the epistemic dependency basis in paper order. A conclusion inherits the justification origin of its own step and every origin already attached to its premises.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExpand a set of route identifiers by one dependency edge, iterated with enough fuel to traverse any acyclic graph on the declared routes.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
Selected instances and coercions
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- constructor
- definition
- checked statement
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- checked statementRaw paper-local inputs construct every Landau route in source order.
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA nonempty comparison of the two retained frequency estimates, not an accuracy theorem for the exact Vlasov solution.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe completed source atom preserves the formulas and eventual large-k dominance.
- definition
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- recursor
- definition
- checked statement
- checked statementNo completed route certificate is needed to cover a route identifier.
- checked statementThe certified short-wave atom retains the actual equations (19)-(20).
- checked statement
- checked statementThe source input now derives the distribution quotient through the actual time-derivative transform, rather than accepting equation (8) as an input.
- checked statementThe same raw source input supplies a genuine Cartesian velocity average and derives equation (9) by Poisson closure and integral linearity.
- checked statementRaw normal-mode and Laplace inputs expose the displayed equations (6)-(10) before the initial-value route is certified.
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statementThe printed equations (6)-(10) are retained from the checked normal-mode result and one-sided transform calculation, not introduced as an unearned operational-formula label.
- definition
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Checked statements: parameters, hypotheses, and interpretation
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA bound for the estimated mode transfers only with a separate bound for the actual signal minus that mode. This is not supplied by a rate formula.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEven an arbitrarily small rate error can invalidate an eventual envelope at the estimated rate. Both functions here are actual smooth damped modes.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementEquation (10) is reconstructed from equation (9) and the explicit transverse-velocity reduction; it is not a second unrelated potential label.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe paper's fixed-ion setup directly supplies both collisionless equations; no contour deformation, damping, or BGK trapped population is assumed.
- checked statement
- checked statementThe completed paper retains the printed short-wave values and dominance.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementFinished outputs retain the actual selected distribution and electric field without reconstructing stronger calculation inputs backward.
- checked statementThe shared collisionless kinetic/Poisson state does not turn the damping of Landau's collective electric field into damping of each velocity component.
- checked statementThe linear fixed-ion kinetic/Poisson route receives Landau's own one-sided initial-value source, rather than BGK's stationary energy-orbit derivation.
- checked statementRaw normal-mode and one-sided-transform inputs expose the source equations (6)-(10) before any contour continuation or damping conclusion is used.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe completed long-wave route retains both displayed p. 28 values while keeping equation (16)'s imported calculation separate from equation (17)'s local Landau calculation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA selected finite-k dominance statement needs this additional criterion; ka > 1 alone does not select a point in the eventual asymptotic tail.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe short-wave branch retains Landau's actual equations (19) and (20).
- checked statement
- checked statement
- checked statement
- checked statementDominance is eventual along the actual large-k family. The coarse ka > 1 selector does not supply this inequality at every selected finite wave number.
- checked statementSource-sensitive shared reuse retains Landau's printed formulas (6)-(10).
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe transformed-formula result retains Landau's displayed equations (6)-(10), not only a named transform calculation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAn algebraic extrapolation of the printed long-wave estimate. This large-k limit is not asserted to approximate the physical damping rate.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
External mathematical declarations
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
This edition follows the Lean semantics, source map, coverage proofs, and independent fidelity certificate. One-sided transform identification, inverse limits, integrated kinetic/Poisson equations, integral interchanges, contour estimates, and asymptotic remainder calculations remain explicit inputs. Their actual integrands, domains, transverse reduction, and physical readout calibrations are retained. Lean derives the quotient formulas, selected-mode uniqueness, field decay, and marginal nondecay; it does not receive these final outcomes as calculation hypotheses. Retarded support, nonzero residue, and nonzero oscillation frequency retain their separate roles. The neighboring nonsmooth-data assertion, wavelength approximations, half-space analysis, and numerical scope retain their own unproved source inputs. Every dependent route recovers its predecessor physics from certified outputs.
Two independent boundary-value problems meet only in the final scoped assessment
The collisionless initial-value root first rejects an insufficient normal-mode treatment, then proceeds through Laplace evolution, analytic continuation, and collective pole damping. That chain branches into long-wave and short-wave asymptotics, plus a late-time route that keeps regularity-sensitive field behavior separate from the initial-value moving-pole distribution behavior. The independent half-space root uses a frequency prescription to select a finite boundary solution, then derives spatial penetration asymptotics while retaining the need for numerical evaluation. The complete result conjoins both physical stories without treating one as a premise of the other.
| Transition | Status | Retained boundary |
|---|---|---|
| Collisionless setup to rejection of normal modes | paper obstruction | The failure concerns the general prescribed initial-value problem. |
| Normal-mode obstruction to retarded, unique evolution | source-derived mode reconstruction | Actual inverse limits and a common zero-free contour derive selected uniqueness; an admissible readout supplies existence. Temporal response support remains a separate input. |
| Entire datum to controlling singularity | contour-deformation argument | The velocity contour passes below the moving pole. |
| Left-half-plane poles to field damping | pole and decrement calculation | The conclusion is collective-field damping, not distribution relaxation. |
| Long-wave damping formula | imported frequency + controlled approximation | Equation (16) is retained but its detailed Vlasov derivation is omitted; equation (17) is retained as Landau's local decrement. |
| Short-wave frequency and decrement | separate controlled asymptotics | Frequency stays below decrement, with frequency/wave number tending to zero and decrement/wave number tending to infinity; no extrapolation from the long-wave formula is used. |
| Initial regularity to late-time behavior | regularity calculation | Smooth-data damping need not survive a derivative discontinuity. |
| Initial-value solution to velocity-resolved motion | moving-pole calculation | The undamped component result is not supplied by the nonsmooth-data branch. |
| Resonant half-space integral to finite solution | frequency and contour prescription | The integral alone does not select a unique contour. |
| Half-space solution to penetration profile | controlled asymptotics + deferred evaluation | The general field integral is not obtained in closed form. |
The collisionless equations define an initial-value problem that the normal-mode ansatz does not solve
The physical setup fixes the ions, neglects both electron–electron and electron–ion collisions, and takes a small perturbation of an equilibrium electron distribution. A linearized kinetic equation is coupled to Poisson's equation. Spatial Fourier components decouple, a wave vector is selected, and the initial distribution is prescribed.
KineticFormulaReadout makes this setup concrete. Its equilibrium is a normalized three-dimensional Maxwellian; its electron charge is signed and negative, and the fixed positive ion charge compensates the equilibrium electron density. Equations (4) and (5) use actual time derivatives and the actual three-dimensional velocity integral of the selected disturbance. The same distribution, initial datum, equilibrium derivative, charge, mass, and potential are tied to the operational-transform readout by KineticFormulaReadoutRepresentsSelectedPhysicsAt.
R[F0+af,aφ] = aL[f,φ] − a2(q/m)∂xφ∂vf,
∂tfk + ikvxfk − ik(q/m)φk∂vxF0 = 0, k2φk = 4πq∫fkd3v.
source_equation_four_is_the_actual_spatial_fourier_equation and source_equation_five_is_the_actual_spatial_poisson_equation; source equations (1)-(5)
(K1)
The shared calculation proves that the linearized equation is the first variation at zero amplitude, including its omitted quadratic force. A Gaussian equilibrium with zero disturbance realizes the complete source domain. A separate positive integrable first-order control has nonlinear residual 1/2, so the approximation cannot be promoted to an exact nonlinear solution. That control is not claimed to be Landau's Maxwellian damping solution or a self-consistent field calculation. See normalized_maxwellian_control_realizes_source_equations and positive_integrable_first_order_solution_is_not_an_exact_nonlinear_solution.
The normal-mode assessment then records four defects at fixed wave vector: the velocity integral diverges, assigning its principal value is not justified, the frequency is not unique, and the normal-mode family is insufficient for arbitrary initial data.
⇒ divergent velocity integral + unjustified principal value + nonunique frequency + failure to represent arbitrary prescribed initial data
⇒ the normal-mode treatment is insufficient for the general initial-value problem.
divergent_normal_mode_integral_does_not_solve_arbitrary_initial_data; journal pp. 25–26
(1)
The conclusion is diagnostic rather than nihilistic: it motivates a method that keeps the prescribed initial distribution throughout the calculation.
One-sided Laplace transformation gives retarded and nonvacuously unique evolution; contour deformation then selects late time
Transformed initial-value solution
The operational calculation uses actual Lebesgue time and velocity integrals. The source readout covers physical future time and Cartesian velocity coordinates, fixes the initial datum, and requires integrability of the transform and velocity quotient integrands on the established right-half-plane domain. The reduced functions are actual transverse marginals. The inverse is a limit of finite vertical contours with positive real part. Lean derives equation (8) from the integration-by-parts and integrated kinetic inputs, equation (9) from actual velocity integration and transformed Poisson closure, and equation (10) from transverse reduction. Two admissible readouts with the same input data then give the same mode on a common zero-free inverse contour. The inverse limits derive positive-time equality, while the prescribed initial datum fixes the endpoint. Inversion, analytic domains, and temporal response support remain explicit inputs; existence and selected uniqueness are derived.
f(v,t) = (2πi)−1∫σ−i∞σ+i∞ fp(v)eptdp,
fp(v) = (p+ikvx)−1{g(v)+ik(e/m)φp∂f0/∂vx},
φp = (4πe/k2) I3d(g)/(1−(4πie2/km)I3d(∂f0)),
φp = (4πe/k2) Iu(g)/(1−(4πie2/km)Iu(df0/du)).
Raw transform domain: Re(p) > 0; sigma > 0; t > 0 for inversion; g(v)=f(v,0) separately.
Actual time/velocity integrability and nonzero displayed denominators are required.
EquationsSixThroughTenFormulaAt; equations (6)–(10), journal p. 26
(2a)
g_bar(u) = integral g(u,v_y,v_z) dv_y dv_z, with integrable transverse profiles.
B_R(t) = (2 pi i)^(-1) integral_-R^R F(sigma+i y) exp((sigma+i y)t) i dy.
R -> infinity: B_R(t) -> f(t), for t > 0 and sigma > 0.
FutureTimeCoordinatesAt, ReducedVelocityMarginalsAt, and EquationSevenInverseTransformAt. Positive-time limiting reconstruction; initial data are separate.
(2b)
k^2 Phi = 4 pi e integral F(v) dv; alpha = 4 pi e/k^2; c = i k e/m.
Actual integral linearity gives integral F = N + c Phi J.
D = 1 - alpha c J; D != 0 implies Phi = alpha N/D.
CalculationInputsAt supplies lower integrated equations and analytic domains, not the quotient conclusions (8)-(10).
(2c)
At p=-1 the time integrand is not integrable; the analytic continuation is F(-1)=-1.
B_R(0)=arctan(R)/pi -> 1/2, while f(0)=1.
The symmetric contour limit exists although the whole-line contour integrand is not absolutely integrable.
A zero functional ignores the past but gives 0 instead of the actual Laplace value 1 at p=1. Scalar transform diagnostics, not full kinetic/Poisson solutions or an endpoint claim printed in the original paper. (2d)
D(sigma+i y) != 0 for every real y; sigma > 0.
Equations (8)-(9) imply Phi_1(p)=Phi_2(p) and F_1(p,v)=F_2(p,v) on that contour.
Common inverse limits imply f_1(v,t)=f_2(v,t) for every v and t > 0.
At t=0, equality follows from g(v), not from an endpoint inverse formula.
SameInitialValueProblemAt, ZeroFreeInverseContourAt, and source_reconstruction_determines_the_actual_mode_state. Input agreement contains no evolved-output equality.
(2e)
k != 0; both initial and selected-time charge-density moments are integrable.
E_k(t) = -i k phi_k(t), identified with the selected physical field.
Evolution means an admissible readout with the same source inputs and this actual final mode.
FourierModeState, modeDynamics, InitialDensityDefinedAt, and ModeDensityDefinedAt. No arbitrary state label or supplied evolution predicate.
(2f)
⇒ an actual selected Fourier-mode continuation exists and every admissible competitor equals it.
Separate represented, past-supported initial-data dependence ⇒ retarded field response.
laplace_formulas_establish_nonvacuous_deterministic_evolution and initial_value_result_retains_the_actual_selected_mode_and_field. No independent global-determinism premise, arbitrary-data PDE well-posedness, or determination of unrepresented modes.
(2)
Both are smooth, real, and positive; f(0)=h(0)=1.
Both actual Laplace integrals at p=1 exist and equal 1/2.
f(log 3)=1/3, while h(log 3)=11/27.
one_laplace_sample_and_the_initial_value_do_not_determine_the_history. One transform sample is not a whole inverse contour. These are operational signals, not kinetic/Poisson solutions.
(2g)
phi_b(x)=cos x+(b/4)cos(2x); E_b(x)=sin x+(b/2)sin(2x).
f_b(x,v)=G(v)[1-a cos x-b a cos(2x)] >= 0.
e=-1; E_b'(x)=4 pi e integral [f_b(x,v)-G(v)] dv; E_b=-phi_b'.
The selected k=1 mode agrees, but E_1(pi/4)-E_0(pi/4)=1/2.
one_selected_fourier_mode_does_not_determine_the_complete_physical_field. Actual initial electrostatic data with integrable densities, not a claimed full time-dependent kinetic solution.
(2h)
phi=0 and phi=1 both obey Poisson; both have E=-i k phi=0.
zero_wave_poisson_does_not_fix_the_constant_potential_but_the_fields_agree. Potential gauge freedom is not electric-field nonuniqueness.
(2i)
On Re(p)=1 both equal the actual Laplace transform of the independent damped signal.
At p=-2+4i the totalized R is zero while F is nonzero.
Agreement on the common contour and explicit positive-time inverse limits suffice for uniqueness. The internal client constructs its own signal and rationalized expression. No global complex-function equality or automatic inversion theorem is assumed. (2j)
lower_operational_inputs_derive_equations_six_through_ten assembles the derived quotient chain. named_operational_transform_output_does_not_supply_equations_six_through_ten retains real time/velocity coordinates and a named nonzero transform, but fails the actual zero-signal integral. The independent Landau operational client constructs a different damped complex signal, verifies its actual transform on Re(p)>-2, changes its prehistory, and calibrates a rescaled clock. Its transform exists even at p=-1: continuation is not being conflated with a blanket prohibition on left-half-plane time integrals. Neither this signal nor the scalar controls is asserted to solve the full plasma problem. Retarded support and deterministic uniqueness remain separate conclusions, tested by unique_forward_evolution_does_not_establish_retarded_response and forward_existence_does_not_establish_determinism.
Analytic continuation
For the first damping analysis, the actual transverse-integrated initial datum must have an entire complex extension. The operational reduced datum is calibrated to that same function, with transverse integrability retained. This is separate from local analyticity of the later p-plane numerator. The velocity-contour deformation and inverse-contour shift remain additional mathematical inputs; entirety alone is not a growth estimate.
exists G : Complex -> Complex, analytic at every complex point, G(u) = g_bar(u) for every real u.
EntireInitialMarginalExtensionAt and certified_analytic_route_retains_actual_entire_initial_data; journal pp. 26-27. The actual transverse integrals and operational initial values must agree.
(3a)
⇒ the singularity nearest the imaginary axis controls late-time behavior.
entire_initial_data_and_deformed_contour_determine_late_time_pole; journal pp. 27–28
(3)
The contour choice is part of the physical-mathematical argument. It is not replaced by a principal-value convention.
The contour estimate gives collective-field decay, with distinct long- and short-wave regimes
The supplied pole calculation identifies the dominant field pole and the contour estimate on the actual potential. The decrement is minus that pole's real part. The Fourier spatial derivative fixes the electric field, and Lean derives both limits. A pole location alone is not a bound on an arbitrary signal.
=> phi_k(t) -> 0 and E_k(t) -> 0.
CollectivePoleEstimateAt and collective_damping_retains_actual_spatial_electric_field_limit; journal p. 27, equations (12)-(13). The bound does not assert an optimal rate or nonzero field amplitude.
(4)
Two wavelength limits
omega_0 a = sqrt(Theta / m).
PlasmaScaleCalibrationAt and calibrated_plasma_scales_retain_source_values; journal p. 28, equations (15)-(16). Theta is thermal energy; n, m, and Theta are positive and e is the signed negative electron charge. The independent half-space branch retains the same equilibrium calibration.
(4a)
The rate formulas below describe estimated modes, not exact field solutions. Each is an actual function of real wave number at fixed Maxwellian parameters. The source requires a small- or large-parameter asymptotic regime; the coarse ka < 1 and ka > 1 branch selectors are not numerical accuracy guarantees. Auxiliary mathematical limit calculations remain explicit hypotheses, from which Lean derives the observable limits.
| Regime | Additional inputs | Checked conclusion | Status |
|---|---|---|---|
| Long wave | Calibrated scales; the equation-(16) frequency estimate imported from Vlasov; equation-(17) decrement estimate and its suppression as k tends to zero from above | Actual frequency, decrement, and relative-damping limits, plus decay of the estimated mode. No global converse from small relative damping to long-wave validity. | imported frequency + asymptotic approximation |
| Short wave | Calibrated scales; the equation-(19) auxiliary function and its mathematical limits; the separately selected principal phase | Derived equation-(20) rates, their actual large-k limits, and eventual decrement dominance. No exact target-field error bound. | asymptotic approximation |
γ = ω0√(π/8)(ka)−3 exp[−1/(2(ka)2)]
positive estimated decrement => the estimated mode tends to zero.
k -> 0+: omega_L(k) -> omega_0, gamma_L(k) -> 0, gamma_L(k)/omega_L(k) -> 0.
LongWaveLimitsAt and certified_long_wave_route_retains_actual_parameter_family; journal p. 28, equations (15)-(17). The explicit mathematical suppression input is gamma_L(k)/k^n -> 0 for every natural n as k -> 0+. This is not a numerical accuracy guarantee at every ka below one.
(5a)
k -> infinity: omega_S(k), gamma_S(k) -> infinity, omega_S(k)/k -> 0, gamma_S(k)/k -> infinity, omega_S(k)/gamma_S(k) -> 0.
omega_S(k) < gamma_S(k) eventually as k -> infinity; gamma_S(k)/(omega_S(k) log(ka)) -> 4/pi.
ShortWaveXiLimitCalculationAt, short_wave_auxiliary_limits_give_observable_hierarchy, and certified_short_wave_route_retains_actual_parameter_family; journal pp. 28-29, equations (18)-(20). The explicit auxiliary inputs are xi -> infinity, k/xi -> infinity, and xi^2/log(ka) -> 4. The coefficient 4/pi refines the implicit approximate equation, not an exact dispersion-root theorem or a literal source quotation. Equation (20) additionally requires the principal-phase selection below.
(5b)
||E(t) - E_est(t)|| <= B exp(-gamma_est t) eventually
=> ||E(t)|| <= (|A| + B) exp(-gamma_est t) eventually.
WavelengthApproximationErrorAt and wavelength_error_control_yields_actual_field_envelope. This is a conditional reconstruction with an additional error hypothesis, not an error estimate supplied by the original paper.
(5c)
Their actual logarithmic decay rates differ by epsilon, but no finite C bounds ||E(t)|| by C exp(-(1+epsilon)t) eventually.
arbitrarily_close_decay_rates_do_not_supply_an_exact_envelope. This smooth-mode counterexample rejects rate-only inference; it does not assert that these arbitrary modes solve the plasma equations.
(5d)
theta = (2r+1) pi satisfies the congruence for every natural r.
Separate nearest-root selection: theta = pi.
every_short_wave_branch_satisfies_phase_congruence and equation_nineteen_and_principal_phase_yield_equation_twenty; original p. 29. Higher odd phases also satisfy the phase equation. Their exclusion is a separate source calculation, not a consequence of the congruence or of the branch-independent leading decrement.
(5e)
xi = 1, k = sqrt(sqrt(2 pi) exp(1/2))/a: ka > 1 and the modulus equation holds, but omega_S > gamma_S.
pointwise_short_wave_dominance_iff_auxiliary_large and coarse_short_wave_point_does_not_have_decrement_dominance. The calibrated control tests the inference from a coarse threshold, not accuracy of an exact plasma root. A separate xi = 10, theta = 3 pi control retains both the modulus equation and damping dominance without selecting the principal branch.
(5f)
For every 0 < k < delta: |omega_L(k) - omega_0| <= epsilon |omega_0|, yet omega_L(k) > omega_0.
certified_long_wave_route_realizes_nonempty_frequency_approximation uses the shared ScaleAndRegime matched-prediction theorem. This compares two retained frequency estimates, not either estimate with the exact Vlasov solution. The interval is nonempty and the predictions are not exactly equal.
(5g)
Separately, omega(k) = 2 v_th k and gamma(k) = v_th k both grow without bound, but gamma(k) never dominates omega(k) for k > 0.
small_extrapolated_relative_damping_does_not_select_long_wavelengths and unbounded_rate_growth_does_not_give_eventual_decrement_dominance. These controls reject invalid converses; they do not extend validity of the long-wave approximation or assert physical dispersion relations for the test rates.
(5h)
long_wave_result_retains_imported_frequency_and_local_decrement extracts the precise division of labor: the frequency is reused from Vlasov and its derivation is omitted, while this paper supplies the decrement formula. long_wave_result_retains_equations_sixteen_and_seventeen separately exposes the two displayed values without collapsing those source statuses. short_wave_result_retains_ordered_asymptotic_regime extracts eventual decrement dominance and actual limits of the two wave-number ratios.
Two adjacent late-time calculations must not be collapsed
The source's regularity calculation introduces a continuous perturbation with a discontinuous derivative and asserts a qualitatively different, undamped field response. This remains an explicit unproved source input. It is not derived from the entire-data contour estimate, and the formalization does not claim a mathematical regularity theorem validating this assertion.
⇒ the associated nonsmooth field does not damp; replacing the entire datum by this piecewise-linear datum changes damping qualitatively.
initial_regularity_controls_collective_field_damping_scope; journal p. 29, conditional on the separate source calculation.
(6)
Landau then analyzes the distribution integrated over the two transverse velocities. This separate calculation uses the initial-value solution, not the derivative-discontinuous datum. The formalization retains its actual half-line Laplace integral and the locally analytic resolvent numerator. Analyticity supplies continuity for the punctured-plane residue limit; an uncancelled residue and a vanishing inversion remainder imply nondecay. These are explicit qualifications of the reconstruction, not assumptions quoted verbatim from the paper.
numerator analytic near p_v; f_bar(u,t) - A(u) exp(-i k u t) -> 0, A(u) != 0
=> ||f_bar(u,t)|| -> ||A(u)|| > 0.
VelocityPoleAsymptoticsAt, longitudinal_resolvent_has_residue, and nonzero_asymptotic_coefficient_prevents_decay; original p. 29, unnumbered formulas.
(6a)
longitudinal marginal at selected u with A(u) != 0: frequency omega = k u, persistent leading phase, no damping
ku != 0 is required for oscillation; ku = 0 gives a constant leading phase.
moving_velocity_pole_yields_undamped_velocity_resolved_distribution and collective_field_damping_coexists_with_undamped_velocity_distribution; journal p. 29. Equation (21) belongs to the half-space problem, not this marginal argument.
(7)
regularity_sensitivity_and_velocity_pole_results_remain_independent joins the two results only after recovering their distinct inputs. A normalized Maxwellian with zero disturbance satisfies the actual kinetic and Poisson equations but has a canceled candidate denominator zero and a decaying zero marginal. The counterexamples denominator_zero_does_not_establish_an_uncancelled_residue and denominator_zero_does_not_establish_marginal_nondecay reject promotion of that denominator zero to a nonzero residue or to nondecay. The older collective/distribution and nonsmooth-data controls remain separate. Nothing here asserts entropy production, collisional equilibration, or microscopic irreversibility.
A positive-imaginary-frequency prescription selects the finite longitudinal half-space solution
The second independent root applies a monochromatic longitudinal external field to a plasma occupying a half-space with an ideal reflecting wall. The transverse problem is excluded, and a dielectric boundary condition fixes the behavior at infinity.
The calculation first gives the external frequency a positive imaginary part and removes it only after selecting the finite solution. It solves the half-space kinetic equation, extends the spatial profile oddly, Fourier transforms it, and encounters a resonant velocity integral. The same frequency prescription fixes the resonant contour.
⇒ a finite Fourier half-space solution with a uniquely fixed resonant velocity contour.
positive_imaginary_frequency_prescription_selects_half_space_solution; journal pp. 30–32
(8)
The prescription is logically indispensable. resonant_integral_without_prescription_does_not_select_unique_contour gives two admissible unprescribed contours and proves that existence of an admissible contour does not select a unique one.
Spatial penetration separates far attenuation and two dielectric resonance branches
Starting from the prescribed half-space solution, the asymptotic calculation classifies the first far-distance term by the sign of the dielectric value. The far profile combines stretched-exponential attenuation with a periodic spatial factor.
| Profile | Dielectric regime | Spatial behavior |
|---|---|---|
| Far-distance profile | Classified by dielectric sign | Stretched-exponential attenuation multiplied by a periodic factor. |
| Negative resonance branch | Small negative dielectric value | Monotone exponential approach to the bulk field. |
| Positive resonance branch | Small positive dielectric value | Spatial oscillation about the bulk field with a small damping decrement. |
| General profile | No special closed-form branch | Requires numerical evaluation and is not evaluated in closed form in the paper. |
⇒ stretched-exponential periodic far attenuation, monotone small-negative-dielectric approach, damped small-positive-dielectric spatial oscillation, and no claimed closed-form evaluation of the general profile.
spatial_asymptotics_retain_distinct_resonance_branches_and_numerical_scope; journal pp. 32–34
(9)
external_penetration_result_retains_deferred_general_evaluation extracts the unresolved numerical obligation directly from the final penetration result.
The complete result is a scoped conjunction, not a relaxation or irreversibility theorem
The paper-level theorem collects nine route results: normal-mode insufficiency, the initial-value solution, analytic continuation, collective-field damping, long-wave damping, short-wave asymptotics, regularity and distribution behavior, the causal half-space solution, and external penetration.
⇒ complete scoped collisionless-damping and penetration assessment.
paper_routes_establish_scoped_collisionless_damping_and_penetration
(10)
Because the complete result contains the underlying route propositions, it retains the imported long-wave frequency, both controlled wavelength approximations, both contour-deformation arguments, and the deferred numerical evaluation. It also retains the collisionless premise and the explicit separation between collective and velocity-resolved dynamics. Thus “damping” here cannot be promoted to a theorem of collision-driven equilibration, entropy increase, or microscopic loss of reversibility.
Concept guide
Collisionless linear regime
Stationary ions, neglected electron collisions, a small perturbation, and linearized kinetic–Poisson evolution of decoupled Fourier components.
CollisionlessInitialValueSetupNormal-mode insufficiency
The combined divergence, prescription, frequency-nonuniqueness, and arbitrary-initial-data obstruction to the naive eigenmode treatment.
NormalModeInsufficiencyResultRetarded initial-data response
A witnessed dependence of the selected later electric field on the prescribed initial distribution, represented by a kernel with no support from a source later than its response.
RetardedInitialValueFieldAtNonvacuous unique evolution
An actual admissible Fourier-mode reconstruction supplies existence. The same input data, common inverse contour, explicit initial endpoint, and Poisson closure derive selected uniqueness and the physical field readout.
InitialValueSolutionResult · FourierModeState · modeDynamicsLandau contour deformation
Passage below the moving velocity pole followed by a leftward inverse-transform contour shift that exposes the late-time singularity.
AnalyticContinuationResultCollective field damping
Decay of the potential and electric field governed by the nearest relevant pole in the left half-plane.
CollectiveFieldDampingResultLong-wave regime
The controlled small-wave-number result combining an imported Vlasov frequency with Landau's locally calculated, exponentially small decrement.
LongWaveDampingResultShort-wave regime
The separate asymptotic branch in which frequency and decrement grow, decrement exceeds frequency, frequency/wave number tends to zero, decrement/wave number tends to infinity, and their relative ratio grows.
ShortWaveAsymptoticResultRegularity sensitivity
The dependence of late-time field behavior on singularities of the initial velocity profile, including derivative discontinuities.
RegularityAndDistributionResultDynamical-level separation
Collective-field decay can coexist with a nondecaying longitudinal marginal at a selected velocity whose moving-pole residue is nonzero. Oscillation additionally requires nonzero frequency.
CollectiveFieldDistributionSeparationPositive-frequency prescription
The temporary positive imaginary part of the driving frequency that selects the finite solution and fixes the resonant contour.
CausalHalfSpaceResultPenetration branches
The far-distance, small-negative-dielectric, and small-positive-dielectric spatial asymptotics of the driven half-space field.
ExternalPenetrationResultDeferred numerical scope
The explicit statement that the general penetration integral requires numerical evaluation and is not closed in the paper.
GeneralPenetrationNumericalScopeComplete route inventory, blocked shortcuts, and provenance
The source map declares ten routes, twenty-eight claims, and twenty-eight sourced steps. Coverage interprets every atom, certifies every route, and proves exhaustive realization. Calculation contracts and local/imported inputs are independent hypotheses; result steps alone apply them to certified predecessor outputs. The nine-part complete result is the declared main conclusion.
| Route | Direct dependencies | Declared output | Profile |
|---|---|---|---|
| Normal-mode insufficiency | — | Collisionless setup plus complete normal-mode obstruction | independent physical root |
| Initial-value solution | Normal-mode insufficiency | Value-level equations (6)–(10), transform formulas, and unique selected forward evolution | operational calculation |
| Analytic continuation | Initial-value solution | Nearest singularity controls late time | deformation argument |
| Collective-field damping | Analytic continuation | Potential and field damping with a decrement | pole calculation |
| Long wavelength | Collective damping | Small exponentially suppressed decrement | imported frequency + controlled approximation |
| Short wavelength | Collective damping | Ordered asymptotics: frequency below decrement, two wave-number ratios, and logarithmic relative-ratio growth | controlled asymptotics |
| Regularity and distribution | Collective damping + initial-value solution | Independent regularity-sensitive field result and moving-pole distribution result, then field/distribution separation | two late-time calculations |
| Causal half-space | — | Finite prescribed Fourier boundary solution | independent deformation root |
| Penetration asymptotics | Causal half-space | Three spatial regimes and retained numerical scope | controlled approximation + deferred evaluation |
| Complete assessment | All nine prior routes | Complete scoped conjunction | logical synthesis |
Normal modes · normal_mode_insufficiency_route_is_semantically_realized
Initial value · initial_value_solution_route_is_semantically_realized
Analytic continuation · analytic_continuation_route_is_semantically_realized
Collective damping · collective_field_damping_route_is_semantically_realized
Long wave · long_wavelength_route_is_semantically_realized
Short wave · short_wavelength_route_is_semantically_realized
Regularity · regularity_and_distribution_route_is_semantically_realized
Half space · causal_half_space_route_is_semantically_realized
Penetration · penetration_asymptotics_route_is_semantically_realized
Complete paper · complete_assessment_route_is_semantically_realized
All twenty-eight source-mapped claims
| Claim group | Primary anchor | Status |
|---|---|---|
| Collisionless setup, normal-mode assessment, insufficiency | pp. 25–26, equations (1)–(3) | Physical principle, paper obstruction, logical composition |
| Laplace calculation, equations (6)–(10) formula, and initial-value result | pp. 26–27, equations (4)–(10) | Paper calculation, value-level source retention, and checked composition |
| Entire datum, contour calculation, continuation result | pp. 27–28, equations (11)–(12) | Physical setup, deformation argument, checked composition |
| Pole calculation and field-damping result | pp. 28–29, equations (13)–(14) | Paper calculation and checked composition |
| Long-wave setup, Vlasov input, decrement calculation, result | p. 28, equations (15)–(17) | Controlled approximation, imported result, controlled calculation |
| Short-wave setup, calculation, result | pp. 28–29, equations (18)–(20) | Controlled approximation and checked composition |
| Regularity calculation, moving-pole distribution calculation, result, field/distribution separation | p. 29, unnumbered marginal formulas | Separate source calculations, actual limits, and explicit residue/frequency qualifications |
| Half-space setup, causal calculation, result | pp. 30–32, equations (22)–(34) | Physical principle, deformation argument, checked composition |
| Penetration calculation, numerical scope, result | pp. 32–34, equations (35)–(44) | Controlled approximation, deferred calculation, checked composition |
| Complete paper result | pp. 25–34 | Checked logical synthesis |
Nine formally blocked shortcuts
The finite plasma witnesses retain the positive long-wave frequency, wave number, Debye-Huckel scale, the ka < 1 domain and equations (16)-(17); initial/late field and distribution amplitudes with the imaginary p = -iku velocity pole; two ordered wave-number samples with frequency, decrement, and ratio growth; and separate derivative-jump, initial-data-pole, and moving-pole values. The non-implications therefore remain physical after identifiers are renamed.
| Available fact | Conclusion not supplied | Lean witness |
|---|---|---|
| Named operational-transform output | The displayed equations (6)–(10) | named_operational_transform_output_does_not_supply_equations_six_through_ten |
| Named imported-frequency and local-decrement calculations | The displayed equation-(16) and equation-(17) values | named_long_wave_calculations_do_not_supply_equations_sixteen_and_seventeen |
| Collective electric-field damping | Damping of the velocity-resolved distribution | collective_field_damping_does_not_entail_distribution_damping |
| Growing short-wave frequency, decrement, and relative ratio | Decrement dominance at the selected scale | short_wave_growth_does_not_supply_decrement_dominance |
| Field damping for smooth data | Field damping for derivative-discontinuous data | smooth_data_damping_does_not_generalize_to_nonsmooth_data |
| Nonsmooth-data sensitivity analysis | The moving-pole velocity-distribution result | nonsmooth_data_analysis_does_not_supply_moving_velocity_pole |
| Unique forward evolution | Past-supported initial-data response | unique_forward_evolution_does_not_establish_retarded_response |
| Existence of one forward continuation | Forward determinism | forward_existence_does_not_establish_determinism |
| Existence of an admissible resonant contour | Selection of a unique contour without prescription | resonant_integral_without_prescription_does_not_select_unique_contour |
Five epistemic-status audits
long_wave_result_retains_imported_frequency and long_wave_result_retains_controlled_approximation preserve both qualifications of the long-wave result. causal_result_retains_deformation_argument keeps contour selection visible. penetration_result_retains_deferred_numerical_evaluation preserves the unclosed general integral. complete_result_retains_imported_approximate_deformation_and_deferred_scope proves that the final paper result still depends on all four status classes.
Direct scope extraction
long_wave_result_retains_imported_frequency_and_local_decrement returns the reused Vlasov input, the omitted frequency derivation, and the locally calculated decrement. long_wave_result_retains_equations_sixteen_and_seventeen returns the two value-level p. 28 formulas while preserving that split. short_wave_result_retains_ordered_asymptotic_regime returns decrement dominance and both wave-number ratios. external_penetration_result_retains_deferred_general_evaluation returns the full numerical-scope proposition from the penetration conclusion.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify source structure. routes_have_exact_predecessor_graph, calculation_contracts_are_independent_hypotheses, operational_formula_claim_depends_on_laplace_calculation, local_setups_imports_and_scope_are_independent_hypotheses, result_steps_apply_selected_inputs_and_contracts, and dependent_routes_consume_certified_predecessor_outputs certify the dependency boundary. every_source_claim_has_semantics covers all twenty-eight claims, and route_semantic_realization_is_exhaustive covers all ten routes. Transform, contour, pole, asymptotic, and boundary calculations remain explicit theorem parameters.
Lean-encoded bibliographic record
L. Landau, On the Vibrations of the Electronic Plasma, Journal of Physics (USSR) 10 (1946), 25–34.
TraceComplete Lean semantic identifier ledger
Reading note. The article above is the human exposition. This collapsed cross-reference records every public theorem and every constructor of the five paper-local source-map vocabularies. It introduces no additional claim; its purpose is to make semantic omissions mechanically detectable.
Primary semantic theorems (237)
fourier_electric_field_is_negative_spatial_derivativelongitudinal_resolvent_has_residuecharge_density_coupling_positiveplasma_scales_positiveplasma_frequency_squareddebye_length_squaredplasma_frequency_times_debye_lengthphysical_domain_retains_equilibriumsource_equation_four_is_the_actual_spatial_fourier_equationsource_equilibrium_is_neutralized_by_the_fixed_ion_chargesource_equation_five_is_the_actual_spatial_poisson_equationnormalized_equilibrium_is_product_gaussiannormalized_maxwellian_control_realizes_source_equationsnormalized_maxwellian_initial_marginal_is_entireentire_extension_needs_actual_initial_valuesnormalized_plasma_frequency_squaredpositive_scale_labels_do_not_calibrate_the_maxwellianlong_frequency_tends_to_plasma_frequencylong_wave_suppression_gives_small_relative_dampingfrequency_comparison_cutoff_is_positive_and_controls_correctionlong_frequency_strictly_exceeds_leadinglong_wave_frequency_estimates_realize_controlled_approximationcontrolled_frequency_comparison_has_a_matched_predictioncontrolled_frequency_comparison_is_not_exact_agreementshort_wave_rates_positiveshort_frequency_over_wave_numbershort_decrement_over_wave_numbershort_frequency_over_decrementshort_decrement_over_frequency_logarithmshort_wave_auxiliary_limits_give_observable_hierarchyevery_odd_phase_satisfies_the_complex_congruenceprincipal_phase_has_first_phase_ratioprincipal_phase_satisfies_the_congruenceshort_branch_has_odd_phase_ratioevery_short_wave_branch_satisfies_phase_congruenceprincipal_phase_excludes_every_higher_odd_branchshort_frequency_has_principal_phaseodd_branch_dominance_iff_auxiliary_largeconstructed_wave_number_retains_the_modulus_equationconstructed_wave_number_lies_above_debye_thresholdextrapolated_long_decrement_tends_to_zeroextrapolated_small_relative_rate_does_not_select_the_long_wave_limitcoarse_short_wave_point_does_not_have_decrement_dominancephysical_higher_phase_does_not_select_the_principal_branchphysical_frequency_approximation_does_not_give_exact_agreementunbounded_rate_growth_does_not_give_eventual_decrement_dominancesmall_extrapolated_relative_damping_does_not_select_long_wavelengthsexponential_envelope_tends_to_zeroexponential_envelope_const_muldamped_mode_normdamped_mode_has_envelopeexponential_envelope_addestimated_mode_error_yields_envelopedamped_mode_logarithmic_decay_rateslower_mode_has_no_faster_envelopearbitrarily_close_decay_rates_do_not_supply_an_exact_envelopeasymptotic_phase_norm_tends_to_coefficientnonzero_asymptotic_coefficient_prevents_decayzero_asymptotic_coefficient_gives_decayzero_frequency_leading_phase_is_constantzero_disturbance_numerator_vanisheszero_disturbance_retains_the_physical_candidatezero_disturbance_has_zero_residuezero_disturbance_marginal_decaysdenominator_zero_does_not_establish_an_uncancelled_residuedenominator_zero_does_not_establish_marginal_nondecaylaplace_integrability_depends_only_on_the_futureactual_laplace_values_depend_only_on_the_futureconstant_amplitudes_preserve_laplace_integrabilityactual_laplace_values_respect_constant_amplitudesballistic_integrand_is_a_single_exponentialballistic_laplace_exists_on_the_rightballistic_laplace_is_the_actual_resolventinverse_resolvent_decomposes_on_the_vertical_linethe_odd_vertical_part_cancelsthe_constant_signal_bromwich_cut_at_zerothe_constant_signal_bromwich_endpoint_is_halfthe_endpoint_limit_is_not_the_initial_valuethe_continued_resolvent_is_not_a_left_half_plane_time_integralthe_vertical_inverse_integrand_is_not_absolutely_integrablethe_constant_signal_has_genuine_finite_contour_integralsthe_reciprocal_continuation_is_analytic_at_minus_onea_totalized_integral_value_is_not_an_analytic_continuationfuture_support_does_not_identify_the_actual_laplace_integralactual_time_integration_uses_only_future_coordinatesthe_actual_truncated_inverse_contour_is_verticalthe_kinetic_denominator_cannot_vanish_in_the_right_half_planeintegration_by_parts_and_the_kinetic_equation_yield_equation_eightequation_eight_has_an_actual_integrable_velocity_averagethe_dielectric_coefficient_is_the_poisson_kinetic_productequation_eight_and_poisson_yield_equation_nineequation_nine_and_transverse_reduction_yield_equation_tenlower_operational_inputs_derive_equations_six_through_tenequation_six_is_the_physical_one_sided_time_integralnamed_operational_transform_output_does_not_supply_equations_six_through_tenequal_transforms_on_the_contour_give_equal_inverse_approximationsa_common_inverse_contour_determines_the_positive_time_valuesame_initial_problem_has_the_same_kinetic_denominatorsame_initial_problem_has_the_same_potential_dataequation_nine_determines_the_potential_on_its_nonzero_domainequation_eight_determines_the_distribution_after_the_potentialthe_source_inverse_formula_determines_the_actual_future_distributionthe_actual_poisson_equation_uniquely_fixes_the_potentialthe_source_initial_problem_determines_its_poisson_potentialthe_source_initial_problem_determines_its_fourier_electric_fieldsource_reconstruction_and_poisson_closure_determine_the_physical_fieldthe_same_initial_problem_is_reflexivethe_explicit_initial_datum_recovers_the_zero_time_modethe_same_initial_problem_has_the_same_initial_modesource_reconstruction_determines_the_actual_mode_statean_actual_admissible_readout_supplies_forward_mode_existencethe_source_reconstruction_derives_selected_mode_determinismactual_source_inputs_establish_nonvacuous_unique_mode_evolutionan_admissible_mode_evolution_retains_both_defined_charge_densitiesthe_decaying_laplace_integrand_is_the_actual_exponentialthe_decaying_signal_has_its_actual_laplace_domainthe_decaying_signal_has_its_actual_resolventthe_actual_decaying_signal_is_smoothboth_actual_signals_are_smooththe_second_signal_is_a_real_positive_polynomial_of_the_decayboth_signals_are_real_and_strictly_positiveboth_signals_have_the_same_nonzero_initial_valuethe_second_signal_has_an_actual_laplace_integralboth_actual_laplace_samples_are_one_halfthe_positive_time_histories_have_different_computed_valuesone_laplace_sample_and_the_initial_value_do_not_determine_the_historythe_initial_comparison_uses_an_actual_normalized_maxwellianthe_computed_density_amplitude_is_small_and_positivethe_gaussian_mode_has_its_actual_charge_densityboth_comparison_modes_obey_the_actual_initial_poisson_equationthe_real_profiles_reconstruct_the_actual_two_mode_coefficientsthe_actual_potential_gradient_is_the_negative_electric_fieldthe_actual_field_gradient_is_the_two_mode_charge_profilethe_complete_distribution_has_its_actual_density_integralthe_small_two_mode_perturbation_keeps_the_full_distribution_nonnegativethe_real_initial_profiles_obey_poisson_with_the_actual_density_momentthe_constructed_initial_profiles_have_physical_positive_density_and_poisson_closurethe_extra_mode_changes_the_actual_field_at_a_computed_positionone_selected_fourier_mode_does_not_determine_the_complete_physical_fieldevery_constant_potential_satisfies_the_actual_zero_wave_poisson_equationzero_wave_poisson_does_not_fix_the_constant_potential_but_the_fields_agreecartesian_coverage_recovers_the_actual_velocity_integralfuture_operational_signal_is_the_selected_kinetic_distributionthe_initial_mode_distribution_is_the_actual_cartesian_initial_datumthe_operational_mode_distribution_is_the_actual_cartesian_time_slicethe_source_initial_slice_has_an_integrable_mode_densitythe_source_time_slice_has_an_integrable_mode_densitythe_source_kinetic_solution_supplies_time_domain_poisson_closurethe_reconstructed_mode_potential_is_the_actual_kinetic_potentialthe_reconstructed_mode_field_is_the_actual_selected_fieldthe_source_data_realize_the_actual_selected_mode_evolutionthe_source_data_derive_unique_selected_mode_evolutionone_sided_initial_value_kernel_realizes_retarded_fieldcollisionless_initial_value_setup_retains_actual_kinetic_and_poisson_equationscollisionless_landau_initial_value_setup_realizes_nonvacuous_kinetic_poissondivergent_normal_mode_integral_does_not_solve_arbitrary_initial_datatransform_formula_result_retains_equations_six_through_tenlower_transform_calculation_derives_the_formula_resultlaplace_formulas_establish_nonvacuous_deterministic_evolutionlaplace_solution_realizes_retarded_initial_value_fieldlaplace_solution_realizes_nonvacuous_unique_forward_evolutioninitial_value_result_retains_the_actual_selected_mode_and_fieldinitial_value_result_identifies_every_admissible_selected_modelaplace_calculation_retains_equations_six_through_tenlandau_initial_value_inputs_realize_source_structural_kinetic_poisson_explanationsource_structural_landau_plasma_explanation_retains_printed_operational_formulasentire_initial_data_and_deformed_contour_determine_late_time_poleanalytic_result_retains_an_entire_extension_of_the_actual_marginalleft_half_plane_pole_yields_collective_field_dampingcollective_damping_retains_actual_fourier_electric_field_limitcollective_damping_retains_actual_spatial_electric_field_limitcalibrated_plasma_scales_retain_source_valueswavelength_error_control_yields_actual_field_envelopelong_wavelength_limit_combines_imported_frequency_and_landau_decrementequation_nineteen_and_principal_phase_yield_equation_twentyseparate_short_wavelength_analysis_yields_growing_damping_ratioshort_wave_result_retains_parameter_limitsshort_wave_result_retains_ordered_asymptotic_regimeshort_wave_result_retains_equations_nineteen_and_twentyshort_wave_result_retains_physical_decrement_dominancepointwise_short_wave_dominance_iff_auxiliary_largeinitial_regularity_controls_collective_field_damping_scopemoving_velocity_pole_yields_undamped_velocity_resolved_distributionvelocity_pole_result_retains_actual_marginal_nondecayvelocity_pole_result_retains_actual_nonzero_residuenonzero_velocity_frequency_yields_asymptotic_oscillationregularity_sensitivity_and_velocity_pole_results_remain_independentcollective_field_damping_coexists_with_undamped_velocity_distributionlandau_collisionless_kinetic_poisson_preserves_collective_distribution_separationnegative_dielectric_response_places_frequency_below_plasma_frequencypositive_dielectric_response_places_frequency_above_plasma_frequencypositive_dielectric_spatial_decrement_is_strictly_positivenegative_dielectric_approximation_has_zero_wall_fieldpositive_dielectric_approximation_has_zero_wall_fieldhalf_space_setup_retains_equations_twenty_four_through_twenty_sixpositive_imaginary_frequency_prescription_selects_half_space_solutioncausal_half_space_result_retains_source_fourier_and_contour_formulasspatial_asymptotics_retain_distinct_resonance_branches_and_numerical_scopepenetration_result_retains_source_boundary_and_asymptotic_formulaspenetration_result_separates_sub_and_super_plasma_frequency_branchesnear_resonance_approximations_do_not_satisfy_exact_wall_boundarypaper_routes_establish_scoped_collisionless_damping_and_penetrationcomplete_result_retains_short_wave_equations_and_dominancecomplete_result_retains_half_space_boundary_and_penetration_formulaslong_wave_result_retains_imported_frequency_and_local_decrementlong_wave_result_retains_equations_sixteen_and_seventeenlong_wave_result_retains_actual_parameter_familyshort_wave_result_retains_actual_parameter_familylong_wave_result_retains_maxwellian_scale_calibrationshort_wave_result_retains_maxwellian_scale_calibrationhalf_space_source_retains_maxwellian_scale_calibrationexternal_penetration_result_retains_deferred_general_evaluationsource_half_space_dielectric_branches_are_nonvacuously_realizeddielectric_signs_do_not_supply_frequency_response_formulasdielectric_response_does_not_supply_bulk_field_boundarydielectric_response_does_not_supply_zero_mode_kernel_identitya_single_contour_choice_does_not_supply_sign_dependent_bypassnamed_far_attenuation_does_not_supply_two_thirds_exponentpositive_spatial_damping_does_not_supply_resonance_oscillationnear_resonance_profile_values_are_not_the_exact_wall_boundarynamed_long_wave_calculations_do_not_supply_equations_sixteen_and_seventeendominant_short_wave_damping_does_not_supply_equations_nineteen_and_twentycollective_field_damping_does_not_entail_distribution_dampingshort_wave_growth_does_not_supply_decrement_dominancesmooth_data_damping_does_not_generalize_to_nonsmooth_datanonsmooth_data_analysis_does_not_supply_moving_velocity_poleunique_forward_evolution_does_not_establish_retarded_responseforward_existence_does_not_establish_determinismresonant_integral_without_prescription_does_not_select_unique_contourcauchy_density_has_actual_derivativecauchy_slope_has_derivative_at_zerocauchy_slope_is_integrableactual_first_order_equation_holdsselected_perturbation_is_regularfinite_amplitude_density_stays_positive_and_integrablefinite_amplitude_nonlinear_residual_is_nonzeropositive_integrable_first_order_solution_is_not_an_exact_nonlinear_solution
Coverage theorems (27)
collisionless_setup_atom_retains_actual_kinetic_and_poisson_equationsevery_source_claim_has_semanticsnormal_mode_insufficiency_route_is_semantically_realizedinitial_value_solution_route_is_semantically_realizedsource_inputs_expose_equations_six_through_tensource_inputs_derive_the_transformed_distribution_quotientsource_inputs_derive_the_transformed_potential_quotientinitial_value_atom_retains_the_actual_selected_mode_and_fieldinitial_value_atom_identifies_every_admissible_selected_modeshort_wave_result_atom_retains_equations_nineteen_and_twentycomplete_result_atom_retains_short_wave_equations_and_dominancehalf_space_setup_atom_retains_equations_twenty_four_through_twenty_sixcausal_half_space_atom_retains_source_fourier_and_contour_formulaspenetration_atom_retains_equations_forty_four_through_forty_sixpenetration_atom_separates_sub_and_super_plasma_frequency_branchespenetration_atom_rejects_approximate_profiles_as_exact_wall_fieldscomplete_result_atom_retains_half_space_source_formula_chainanalytic_continuation_route_is_semantically_realizedcollective_field_damping_route_is_semantically_realizedlong_wavelength_route_is_semantically_realizedshort_wavelength_route_is_semantically_realizedregularity_and_distribution_route_is_semantically_realizedcausal_half_space_route_is_semantically_realizedpenetration_asymptotics_route_is_semantically_realizedcomplete_assessment_route_is_semantically_realizedall_routes_are_semantically_realizableroute_semantic_realization_is_exhaustive
Source-map audit theorems (14)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphcalculation_contracts_are_independent_hypothesesoperational_formula_claim_depends_on_laplace_calculationlocal_setups_imports_and_scope_are_independent_hypothesesresult_steps_apply_selected_inputs_and_contractsdependent_routes_consume_certified_predecessor_outputslong_wave_result_retains_imported_frequencylong_wave_result_retains_controlled_approximationcausal_result_retains_deformation_argumentpenetration_result_retains_deferred_numerical_evaluationcomplete_result_retains_imported_approximate_deformation_and_deferred_scope
Semantic atoms (28)
collisionlessSetupnormalModeAssessmentnormalModeResultlaplaceCalculationoperationalTransformFormulainitialValueResultentireDatumSetupanalyticContinuationCalculationanalyticContinuationResultfieldDampingCalculationfieldDampingResultlongWaveSetupreusedVlasovFrequencylongWaveCalculationlongWaveResultshortWaveSetupshortWaveCalculationshortWaveResultregularityDistributionCalculationregularityDistributionResultfieldDistributionSeparationhalfSpaceSetupcausalHalfSpaceCalculationcausalHalfSpaceResultpenetrationCalculationgeneralNumericalScopeexternalPenetrationResultcompletePaperResult
Claim identifiers (28)
collisionlessSetupnormalAssessmentnormalResultlaplaceCalculationoperationalFormulainitialResultentireDatumanalyticCalculationanalyticResultdampingCalculationdampingResultlongSetupvlasovFrequencylongCalculationlongResultshortSetupshortCalculationshortResultregularityCalculationregularityResultseparationResulthalfSpaceSetupcausalCalculationcausalResultpenetrationCalculationnumericalScopepenetrationResultcompleteResult
Step identifiers (28)
stateCollisionlessSetupassessNormalModesderiveNormalResultsupplyLaplaceCalculationretainOperationalFormuladeriveInitialResultstateEntireDatumsupplyAnalyticCalculationderiveAnalyticResultsupplyDampingCalculationderiveDampingResultstateLongWaveSetupimportVlasovFrequencysupplyLongWaveCalculationderiveLongWaveResultstateShortWaveSetupsupplyShortWaveCalculationderiveShortWaveResultsupplyRegularityCalculationderiveRegularityResultderiveFieldDistributionSeparationstateHalfSpaceSetupsupplyCausalCalculationderiveCausalResultsupplyPenetrationCalculationretainGeneralNumericalScopederivePenetrationResultassembleCompleteResult
Route identifiers (10)
normalModeInsufficiencyinitialValueSolutionanalyticContinuationcollectiveFieldDampinglongWavelengthshortWavelengthregularityAndDistributioncausalHalfSpacepenetrationAsymptoticscompleteAssessment
Route kinds (10)
collisionlessNormalModeCritiquelaplaceInitialValueEvolutioncomplexContourDeformationcollectivePoleDampingimportedFrequencyLongWaveApproximationshortWaveAsymptoticsregularityAndDynamicalLevelSeparationcausalBoundaryPrescriptionspatialPenetrationAsymptoticscompleteScopedAssessment
Checked source-route details
This ledger is generated from the elaborated Lean route records. It lists direct predecessors, ordered inference steps, and exported claims. The independent fidelity audit checks every field; this ledger does not replace the physical semantics or certify every explanatory diagram.
normalModeInsufficiency
Logical kind: collisionlessNormalModeCritique.
Required predecessor routes: none.
Ordered inference steps: stateCollisionlessSetup, assessNormalModes, deriveNormalResult.
Exported conclusions: normalResult.
initialValueSolution
Logical kind: laplaceInitialValueEvolution.
Required predecessor routes: normalModeInsufficiency.
Ordered inference steps: supplyLaplaceCalculation, retainOperationalFormula, deriveInitialResult.
Exported conclusions: operationalFormula, initialResult.
analyticContinuation
Logical kind: complexContourDeformation.
Required predecessor routes: initialValueSolution.
Ordered inference steps: stateEntireDatum, supplyAnalyticCalculation, deriveAnalyticResult.
Exported conclusions: analyticResult.
collectiveFieldDamping
Logical kind: collectivePoleDamping.
Required predecessor routes: analyticContinuation.
Ordered inference steps: supplyDampingCalculation, deriveDampingResult.
Exported conclusions: dampingResult.
longWavelength
Logical kind: importedFrequencyLongWaveApproximation.
Required predecessor routes: collectiveFieldDamping.
Ordered inference steps: stateLongWaveSetup, importVlasovFrequency, supplyLongWaveCalculation, deriveLongWaveResult.
Exported conclusions: longResult.
shortWavelength
Logical kind: shortWaveAsymptotics.
Required predecessor routes: collectiveFieldDamping.
Ordered inference steps: stateShortWaveSetup, supplyShortWaveCalculation, deriveShortWaveResult.
Exported conclusions: shortResult.
regularityAndDistribution
Logical kind: regularityAndDynamicalLevelSeparation.
Required predecessor routes: collectiveFieldDamping, initialValueSolution.
Ordered inference steps: supplyRegularityCalculation, deriveRegularityResult, deriveFieldDistributionSeparation.
Exported conclusions: regularityResult, separationResult.
causalHalfSpace
Logical kind: causalBoundaryPrescription.
Required predecessor routes: none.
Ordered inference steps: stateHalfSpaceSetup, supplyCausalCalculation, deriveCausalResult.
Exported conclusions: causalResult.
penetrationAsymptotics
Logical kind: spatialPenetrationAsymptotics.
Required predecessor routes: causalHalfSpace.
Ordered inference steps: supplyPenetrationCalculation, retainGeneralNumericalScope, derivePenetrationResult.
Exported conclusions: penetrationResult, numericalScope.
completeAssessment
Logical kind: completeScopedAssessment.
Required predecessor routes: normalModeInsufficiency, initialValueSolution, analyticContinuation, collectiveFieldDamping, longWavelength, shortWavelength, regularityAndDistribution, causalHalfSpace, penetrationAsymptotics.
Ordered inference steps: assembleCompleteResult.
Exported conclusions: completeResult.