Formal reconstruction · anomalous self-consistency, nonperturbative quasiparticle gap, gauge-phase family, matched electromagnetic vertex, Ward identity, conserving current, gauge-invariant Meissner response, collective pair spectrum, nonlocal charge cloud, Coulomb plasma conversion, and open approximation boundaries
Quasi-Particles and Gauge Invariance in the Theory of Superconductivity
How a conserving vertex repairs longitudinal gauge response while preserving transverse screening—and how the same collective structure organizes zero modes, charge dressing, and the plasma shift
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- structureProof-free ordinary broken-phase structure used in the shared Goldstone explanation. The gapless-mode and spectral-membership relations are excluded because they belong to the explained phenomenon rather than the constraining structure. Paper-local provenance is also excluded from this ordinary physical constraint.
- structureSource-sensitive refinement of the ordinary broken-phase constraint. It adds one typed paper-local derivation and a proposition-valued realization relation without making provenance part of ordinary physical explanation.
- structureThe selected mode-conversion calculation is proof-free. It retains its physical indices and every proposition-valued relation family used by the shared Goldstone-spectrum and conversion routes, but no proof that either route applies or that the model represents a physical system.
- inductiveOnly claims in the shared Goldstone-originated mode-conversion route transfer. Paper-local response equations, polarization functions, gap calculations, and relativistic interpretations are not constructors.
- structure
- structurePaper-local meanings for the selected conversion calculation, the theory using it, and the physical world it represents.
- structureThe containing theory is distinct from the selected calculation.
- structureThe represented physical world is distinct from model and theory.
- structureThe selected spectral calculation is proof-free data. It retains both its physical indices and the exact proposition-valued relations used to state spontaneous breaking, gaplessness, and spectral membership.
- inductiveOnly the shared broken-phase spectral claims transfer. Mode conversion, finite-frequency generation, gauge-field dynamics, and gap calculations are not constructors.
- structure
- structurePaper-local meanings for the selected spectral calculation, its containing theory, and the physical system or spectrum it represents.
- structureThe theory using the spectral calculation is distinct from it.
- structureThe represented physical system is distinct from model and theory.
- structureBulk exclusion of the selected field from the selected system.
- structure
- structure
- structure
- structure
- structure
- structure
- structureThe calculated induced-current response to the selected transverse field.
- structureThe spectrum-scoped gapless-mode phenomenon explained by the selected broken phase. This record retains the relations needed to distinguish gaplessness from mere membership in a named spectrum.
- structureThe five selected physical indices constrained by one complete self-consistency-to-gap route. This proof-free type contains no validity, solution, spectral-membership, finiteness, or spectrum-gap proposition.
- inductiveEvery proposition retained by the shared calculation route.
- structureThe repeated paper vocabulary together with the five selected physical indices. A paper adapter fixes these indices before any shared route can be applied.
- structurePaper-local meanings for theory use, world representation, and claims.
- structureProof-free semantics selected from one self-consistent spectral-gap calculation. Every field is data, a value, or a proposition-valued relation; none supplies a setup proof, calculation, bridge, or desired conclusion.
- structureThe nontrivial solution and finite selected-spectrum gap obtained by the route. Keeping this type distinct from the constraint prevents a value named as a gap from explaining itself.
- structureProof-free source constraint for one paper-local self-consistent gap derivation. It retains the exact selected model, a typed derivation token, and its proposition-valued realization relation, but neither a proof that the derivation obtains nor a spectral-gap output.
- structure
- structure
- structureOne fixed spatial direction and probe, with an actual radial wave-number family. The positive-side limit never substitutes the value at zero momentum.
- structureThe static linear-response organization in which screening is calculated.
- inductive
- structureThe repeated response vocabulary. The microscopic meaning of each predicate is supplied by a paper adapter.
- structure
- structurePaper-local interpretation of the selected response model. Theory use, world representation, and transferred claims are explicit propositions.
- structureProof-free semantics selected from one transverse-screening calculation. No field stores a setup proof, calculation, interpretation, or conclusion.
- structure
- structure
- structureThe selected superconducting system, current channel, and applied field.
- 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
- inductiveThe source-specific join from anomalous gap to gauge-restored response.
- inductiveThe paper-local theory role for the anomalous self-energy gap model.
- inductiveNambu's source-specific join from the neutral pair to the plasma pole.
- inductiveTheory role for the gauge-restored transverse response calculation.
- inductiveNambu's paper-local source of the collective-mode conversion.
- inductiveNambu's anomalous-self-energy route to the selected quasiparticle gap.
- inductiveNambu's source route from the anomalous gap to gauge-restored screening.
- structure
- structureFinite tensors realizing the outputs of the section-5 calculation. No value represents an unregulated divergent integral.
- structurePaper-local physical objects and predicates. The uncoupled collective spectrum is kept distinct from the Coulomb-coupled plasma spectrum, and a gauge-dependent representative is kept distinct from gauge-independent physical response.
- structureA finite readout of the Coulomb-omitted collective dispersion (6.11) and the Coulomb-coupled plasma frequency (8.11). It keeps the two mode frequencies separate.
- structureA finite readout of the selected values in equation (2.15). It is deliberately smaller than `SuperconductivityFramework`: the countermodel tests whether a named gapped-spectrum output alone retains the printed square-root and twice-pairing-scale equations.
- structureA finite readout of the matrix Ward relation (4.4b) and longitudinal cancellation (5.9). Quasiparticle matrices are two-by-two; the spatial response matrices are three-by-three and act on an actual wavevector.
- structureThe renormalized reference is distinct from the residual vertex correction.
- structure
- structure
- structure
- structure
- structureLaw symmetry and admissible state action, without interpretation, vacuum selection, or variational claims.
- structureA law-specific selected family adds no physical or descriptive classification of its representative action.
- structure
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA source-sensitive explanation of the selected mode conversion.
- definitionThe direct physical content of the stronger Goldstone-originated route. The generic conversion remains visible, but it is paired with the direct nonvacuous child spectrum: a continuous exact symmetry moves two distinct states in the selected phase and a concrete gapless mode belongs to the uncoupled spectrum. Keeping that child prevents a completed conversion from retroactively manufacturing a spontaneous-breaking origin.
- definitionThe direct physical content of a generic two-spectrum mode conversion. The selected original mode and finite-frequency converted mode are distinct, as are the uncoupled and interacting spectra, and every setup and final-state relation is active. This endpoint deliberately does not assert a broken-symmetry origin: a paper may establish this conversion pattern without first earning a Goldstone-spectrum route.
- definitionThe selected original mode is gapless in the uncoupled spectrum.
- definitionThe selected calculation produces the complete final-spectrum change.
- definitionEvery setup relation used by the selected conversion is active.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected coupling activity together with one paper-local derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe uncoupled part of the conversion model as a spectrum calculation.
- definition
- definition
- definition
- definition
- definitionThe output-led stronger result retains exact selection for both the composed conversion model and its uncoupled-spectrum child, together with the direct nonvacuous Goldstone-originated conversion endpoint. The implication-valued routes are reconstructed from these facts rather than stored here.
- definition
- definitionThe stronger route used by Anderson and Nambu. The uncoupled spectrum must first be established as a broken-symmetry Goldstone spectrum, and the selected mode-conversion route must then be independently applicable to a particular gapless mode in that spectrum.
- definition
- definition
- definition
- definitionThe proof-free model is exactly the context-owned selected model. A candidate cannot choose its own symmetry, phase, modes, spectra, interaction, or system.
- definition
- definitionThe exactly selected conversion model together with the physical setup used by its conversion calculation. This proposition contains no calculation, route, converted-mode output, or Goldstone-origin claim.
- definitionA source-sensitive Goldstone-originated conversion retains the exactly selected conversion model and its exactly selected uncoupled-spectrum child, an inhabited broken-symmetry/two-spectrum endpoint, separately sourced Goldstone and conversion explanations, and an additional paper-local joining derivation. Agreement on a finite-frequency endpoint cannot identify Nambu's Coulomb-resummed pair calculation with Anderson's conductor response and superconducting gauge-field argument.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionBuild the proof-free selected calculation while retaining every relation family used by the shared Goldstone-originated conversion route.
- definition
- definition
- definition
- definitionThe unique conversion model fixed by the context's eight selected physical indices and eleven retained relation families.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected broken phase is nonvacuous when it exhibits two distinct states related by the selected continuous exact symmetry and a concrete gapless mode belonging to the selected spectrum.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe ordinary proof-free broken-phase constraint selected by this model.
- definitionThe source-sensitive broken-phase constraint selected by this model.
- definitionThe exact spectrum-scoped gapless phenomenon selected by this model.
- definition
- definition
- definition
- definition
- definitionThe retained breaking relations, reconstructed without adding proofs.
- definition
- definition
- definition
- definitionSource-sensitive explanation by one typed paper-local derivation.
- definitionOrdinary structural explanation of the selected scoped gapless mode.
- definition
- definition
- definition
- definitionThe proof-free model is exactly the context-induced model at its own selected symmetry, phase, and spectrum. Whole-model equality keeps every retained relation family in the certificate when the structure evolves.
- definition
- definition
- definition
- definition
- definition
- definitionThe unique symmetry, phase, and spectrum model selected by the context.
- definition
- definition
- definition
- definitionSource-sensitive structural semantics for one typed paper-local derivation. The source constraint wraps the ordinary constraint and requires its route plus a realized derivation token.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 imported or deferred calculation producing a nontrivial solution.
- definitionThe complete selected self-consistency route structurally explains the nontrivial finite gap in its selected excitation spectrum.
- definition
- definitionExact selected semantics together with the inhabited pre-calculation setup.
- definitionSource-sensitive explanation by one typed paper-local gap derivation.
- definitionThe separate physical interpretation of the calculated solution.
- definition
- definition
- definitionThe exact proof-free model fixed by this context.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe complete inhabited gap route stated directly on all five selected indices and all six retained relation families. The self-consistency problem is posed, its selected gap is an actual nontrivial solution, and that same gap is finite and gaps a spectrum containing the selected excitation.
- definitionThe route's direct physical output, stated without setup or implication-valued calculation contracts.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionExact proof-free source constraint selected by a model and derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe conventional Fourier factor `i` is absorbed in the arbitrary complex gauge amplitude. This concerns external potentials, not vacuum representatives.
- definition
- definition
- definition
- definition
- definition
- definition
- 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 selected established self-consistent gap is admissible as an upstream input to one paper's transverse-response setup. The bridge receives the complete established gap route and every retained output separately. This permits BCS to use the excitation and gapped-spectrum content while Nambu uses the nonperturbative solution. The bridge remains paper-local because neither use follows from the shared meaning of a spectral gap.
- definition
- definitionThe physical interpretation of the calculated opposing current. This bridge is separate because an opposing-current relation is not definitionally bulk field exclusion.
- definitionThe paper-local response calculation. It must produce both an induced current and the long-wavelength screening sign; neither follows from merely selecting a transverse field.
- definitionDirect physical content of the composed gap-supported screening route. The generic transverse-screening endpoint remains gap-agnostic, since a different paper could earn that route without a self-consistent gap. The BCS and Nambu source-order routes are stronger: their exact established gap route, the direct nonvacuous gap content, the paper-local admissibility bridge, the selected response setup, and the direct screening endpoint must all hold together. Requiring the direct child endpoint prevents an implication-valued gap route from being remembered only in the theorem's ancestry.
- definitionThe actual gap-to-response calculation retains the selected quasiparticle spectrum and finite gap, the paper-local admissibility bridge, and the independently calculated transverse current, opposing sign, and bulk-field exclusion. A gapped quasiparticle spectrum is not identified with a gapless collective spectrum or with electromagnetic screening by itself.
- definitionThe selected model retains all six physical indices and all six semantic families exactly. This certificate supplies no setup, calculation, route, or physical conclusion.
- definitionCompleted gap-supported screening with all three historical sources.
- definitionThe gap explanation, screening mechanism, and their paper-local joining calculation have separately typed, independently realized derivations. Both exact selected models and the physical cross-framework handoff remain present in the conclusion.
- definition
- definition
- definitionCompatibility name retained for existing paper adapters and audits.
- definition
- definition
- definition
- definitionThe exact proof-free response model selected by this context.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe unique model fixed by the context's six selected physical objects.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe complete transverse-response route mechanistically explains screening.
- definition
- definitionThe model-native physical bridge from long-wavelength opposition to bulk field exclusion. The bridge is separate from the response calculation.
- definitionThe model-native current calculation. It stays implication-valued because a paper must still supply the calculation, while the direct endpoint below also requires the antecedent and both outputs.
- definitionDirect physical content of one completed transverse-screening calculation. This model-native endpoint drops exact record equality while retaining an actual setup and the calculated current, screening sign, and bulk field exclusion on one model. It stores neither the implication-valued calculation nor the field-exclusion bridge.
- definitionThe model-native response setup. It keeps the selected validity regime, static transverse field, and linear-response data together without requiring equality to a context-selected record.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected bulk field-exclusion phenomenon.
- definitionThe induced and long-wavelength-opposing current activity.
- definitionThe selected static transverse linear-response organization.
- definitionThe current-bearing component selected by the screening model.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionParameterized compatibility name used by generic route constructors.
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- definition
- definitionA finite response control, not a reconstruction of the microscopic loop integrals.
- definition
- definition
- definition
- definition
- definition
- definitionThe complete kernel is assembled, but the separate c-number term fails its Ward condition. The displayed (5.9) contraction is still satisfied.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAll selected printed formulas retained by Nambu's paper-local routes.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPhysical Review p. 662, equation (8.11): Coulomb polarization shifts the collective mode to the ordinary plasma frequency.
- definitionPhysical Review p. 658, equation (5.9): the contact part (1a) and corrected vertex response (2) have zero contraction with the finite spatial wavevector. The finite tensors represent the imported, consistently regulated output; this definition does not justify shifts of divergent loop integrals.
- definitionPhysical Review p. 656, equation (4.4b): the charge vertex is the noncommutative difference L(p') tau_3 - tau_3 L(p).
- definitionPhysical Review p. 659, equation (6.11): the Coulomb-omitted collective pair has a gapless linear dispersion.
- definitionPhysical Review p. 652, equation (2.15), together with the stated two-pairing-scale quasiparticle gap.
- definitionPhysical Review p. 652, equation (2.14): the selected self-energy has a diagonal chi tau_3 term and an off-diagonal phi tau_1 term, while the quasiparticle Hamiltonian uses the renormalized dispersion epsilon-prime = epsilon + chi.
- definitionPhysical Review p. 652, equation (2.16): the selected quasiparticle Green function has the Nambu numerator and the causal p_0^2 - E_p^2 + i epsilon denominator.
- definitionPhysical Review p. 653, equation (2.20): constant gauge phase rotates the two anomalous self-energy components through a circle.
- definitionLiteral central formulas retained by Nambu's paper-local routes.
- definitionThe p. 652 two-component matrix formulas retained by the gap setup.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe tensor calculation supplies the contraction and residual terms. Pure-gauge cancellation, gauge invariance, and the calibrated current limit are deductions from these outputs, not additional calculation premises.
- definition
- definitionExact raw premises realizing Nambu's typed selected-gap derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquations (5.7)-(5.10) retain the separate c-number term and the vanishing static polarization correction. Equation (5.9) alone is not the full kernel.
- definitionThe p. 658 correction is of order `g^2 N`, apart from renormalization. This is an eventual relative-order statement with an unspecified constant and threshold, not an error bar at the selected finite coupling.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 causal denominator in Physical Review p. 652, equation (2.16).
- definitionThe matrix numerator in Physical Review p. 652, equation (2.16).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionNambu's joining source retains the anomalous nonperturbative gap, gauge-phase family, matrix Ward identity, explicitly gauge-defective bare response, Coulomb-omitted gapless collective state, printed longitudinal cancellation, surviving transverse current, gauge-restored response, and field expulsion. It does not silently replace the neutral collective branch by the later Coulomb-shifted plasma spectrum.
- definitionNambu's joining source retains the matched matrix Ward identity, the Coulomb-omitted neutral acoustic pair and its printed equation (6.11), the later Coulomb pair process and polarization resummation, and the distinct plasma-frequency equation (8.11). Its weak-coupling, linear-field, and generalized-Hartree-Fock limitations remain explicit instead of being silently promoted to an exact all-orders mass-generation theorem.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 Pauli matrix tau_1 that carries Nambu's off-diagonal anomalous self-energy component in equation (2.14).
- definitionThe Pauli matrix tau_3 used in Nambu's two-component quasiparticle notation. Writing it explicitly keeps the Ward relation matrix-valued.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionInterpret the selected anomalous self-energy setup as a model used by Nambu's generalized Hartree-Fock quasiparticle theory and representing the superconductor. Model use retains the unsolved Hartree-Fock self-consistency setup. The nonperturbative solution remains model-level; only the repeated spectral claims transfer once separately established. Primary-source anchors: Physical Review pp. 652-653, especially equations (2.12)-(2.19), for the self-consistent anomalous solution, separation of the quasiparticle branches, and identification with the BCS energy-gap equation.
- definition
- definition
- definition
- definitionThe common transverse-screening view of Nambu's corrected response. The longitudinal Ward-identity repair remains a stronger paper-local route.
- definition
- definitionRetention means a positive transverse London limit plus the qualified weak-coupling comparison. It does not equate corrected and bare coefficients.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe zero-momentum pair calculation selected for explanation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionAn exact continuous symmetry moves one phase member to a distinct member of the same declared phase scope. Physical, descriptive, and gauge classifications remain outside this neutral proposition.
- definition
- definition
- definition
- definition
- definition
- definitionThe phase-relative vocabulary interpreted in the neutral philosophy layer. The adapter retains exact law symmetry, phase membership, and movement of a state. It contains no observable, variational, or physical-classification fields, so it neither affirms nor denies those additional claims.
- definitionAn exact law symmetry with an admissible state that is moved to a distinct admissible state in the same declared regime. This proposition deliberately does not classify the transformation as physical rather than descriptive or gauge-redundant.
- definitionA moved-state witness whose transformed endpoint remains physically admissible in the same declared regime. Bare movement is kept separately because an arbitrary relation can send a physical state outside the modeled state space or phase scope.
- definition
- definition
- definition
- definitionSelected-state movement still leaves physical versus descriptive or gauge classification, and the action laws, as independent obligations.
- definitionSelection specifies the relevant vacuum, equilibrium, or other physical state family for this law. It is not arbitrary kinematic admissibility and does not pick just one member of a degenerate family.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionA model-to-world interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definitionA model-to-theory interpretation law. It does not assert that the model has produced a conclusion; use `GroundedModelConclusionAt` for that.
- definition
- definition
- definition
- 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
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
- instance
- instance
- instance
- instance
Source mappings and interpretation choices
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- recursor
- definition
- 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
- 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
- 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
- definition
- definition
- 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
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- inductive
- definition
- instance
- definition
- 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
- definition
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- checked statement
- recursor
- definition
- definition
- constructor
- definition
- checked statement
- structure
- definition
- instance
- checked statement
- checked statement
- definition
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- checked statement
- recursor
- definition
- checked statement**Alias** of `PhysicsLogic.Papers.Nambu1960.SemanticContext.all_routes_are_semantically_realizable`.
- checked statement
- checked statement
- checked statement
- inductive
- definition
- instance
- 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
- 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
- definition
- definition
- 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
- 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
- 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
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- definition
- definition
- checked statement
- 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
- definition
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- 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 statementNamed gapless and plasma-mode outputs do not retain the distinct dispersion and plasma-frequency formulas that separate the two spectra.
- checked statementThe name of a finite quasiparticle gap does not retain Nambu's selected pairing scale, square-root spectrum, or twice-pairing-scale gap formula.
- checked statementNamed Ward and cancellation outputs can hold while the printed matrix Ward relation fails. In particular, a zero named vertex cannot silently replace the nonzero tau_3 commutator selected by (4.4b).
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementGround Nambu's anomalous self-energy model from the selected Hartree-Fock self-consistency setup and represented quasiparticle vacuum. This theorem does not use the nonperturbative gap calculation or the spectral interpretation.
- checked statementNambu's anomalous gap supports screening only after the matched Ward vertex, neutral collective intermediate, and longitudinal cancellation restore gauge invariance without erasing the physical transverse magnetic response.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe finite-momentum branch retains the printed equation (6.11).
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe Coulomb calculation retains Nambu's plasma-frequency equation.
- checked statement
- checked statement
- checked statementNambu's pre-conversion Coulomb setup realizes the exact selected shared setup without consuming polarization resummation or the plasma-mode calculation.
- checked statement
- checked statementThe Coulomb polarization calculation already realizes the generic two-spectrum conversion before its broken-phase Goldstone origin is added.
- checked statementNambu's Coulomb-polarization coupling and before/after spectra realize the shared mechanistic explanation independently of the stronger broken-phase origin route.
- checked statementJournal pp. 660-662: pair annihilation-creation and Coulomb polarization shift the gapless collective dispersion to the nonzero plasma energy, while the Coulomb-omitted calculation retains the original zero-energy branch.
- checked statement
- checked statement
- checked statement
- checked statementEquation (2.14) makes the anomalous pairing amplitude an actual off-diagonal entry of the selected self-energy matrix.
- checked statementEquations (2.14) and (2.15) together make the anomalous off-diagonal entry nonzero at the selected Fermi-surface momentum.
- checked statementThe established anomalous self-energy solution supplies the self-consistency equation and nonperturbative solution required by the Ward route. The paper-local vertex construction then establishes the Ward identity, continuity equation, and conserving current before the corrected Meissner response is admitted. Primary-source anchors: Physical Review pp. 652-658, especially equations (2.12)-(2.19), (3.10)-(3.12), and the discussion retaining the transverse BCS response after the collective vertex correction.
- checked statementNambu realizes the shared gap-to-response admissibility proposition through the matched Ward-identity calculation. The nonperturbative gap route alone does not provide the vertex construction or the transverse response setup.
- checked statement
- checked statementThe gap calculation retains the printed quasiparticle dispersion and gap.
- checked statement
- checked statementThe source-order Nambu route composes the established self-consistent gap, the conserving Ward-identity vertex, the corrected transverse-current calculation, and the field-expulsion interpretation.
- checked statement
- checked statementThe composed source-order route establishes the shared screening result while retaining the self-consistent anomalous gap and Ward calculation as explicit upstream dependencies.
- checked statement
- checked statement
- checked statementThe broken-phase setup retains Nambu's circular pairing-field family.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe homogeneous neutral pair, its finite-momentum acoustic dispersion, and the later Coulomb-resummed plasma pole form Nambu's specific composition; the matrix Ward identity and uncontrolled approximation extensions remain part of that source-local handoff.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe Meissner calculation retains the printed longitudinal cancellation.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementNambu's direct shared route uses the corrected static transverse response after the conserving vertex construction; it does not export the stronger longitudinal Ward-identity machinery into the shared component. Primary-source anchor: Nambu 1960, section 5, pp. 657-658, where the induced current is evaluated for a static external field and the collective correction is described as drastic longitudinally but small for the physical transverse magnetic response, leaving the BCS Meissner result essentially unaltered.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementNambu's complete source route retains both source-sensitive stages: anomalous self-energy explains the selected quasiparticle gap, while the Ward-vertex, collective-intermediate, and retained transverse-response route explains screening. The conjunction keeps those logically distinct derivations together without identifying the gapless collective spectrum with the gapped quasiparticle spectrum.
- checked statement
- checked statementNambu, Physical Review pp. 652-658: the nonperturbative anomalous self-energy supplies the gap equation, and the Ward-identity vertex plus collective intermediate state repairs the nonconserving bare longitudinal response. Section 5 then retains the corrected transverse BCS current and its Meissner screening interpretation. These source stages directly realize the shared mechanism without exporting Nambu's longitudinal vertex construction into the generic explanation and before any terminal shared screening endpoint exists.
- checked statement
- checked statementNambu's raw anomalous-self-energy premises realize a source-sensitive explanation distinct from BCS pairing. Ward-identity and collective-mode calculations are deliberately absent from this derivation token.
- checked statementNambu's anomalous self-energy solution and its separate split-quasiparticle interpretation realize the shared structural explanation. The direct route does not classify the separate collective ladder spectrum as gapped and does not identify anomalous self-energy with BCS's paired variational mechanism.
- checked statementThe anomalous nonperturbative solution and split quasiparticle branches on pp. 652-653 directly exhibit the inhabited shared gap at the same self-energy description, gap, selected quasiparticle spectrum, and regime. Nambu's separate ladder spectrum still contains a gapless collective mode.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe selected paper routes retain the central printed formulas without identifying the gapped quasiparticle spectrum with the gapless ladder mode or its Coulomb-shifted descendant.
- checked statementThe full selected route retains Nambu's two-component matrix structure together with the later gap, phase, Ward, response, dispersion, and plasma formulas.
- checked statement
- checked statement
- checked statement
- checked statementThe selected self-consistent setup retains the two-component self-energy, Hamiltonian, and Green-function formulas before a gap calculation is applied.
- checked statement
- checked 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 matched-vertex result retains Nambu's matrix Ward formula.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementJournal p. 658: the gauge-phase family and homogeneous pair solution jointly exhibit a nonvacuous broken phase and an in-spectrum zero mode.
- checked statement
- checked statementThe same journal route with its homogeneous zero-momentum pair derivation retained as source provenance.
- checked statementJournal p. 658: the gauge-phase family and homogeneous zero-momentum pair solution structurally explain the gapless collective mode in the ladder-pair spectrum. Coulomb polarization and the later finite plasma frequency remain in the separate mode-conversion route.
- checked statementGround the selected broken-phase pair-spectrum model through its physical-system representation without assuming the Ward identity or pair-mode 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
Constructors, projections, and other meaning dependencies
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- 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
- constructor
- constructor
- constructor
- constructor
- 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
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- constructor
- 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
- 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
Every statement below comes only from Nambu1960.lean, SourceMap.lean, and Coverage.lean. Equations (2.14), (2.15), (2.16), (2.20), (4.4b), (5.9), (6.11), and (8.11) are rendered from value-level Lean propositions using the explicit τ1/τ3 two-by-two complex matrices, a causal Green-function denominator, real square roots and trigonometric functions, and selected response and spectrum values. Each equation package is also a separate source-map claim whose retention step consumes the exact setup and calculation claims that carry it. The integral equations, response-kernel evaluations, polarization sums, and approximation estimates remain proposition-valued calculation inputs. The source graph keeps each implication-valued calculation or interpretation contract independent from the setup to which it is later applied. Ward, Meissner, zero-mode, dispersion, charge-cloud, and plasma setups expose their fresh local hypotheses as separate source claims before assembling them with inherited results. Coverage recovers every nontrivial step input from a checked ClaimsHold map; route certificates establish availability but do not supply semantic conclusions.
Three roots feed a gauge-restored response and several independent collective consequences
The self-consistent gap, gauge-phase family, and approximation boundary are independent roots. The gap feeds the Ward identity. Ward plus the phase family feed both the gauge-invariant Meissner route and the zero-momentum pair route. The latter then supports finite-momentum dispersion and Coulomb conversion; together with Ward it also supports the quasiparticle charge cloud. The source map declares gauge-invariant Meissner response—not a conjunction of every branch—as its formal main conclusion.
| Transition | Status | Retained boundary |
|---|---|---|
| Hartree–Fock self-consistency to anomalous gap | controlled approximation | The setup is generalized Hartree–Fock and weak coupling; the calculation is explicit. |
| Constant phase rotation to broken representation | paper derivation | The exact law symmetry moves the state; physical response invariance is proved later. |
| Self-energy equation to Ward identity | matched-vertex calculation | The gap alone does not supply the electromagnetic vertex construction. |
| Bare response to gauge-invariant screening | linear-response calculation | Collective longitudinal cancellation and a transverse interpretation bridge are required. |
| Zero mode to finite-momentum branch | controlled dispersion | Weak coupling and absence of Coulomb pair processes remain explicit. |
| Coulomb-omitted to Coulomb-coupled spectrum | polarization conversion | The two spectra are distinct before and after interaction. |
| Selected approximation to higher-order theory | open obligation | Higher fields, neglected terms, and beyond-Hartree–Fock corrections are not controlled. |
Self-consistency opens the quasiparticle gap, while constant phase rotations generate a family of representatives
Nonperturbative anomalous solution
The gap setup assumes the generalized Hartree–Fock approximation in the weak-coupling regime and a self-consistency equation for the anomalous self-energy generated by the phonon interaction. Before the supplied calculation is applied, the setup retains Nambu’s two-component matrix content: the self-energy has diagonal χ(p)τ3 and off-diagonal φ(p)τ1 pieces, the quasiparticle Hamiltonian uses ε′(p)τ3 + φ(p)τ1, and the Green function has the causal p02 − Ep2 + iε denominator. The supplied calculation then establishes anomalous pairing, a nonperturbative self-energy solution, failure of generation by any finite perturbation series, the associated gap equation, and satisfaction of that equation.
A separate physical interpretation bridge converts the solved gap equation into a finite energy gap and a gapped quasiparticle spectrum.
G(p,p0) = i[p0 + ε′(p)τ3 + φ(p)τ1] / [p02 − E(p)2 + iε],
E(p) = √[ξ(p)2 + φ(p)2], gap = 2|φ|,
with φ ≠ 0 and no finite perturbation-series construction of the anomalous solution. value-level equations (2.14)–(2.16) and twice-pairing-scale gap;
self_consistent_gap_setup_retains_equations_two_fourteen_and_sixteen · gap_calculation_retains_equation_two_fifteen; Physical Review pp. 652–653
(1)
equation_two_fourteen_retains_off_diagonal_pairing checks that the selected self-energy’s off-diagonal matrix entry is exactly φ(p), and equations_two_fourteen_and_two_fifteen_make_anomalous_entry_nonzero combines that with the positive selected Fermi-surface pairing scale. The source map associates the spectral separation with twice that scale and equation (2.19) with the BCS gap equation. The route retains these finite matrix and dispersion formulas while still leaving the self-consistent integral equation itself as an explicit calculation hypothesis.
Gauge-phase family
The second root selects a continuous constant-phase symmetry that is exact for the matter law. The quasiparticle vacuum belongs to the superconducting phase, and the symmetry moves it to a distinct but gauge-related vacuum. A separate representative premise states that both vacua represent the same selected superconductor.
with the vacuum moved within the superconducting phase. value-level equation (2.20);
gauge_phase_setup_retains_equation_two_twenty; p. 653
(2)
This does not yet say that a gauge-dependent response calculation is physical. Equality of the corrected response on both selected representatives is obtained only after response invariance is established downstream.
The electromagnetic vertex must be matched to the self-energy kernel
The Ward setup retains the self-consistency equation and nonperturbative self-energy solution. It then adds a vertex equation built from the same self-energy kernel, photon insertion at every charged line, and a vertex correction from the bare charge current to the corrected current.
⇒ exact Ward identity, corrected-current continuity, and quasiparticle charge conservation through the corrected current. value-level matrix equation (4.4b);
ward_result_retains_equation_four_four; Physical Review pp. 655–656
(3)
The theorem matched_vertex_equation_establishes_conserving_current exposes all three outputs. The route depends on the nonperturbative gap, but its vertex setup and calculation are additional inputs rather than consequences of the gap alone.
A collective intermediate state cancels the spurious longitudinal response without erasing transverse screening
The bare longitudinal response is explicitly not gauge invariant. The corrected setup therefore includes the Ward identity and conserving current, a zero-momentum collective intermediate state, the linear external-field approximation, and a static transverse vector potential.
The response calculation separates longitudinal and transverse effects. Equation (5.9) cancels the contact-plus-vertex tensor contraction. The separate c-number and static-polarization terms must also be controlled before the full pure-gauge current vanishes. The finite small-q calculation (5.11)-(5.13) identifies the collective contribution. Transverse retention is qualified by small corrections and renormalization, not exact equality.
(K_1a+K_2) q=0, K_1b q=0, K_pol=0 imply K q=0.
K q=0 is equivalent to K(A+chi*q)=K A for every complex A and chi. Equation (5.9) controls contact plus vertex only; (5.10) and the static polarization argument supply the remaining terms. The Fourier factor i is absorbed in chi. pp. 657-658. (4)
equation_five_nine_and_remaining_terms_cancel_the_actual_longitudinal_kernel · meissner_calculation_derives_response_outputs
K_eta(r) A -> -kappa(eta)*A as r->0+.
For some C>=0 and delta>0, if 0<eta<delta:
kappa_ref(eta)>0 and |kappa(eta)-kappa_ref(eta)|<=C*eta*|kappa_ref(eta)|. eta represents the weak-coupling order g^2 N; the reference retains renormalization. This is not exact equality or a numerical error bar at the selected finite coupling. p. 658. (4a)
meissner_calculation_exhibits_actual_transverse_london_limit · retained_transverse_response_has_a_qualified_correction_order
K=diag(-(1+eta),-(1+eta),0): at eta=1/10, stiffness=11/10, not 1.
Adding an unchecked I3 to K_1b or K_pol preserves (5.9) but breaks full gauge invariance.
H=[[0,0,1],[0,0,0],[1,0,0]] is Hermitian: q.H.q=0 but H*q!=0. Finite tensor controls, not reconstructed microscopic loop integrals. Zero-wavevector cancellation is vacuous; gauge invariance alone does not establish a nonzero London limit. (4b)
nonzero_transverse_corrections_preserve_gauge_invariance_and_screening · scalar_longitudinal_projection_does_not_establish_tensor_cancellation
At eta=1/1000, |kappa-kappa_ref|=10>1 while kappa=11>0. A constructed correction family, not Nambu's numerical coefficient. An unspecified asymptotic constant cannot certify a relative error below one at a chosen coupling. (4c)
asymptotic_order_is_not_a_selected_finite_coupling_error_bar
Nambu explicitly notes that the individual loop integrals are infinite and that the momentum translation used in (5.6) is ambiguous. The Lean tensor readout represents finite, consistently interpreted calculation outputs; it does not evaluate those divergent integrals or establish regulator independence. The alternative finite small-q calculation and the source's warning about unassessed neglected terms remain important limits on the physical argument.
A separate interpretation bridge turns the opposing long-wavelength current into exclusion of the field from the bulk. The resulting gauge-invariant response is the source map's formal main conclusion.
⇒ bulk field expulsion and a gauge-invariant Meissner calculation.
corrected_transverse_response_establishes_meissner_screening; pp. 648, 657–658
(5)
The anomalous gap prepares the matched Ward problem; the vertex and collective correction repair the bare longitudinal response; and the corrected transverse calculation supplies the induced opposing current. A separate field-exclusion bridge is still required. Together these source stages realize the typed screening mechanism directly, while the microscopic vertex and collective interpretation remain Nambu-local.
nambu_source_inputs_realize_mechanistic_transverse_meissner_screening_explanation · Physical Review pp. 652–658
The raw relation retains the anomalous gap, matched Ward vertex, bare longitudinal defect, gauge-phase and homogeneous pair calculation, a separate collective-insertion bridge, corrected transverse calculation, and field-exclusion bridge. Checked helpers derive the pair result before placing it in the longitudinal Meissner correction. nambu_source_derivation_realizes_source_gap_and_screening_explanations retains this screening explanation together with the source-sensitive anomalous-gap explanation, without identifying the gapped quasiparticle spectrum with the gapless collective spectrum. The corrected response cancels the pure-gauge longitudinal current while retaining the essentially unchanged transverse BCS response.
nambu_source_derivation_establishes_zero_momentum_pair_result · nambu_source_derivation_exposes_collective_meissner_intermediate · nambu_source_derivation_realizes_source_mechanistic_transverse_meissner_screening_explanation · nambu_source_derivation_realizes_source_gap_and_screening_explanations · Physical Review pp. 652–658
The calculation also establishes the corrected response as invariant under gauge-related states. Once both selected vacua are known to represent the same superconductor, invariant_response_agrees_on_selected_gauge_representatives gives equality of their corrected response values.
The homogeneous vertex solution yields a zero mode before Coulomb pair processes are included
The zero-momentum setup combines the Ward and gauge-phase data with phonon-mediated ladder pair scattering and explicitly omits Coulomb pair annihilation–creation from the ladder spectrum. The calculation makes the vertex solution homogeneous at zero momentum and identifies a bound quasiparticle pair with zero total energy and momentum.
⇒ bound zero-energy, zero-momentum pair, gapless collective mode in the ladder spectrum, and a zero-frequency pole there.
ZeroMomentumPairCalculation; Physical Review p. 658
(6)
This route realizes the output-led shared broken-symmetry spectrum result by directly retaining the moved gauge-phase vacua and the concrete zero mode in the ladder spectrum. Its complete Goldstone route is reconstructible from that output. The grounding requires the gauge-phase broken setup and physical-system representation, but not the Ward calculation or zero-mode calculation. Its finite-momentum continuation retains weak coupling and continued omission of the Coulomb pair terms.
for the finite-momentum continuation in the Coulomb-omitted ladder spectrum. value-level equation (6.11);
collective_dispersion_retains_equation_six_eleven; p. 659
(7)
The source anchor describes the derived branch as linear. The route now retains its squared slope formula while keeping weak coupling and Coulomb omission explicit.
Conserved corrected current does not make the bare quasiparticle a local charge eigenstate
The charge-cloud setup states that the selected quasiparticle is not a charge eigenstate even though the corrected current satisfies continuity. That current decomposes into a quasiparticle core and a collective cloud associated with the zero-momentum pair mode.
accelerated quasiparticle exchanges charge with the medium, so its finite-region charge is not constant.
conserved_current_uses_nonlocal_collective_charge_cloud; pp. 660–661
(8)
The result reconciles current continuity with nonlocal charge dressing: conservation belongs to the core-plus-cloud current, not to an isolated local quasiparticle charge.
Coulomb polarization converts the ladder zero mode into a finite plasma mode
The conversion setup keeps the original mode in the Coulomb-omitted ladder spectrum and selects a different Coulomb-coupled spectrum in which pair annihilation–creation is active. The original mode is coupled through Coulomb polarization, and polarization bubbles are resummed.
in the Coulomb-coupled spectrum: finite plasma mode, original zero mode absent, zero-frequency pole removed, and correct total-charge correlation limit. value-level equation (8.11);
coulomb_calculation_retains_equation_eight_eleven; pp. 661–662
(9)
Before and after are not one spectrum
coulomb_plasma_setup_distinguishes_before_and_after_spectra proves that Coulomb pair processes are absent from the ladder spectrum and present in the coupled spectrum. The zero-energy pole and finite-frequency plasma mode therefore belong to different calculation stages.
The paper's approximation boundary is an independent formal route
The scope proposition states generalized Hartree–Fock in the weak-coupling regime, linear response in the static field regime, and a weak-coupling approximation. It simultaneously states three negative results.
with higher field orders unanalyzed, neglected weak-coupling terms uncontrolled, and beyond-Hartree–Fock corrections unassessed.
ApproximationScope; pp. 656, 662–663
(10)
This route has no dependency on the successful Meissner or collective calculations, which prevents those results from silently discharging the missing higher-order theory.
Selected-State Scope
Both gauge-related representatives remain in the selected self-consistent family. Their law-specific selected orbit is explicit.
Selected representatives are not automatically physically distinct states. The neutral adapter has no physical-classification field: it neither affirms nor denies that interpretation, and supplies no Ward or collective-mode calculation.
the_selected_pairing_vacua_retain_selection_without_physical_classification
Concept guide
Self-consistent anomalous gap
The generalized Hartree–Fock solution that is anomalous, nonperturbative, not finitely perturbative, and carries the square-root quasiparticle dispersion with gap 2|φ|.
SelfConsistentGapSetup · EquationTwoFifteenQuasiparticleGapFormulaAtGauge-phase family
An exact continuous constant-phase symmetry moving the quasiparticle vacuum through the cosine-sine anomalous-self-energy family.
GaugePhaseFamilySetup · EquationTwoTwentyGaugePhaseFamilyFormulaAtGauge-representative agreement
Equality of corrected physical response values after invariance has been proved on two gauge-related states representing the same system.
SelectedGaugeRepresentativesMatched Ward vertex
The vertex built from the self-energy kernel with photon insertion at every charged line, retaining the two-by-two matrix relation L(p′)τ3 − τ3L(p).
WardIdentitySetup · EquationFourFourChargeWardFormulaAtGauge-invariant Meissner response
Collective longitudinal cancellation at nonzero q together with retained transverse current, field opposition, bulk exclusion, and response invariance.
GaugeInvariantMeissnerSetup · EquationFiveNineLongitudinalCancellationFormulaAtCoulomb-omitted zero mode
The bound zero-energy, zero-momentum pair and zero-frequency pole in the phonon ladder spectrum.
ZeroMomentumCollectiveSetupFinite-momentum collective branch
The weak-coupling continuation whose equation-(6.11) linear dispersion remains in the ladder spectrum and begins at zero energy.
FiniteMomentumCollectiveSetup · EquationSixElevenCollectiveDispersionFormulaAtNonlocal quasiparticle charge cloud
The conserving current's quasiparticle core and collective cloud, with charge exchange across finite regions.
QuasiparticleChargeCloudSetupCoulomb plasma conversion
Resummed polarization converting the ladder zero mode into the distinct Coulomb-coupled plasma mode with equation-(8.11) frequency.
CoulombPlasmaSetup · EquationEightElevenPlasmaFrequencyFormulaAtApproximation boundary
Generalized Hartree–Fock, linear field, and weak coupling, with three classes of correction left open.
ApproximationScopeShared superconductivity semantics
The four grounded reusable models for spectral gap, transverse screening, broken-symmetry spectrum, and interaction-driven mode conversion.
selfConsistentSpectralGapModelComplete route inventory and provenance
The source map declares nine routes, forty-seven claims, and forty-seven sourced steps. Coverage interprets every atom, certifies every route, and proves exhaustive semantic realization. Six dependent setup families now have explicit local-input claims and assembly steps, and every nontrivial step reconstructs its selected atoms from checked premises before applying a paper-local theorem. Gauge-invariant Meissner response is the declared main conclusion; the finite-momentum, charge-cloud, plasma, and approximation-boundary outputs remain separately certified rather than being assembled into an unlisted complete result.
| Route | Direct dependencies | Declared outputs | Profile |
|---|---|---|---|
| Self-consistent gap | — | Nonperturbative solution; finite gap | independent controlled root |
| Gauge-phase family | — | Broken phase; selected representatives | independent physical root |
| Ward identity | Self-consistent gap | Exact Ward solution; conserving current | matched-vertex route |
| Gauge-invariant Meissner | Gauge phase; Ward identity | Cancellation, pure-gauge zero, transverse response, screening, invariance, representative agreement | formal main route |
| Zero-momentum collective mode | Gauge phase; Ward identity | Ladder bridge; zero mode in spectrum | Coulomb-omitted ladder route |
| Finite-momentum dispersion | Zero-momentum mode | Gapless collective branch | controlled continuation |
| Quasiparticle charge cloud | Ward identity; zero-momentum mode | Nonlocal core-plus-cloud charge exchange | conserving-current interpretation |
| Coulomb plasma shift | Zero-momentum mode | Conversion bridge, finite plasma mode, zero-pole removal, charge limit | polarization conversion |
| Approximation boundary | — | Higher-field, neglected-term, and beyond-Hartree–Fock limitations | independent open root |
Gap · self_consistent_gap_route_is_semantically_realized
Gauge phase · gauge_phase_family_route_is_semantically_realized
Ward identity · ward_identity_route_is_semantically_realized
Meissner response · gauge_invariant_meissner_route_is_semantically_realized
Zero mode · zero_momentum_collective_route_is_semantically_realized
Finite momentum · finite_momentum_dispersion_route_is_semantically_realized
Charge cloud · quasiparticle_charge_cloud_route_is_semantically_realized
Plasma conversion · coulomb_plasma_shift_route_is_semantically_realized
Approximation boundary · approximation_boundary_route_is_semantically_realized
All forty-seven source-mapped claims
| Claim group | Source anchor | Status |
|---|---|---|
| Two-component matrix setup, gap calculation, interpretation, nonperturbative solution, and finite gap | Physical Review pp. 652–653 | Controlled setup and paper derivation |
| Phase setup, broken representation, representatives, response invariance, and agreement | pp. 650, 653, 657–658 | Physical principle and paper derivation |
| Ward local input, assembled setup, calculation, identity, and conserving current | pp. 652, 655–656 | Controlled setup and paper derivation |
| Meissner local input, assembled setup, calculation, cancellation, pure-gauge zero, transverse result, bridge, and invariant response | pp. 648, 657–658 | Linear-response calculation and physical interpretation |
| Zero-mode local input, assembled setup, calculation, ladder bridge, and spectrum result | p. 658 | Controlled approximation and derivation |
| Finite-momentum local input, assembled setup, calculation, and branch | p. 659 | Controlled approximation |
| Charge-cloud local input, assembled setup, calculation, and exchange result | pp. 660–661 | Physical setup and paper derivation |
| Plasma local input, assembled setup, calculation, conversion bridge, shift, pole removal, and charge limit | pp. 650, 661–662 | Physical setup and paper derivation |
| Approximation scope and three open corrections | pp. 656, 662–663 | Open obligations |
Finite formula-boundary countermodels
Three reduced readouts show that named physical outputs cannot replace the printed equations. A positive pairing scale/gap with nonnegative quasiparticle energy can still fail equation (2.15)'s selected pairing equality. A nonzero longitudinal wavevector with exact longitudinal cancellation can still fail the two-by-two complex matrix Ward relation (4.4b). Positive electron mass/density and a valid Coulomb plasma-frequency equation can still fail the Coulomb-omitted collective dispersion (6.11). No constant proposition or formula-label truth table is used. The broader logical boundaries remain carried by explicit negative propositions: no finite perturbation-series generation, bare longitudinal non-invariance, absence or presence of Coulomb pair processes in different spectra, nonconstant finite-region charge, removed zero-frequency pole, and three unassessed correction classes.
Three epistemic-status audits
gap_route_retains_controlled_approximation preserves the generalized Hartree–Fock ancestry of the finite gap. collective_branch_retains_controlled_approximation preserves the controlled status of the finite-momentum branch. higher_order_scope_retains_open_obligation preserves the uncomputed higher-field orders.
Machine-checked audit boundary
argument_wellFormed, argument_auditable, and routes_wellFormed certify source structure. Exact predecessor, independent-contract, local-input, setup-assembly, formula-retention, and contract-application guards check that the graph does not manufacture calculation rules from their own antecedents or hide fresh setup assumptions inside inherited outputs. every_source_claim_has_semantics covers all fifty-four claims, and route_semantic_realization_is_exhaustive covers all nine routes. Four adapters separately establish and ground the reusable gap, transverse-screening, broken-symmetry-spectrum, and Coulomb-conversion patterns.
Lean-encoded bibliographic record
Y. Nambu, Quasi-Particles and Gauge Invariance in the Theory of Superconductivity, Physical Review 117 (1960), 648–663.
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 identifiers (105)
named_quasiparticle_gap_does_not_supply_equation_two_fifteennamed_ward_and_cancellation_outputs_do_not_supply_equations_four_four_and_five_ninenamed_collective_and_plasma_outputs_do_not_supply_equations_six_eleven_and_eight_eleven
self_consistent_gap_calculation_establishes_nonperturbative_solutionself_consistent_gap_inputs_establish_finite_quasiparticle_gapward_local_setup_and_nonperturbative_solution_make_ward_setupward_outputs_and_local_inputs_make_meissner_setupmeissner_calculation_establishes_longitudinal_cancellationmeissner_calculation_establishes_vanishing_pure_gauge_responsemeissner_calculation_retains_transverse_responsemeissner_outputs_and_bridge_establish_gauge_invariant_responsephase_ward_and_local_inputs_make_zero_momentum_setupzero_momentum_result_and_local_inputs_make_dispersion_setupcurrent_zero_mode_and_local_inputs_make_charge_cloud_setupzero_mode_result_and_local_coulomb_inputs_make_plasma_setupplasma_setup_and_conversion_bridge_establish_plasma_shiftcoulomb_calculation_removes_zero_frequency_polecoulomb_calculation_establishes_total_charge_limit
zero_momentum_pair_inputs_realize_structural_goldstone_spectrum_explanationzero_momentum_pair_inputs_realize_source_structural_goldstone_spectrum_explanation
nambu_source_inputs_realize_mechanistic_transverse_meissner_screening_explanation
nambuTransverseMeissnerScreeningDerivationObtainsnambu_source_derivation_makes_shared_screening_route_applicablenambu_source_derivation_realizes_source_mechanistic_transverse_meissner_screening_explanationnambu_source_derivation_realizes_source_gap_and_screening_explanations
ZeroMomentumPairMeissnerIntermediateBridgenambu_source_derivation_establishes_zero_momentum_pair_resultnambu_source_derivation_exposes_collective_meissner_intermediate
coulomb_plasma_setup_realizes_selected_mode_conversion_setup
coulomb_polarization_realizes_mechanistic_mode_conversion_explanation
zero_momentum_pair_and_coulomb_inputs_make_plasma_setup
nambuModeConversionDerivationObtains
matched_vertex_zero_mode_and_coulomb_resummation_realize_source_mechanistic_mode_conversion_explanation
equation_two_fourteen_retains_off_diagonal_pairingequations_two_fourteen_and_two_fifteen_make_anomalous_entry_nonzeroself_consistent_gap_setup_retains_equations_two_fourteen_and_sixteenselected_nambu_routes_retain_central_printed_formulasselected_nambu_routes_retain_two_component_and_central_printed_formulas
broken_symmetry_spectrum_model_retains_paper_selected_databroken_symmetry_mode_conversion_model_retains_paper_semanticsself_consistent_spectral_gap_model_retains_paper_semanticsmeissner_screening_model_retains_paper_semanticsself_consistent_gap_setup_realizes_shared_setupself_consistent_inputs_select_shared_spectral_gap_setupnonperturbative_calculation_realizes_shared_gap_solutiongap_interpretation_realizes_shared_spectral_bridgeself_consistent_inputs_make_shared_gap_route_applicableself_consistent_nonperturbative_solution_realizes_shared_gapnonperturbative_solution_exhibits_nonvacuous_shared_spectral_gapestablished_nonperturbative_gap_realizes_every_selected_shared_claimanomalous_gap_model_inputs_establish_theory_model_groundingself_consistent_solution_establishes_theory_model_grounded_gapgrounded_nonperturbative_gap_transfers_every_selected_shared_claimself_consistent_nonperturbative_solution_establishes_gapgauge_phase_family_realizes_foundation_breakinggauge_phase_family_realizes_continuous_exact_symmetry_with_moved_stateinvariant_response_agrees_on_selected_gauge_representativesmatched_vertex_equation_establishes_conserving_currentcollective_vertex_correction_restores_meissner_gauge_invariancecorrected_transverse_response_establishes_meissner_screeningnambu_meissner_setup_realizes_shared_transverse_response_setupnambu_response_calculation_realizes_shared_induced_currentnambu_field_expulsion_realizes_shared_interpretation_bridgeestablished_gap_and_ward_inputs_make_gauge_invariant_meissner_setupestablished_gap_is_admissible_for_nambu_transverse_response_setupnambu_inputs_make_shared_meissner_screening_route_applicablegap_supported_nambu_inputs_make_shared_meissner_screening_route_applicablenambu_response_realizes_shared_transverse_meissner_screeningnambu_response_exhibits_nonvacuous_shared_transverse_meissner_screeninggap_supported_nambu_response_realizes_shared_transverse_meissner_screeninggap_supported_nambu_response_exhibits_nonvacuous_shared_transverse_meissner_screeningnambu_screening_model_inputs_establish_theory_model_groundingnambu_response_establishes_grounded_shared_meissner_screeninggrounded_nambu_screening_transfers_every_shared_claimzero_momentum_pair_calculation_realizes_shared_spectral_bridgezero_momentum_pair_inputs_make_shared_goldstone_route_applicableself_energy_and_vertex_structure_establish_zero_energy_pair_modezero_momentum_pair_calculation_establishes_specific_ladder_modezero_momentum_pair_result_exposes_scoped_gapless_modezero_momentum_pair_exhibits_nonvacuous_broken_phase_and_ladder_modezero_momentum_pair_realizes_every_shared_goldstone_spectrum_claimzero_momentum_pair_model_inputs_establish_theory_model_groundingzero_momentum_pair_establishes_theory_model_grounded_goldstone_spectrumgrounded_zero_momentum_pair_spectrum_transfers_every_shared_claimperturbative_continuation_yields_gapless_collective_branchconserved_current_uses_nonlocal_collective_charge_cloudcoulomb_plasma_setup_distinguishes_before_and_after_spectracoulomb_calculation_realizes_shared_mode_conversion_calculationcoulomb_polarization_establishes_shared_mode_conversioncoulomb_polarization_exhibits_nonvacuous_shared_mode_conversionbroken_phase_goldstone_and_coulomb_conversion_realize_shared_routecoulomb_polarization_route_exhibits_nonvacuous_two_spectrum_conversionbroken_phase_goldstone_and_coulomb_conversion_realizes_every_shared_claimcoulomb_coupled_model_inputs_establish_theory_model_groundingbroken_phase_goldstone_and_coulomb_conversion_establish_theory_model_grounded_conversiongrounded_broken_phase_conversion_transfers_every_shared_claimcoulomb_polarization_shifts_collective_mode_to_plasma_frequencyapproximation_scope_preserves_open_correctionsplasma_shift_retains_imported_response_calculationhigher_field_and_beyond_hartree_fock_extensions_remain_open
Coverage theorems (11)
every_source_claim_has_semanticsself_consistent_gap_route_is_semantically_realizedgauge_phase_family_route_is_semantically_realizedward_identity_route_is_semantically_realizedgauge_invariant_meissner_route_is_semantically_realizedzero_momentum_collective_route_is_semantically_realizedfinite_momentum_dispersion_route_is_semantically_realizedquasiparticle_charge_cloud_route_is_semantically_realizedcoulomb_plasma_shift_route_is_semantically_realizedapproximation_boundary_route_is_semantically_realizedall_routes_are_semantically_realizable
Source-map audit theorems (15)
argument_wellFormedargument_auditableroutes_wellFormedroutes_have_exact_predecessor_graphroutes_have_exact_dependency_closurecalculation_and_interpretation_contracts_are_independent_hypothesesroot_local_representative_and_scope_inputs_are_independent_hypothesesdependent_setup_assembly_steps_name_all_selected_inputsgap_ward_and_meissner_result_steps_apply_selected_setups_and_contractscollective_and_plasma_result_steps_apply_selected_setups_and_contractsprinted_formula_steps_apply_selected_setups_and_contractsdependent_routes_consume_certified_predecessor_outputsgap_route_retains_controlled_approximationcollective_branch_retains_controlled_approximationhigher_order_scope_retains_open_obligation
Semantic atoms (54)
selfConsistentGapSetupnonperturbativeGapCalculationgapInterpretationBridgeanomalousNonperturbativeSolutionfiniteQuasiparticleGaptwoComponentMatrixFormulasquasiparticleGapFormulagaugePhaseFamilySetupfoundationBreakingselectedGaugeRepresentativescorrectedResponseInvariantgaugeRepresentativeAgreementgaugePhaseFormulawardIdentityLocalSetupwardIdentitySetupwardIdentityCalculationexactWardSolutionconservingQuasiparticleCurrentchargeWardFormulagaugeInvariantMeissnerLocalSetupgaugeInvariantMeissnerSetupmeissnerResponseCalculationlongitudinalCollectiveCancellationpureGaugeResponseVanishestransverseResponseRetainedtransverseScreeningInterpretationBridgegaugeInvariantMeissnerResponselongitudinalCancellationFormulazeroMomentumCollectiveLocalSetupzeroMomentumCollectiveSetupzeroMomentumPairCalculationsharedLadderSpectrumBridgezeroEnergyPairInLadderSpectrumfiniteMomentumCollectiveLocalSetupfiniteMomentumCollectiveSetupfiniteMomentumDispersionCalculationgaplessCollectiveBranchcollectiveDispersionFormulachargeCloudLocalSetupchargeCloudSetupchargeCloudCalculationnonlocalChargeExchangecoulombPlasmaLocalSetupcoulombPlasmaSetupcoulombPlasmaCalculationsharedCoulombConversionBridgeplasmaFrequencyShiftzeroFrequencyPoleRemovedtotalChargeEigenstateLimitplasmaFrequencyFormulaapproximationScopehigherFieldOrdersOpenneglectedTermsUncontrolledbeyondHartreeFockOpen
Claim identifiers (54)
gapSetupgapCalculationgapBridgenonperturbativeSolutionfiniteGaptwoComponentFormulasgapFormulaphaseSetupbrokenPhaserepresentativesresponseInvariantrepresentativeAgreementphaseFormulawardLocalSetupwardSetupwardCalculationwardIdentityconservingCurrentwardFormulameissnerLocalSetupmeissnerSetupmeissnerCalculationlongitudinalCancellationvanishingGaugeResponseretainedTransverseResponsemeissnerBridgeinvariantMeissnercancellationFormulazeroModeLocalSetupzeroModeSetupzeroModeCalculationladderBridgezeroModeSpectrumdispersionLocalSetupdispersionSetupdispersionCalculationcollectiveBranchdispersionFormulacloudLocalSetupcloudSetupcloudCalculationchargeCloudplasmaLocalSetupplasmaSetupplasmaCalculationplasmaBridgeplasmaShiftzeroPoleRemovalchargeLimitplasmaFormulascopehigherFieldScopeneglectedTermScopehartreeFockScope
Step identifiers (54)
stateGapSetupsupplyGapCalculationsupplyGapInterpretationderiveNonperturbativeSolutionderiveFiniteGapretainTwoComponentFormulasretainGapFormulastateGaugePhaseSetuprealizeBrokenPhasestateSelectedRepresentativesretainCorrectedResponseInvariancederiveRepresentativeAgreementretainGaugePhaseFormulastateWardLocalSetupassembleWardSetupsupplyWardCalculationderiveWardIdentityderiveConservingCurrentretainWardFormulastateMeissnerLocalSetupassembleMeissnerSetupsupplyMeissnerCalculationderiveLongitudinalCancellationderiveVanishingGaugeResponseretainTransverseResponsestateMeissnerBridgederiveGaugeInvariantMeissnerretainCancellationFormulastateZeroModeLocalSetupassembleZeroModeSetupsupplyZeroModeCalculationrealizeLadderSpectrumBridgederiveZeroModeSpectrumstateDispersionLocalSetupassembleDispersionSetupsupplyDispersionCalculationderiveCollectiveBranchretainDispersionFormulastateChargeCloudLocalSetupassembleChargeCloudSetupsupplyChargeCloudCalculationderiveNonlocalChargeExchangestatePlasmaLocalSetupassemblePlasmaSetupsupplyPlasmaCalculationrealizePlasmaBridgederivePlasmaShiftremoveZeroFrequencyPolederiveChargeEigenstateLimitretainPlasmaFormulastateApproximationScoperetainHigherFieldScoperetainNeglectedTermScoperetainBeyondHartreeFockScope
Route identifiers (9)
selfConsistentGapgaugePhaseFamilywardIdentitygaugeInvariantMeissnerzeroMomentumCollectivefiniteMomentumDispersionquasiparticleChargeCloudcoulombPlasmaShiftapproximationBoundary
Route kinds (9)
nonperturbativeSelfConsistencygaugeRelatedBrokenRepresentationmatchedVertexIdentitygaugeRestoredLinearResponsehomogeneousPairModecontrolledDispersionnonlocalConservedChargecoulombPolarizationConversionunresolvedApproximationScope
Current checked semantic identifiers
These complete lists follow current Lean declaration order. Historical and selected explanatory lists elsewhere retain their separate scope.
Primary semantic theorems (134)
actual_ward_contraction, equation_two_fourteen_retains_off_diagonal_pairing, equations_two_fourteen_and_two_fifteen_make_anomalous_entry_nonzero, equation_five_nine_and_remaining_terms_cancel_the_actual_longitudinal_kernel, actual_tensor_cancellation_implies_vanishing_pure_gauge_response, actual_tensor_cancellation_implies_gauge_invariant_current, named_quasiparticle_gap_does_not_supply_equation_two_fifteen, named_ward_and_cancellation_outputs_do_not_supply_equations_four_four_and_five_nine, named_collective_and_plasma_outputs_do_not_supply_equations_six_eleven_and_eight_eleven, broken_symmetry_spectrum_model_retains_paper_selected_data, broken_symmetry_mode_conversion_model_retains_paper_semantics, self_consistent_spectral_gap_model_retains_paper_semantics, self_consistent_gap_setup_retains_equations_two_fourteen_and_sixteen, meissner_screening_model_retains_paper_semantics, self_consistent_gap_calculation_establishes_nonperturbative_solution, self_consistent_gap_inputs_establish_finite_quasiparticle_gap, gap_calculation_retains_equation_two_fifteen, self_consistent_gap_setup_realizes_shared_setup, self_consistent_inputs_select_shared_spectral_gap_setup, nonperturbative_calculation_realizes_shared_gap_solution, gap_interpretation_realizes_shared_spectral_bridge, self_consistent_inputs_make_shared_gap_route_applicable, nonperturbative_gap_route_realizes_structural_self_consistent_spectral_gap_explanation, nonperturbative_gap_route_realizes_source_structural_self_consistent_spectral_gap_explanation, self_consistent_nonperturbative_solution_realizes_shared_gap, nonperturbative_solution_exhibits_nonvacuous_shared_spectral_gap, established_nonperturbative_gap_realizes_every_selected_shared_claim, anomalous_gap_model_inputs_establish_theory_model_grounding, self_consistent_solution_establishes_theory_model_grounded_gap, grounded_nonperturbative_gap_transfers_every_selected_shared_claim, self_consistent_nonperturbative_solution_establishes_gap, gauge_phase_setup_retains_equation_two_twenty, gauge_phase_family_realizes_foundation_breaking, gauge_phase_family_realizes_continuous_exact_symmetry_with_moved_state, the_selected_pairing_vacua_retain_selection_without_physical_classification, invariant_response_agrees_on_selected_gauge_representatives, ward_local_setup_and_nonperturbative_solution_make_ward_setup, matched_vertex_equation_establishes_conserving_current, ward_result_retains_equation_four_four, retained_transverse_kernel_and_current_calibration_imply_london_current, meissner_calculation_derives_response_outputs, meissner_calculation_exhibits_actual_transverse_london_limit, retained_transverse_response_has_a_qualified_correction_order, ward_outputs_and_local_inputs_make_meissner_setup, collective_vertex_correction_restores_meissner_gauge_invariance, meissner_calculation_establishes_longitudinal_cancellation, meissner_calculation_retains_equation_five_nine, meissner_calculation_establishes_vanishing_pure_gauge_response, meissner_calculation_retains_transverse_response, meissner_outputs_and_bridge_establish_gauge_invariant_response, corrected_transverse_response_establishes_meissner_screening, nambu_meissner_setup_realizes_shared_transverse_response_setup, nambu_response_calculation_realizes_shared_induced_current, nambu_field_expulsion_realizes_shared_interpretation_bridge, established_gap_and_ward_inputs_make_gauge_invariant_meissner_setup, established_gap_is_admissible_for_nambu_transverse_response_setup, nambu_inputs_make_shared_meissner_screening_route_applicable, gap_supported_nambu_inputs_make_shared_meissner_screening_route_applicable, nambu_source_inputs_realize_mechanistic_transverse_meissner_screening_explanation, nambu_response_realizes_shared_transverse_meissner_screening, nambu_response_exhibits_nonvacuous_shared_transverse_meissner_screening, gap_supported_nambu_response_realizes_shared_transverse_meissner_screening, gap_supported_nambu_response_exhibits_nonvacuous_shared_transverse_meissner_screening, nambu_screening_model_inputs_establish_theory_model_grounding, nambu_response_establishes_grounded_shared_meissner_screening, grounded_nambu_screening_transfers_every_shared_claim, phase_ward_and_local_inputs_make_zero_momentum_setup, zero_momentum_pair_calculation_establishes_specific_ladder_mode, zero_momentum_pair_result_exposes_scoped_gapless_mode, zero_momentum_pair_calculation_realizes_shared_spectral_bridge, zero_momentum_pair_inputs_make_shared_goldstone_route_applicable, nambu_source_derivation_establishes_zero_momentum_pair_result, nambu_source_derivation_exposes_collective_meissner_intermediate, nambu_source_derivation_makes_shared_screening_route_applicable, nambu_source_derivation_realizes_source_mechanistic_transverse_meissner_screening_explanation, nambu_source_derivation_realizes_source_gap_and_screening_explanations, anomalous_gap_ward_collective_cancellation_realize_source_sensitive_meissner_screening, zero_momentum_pair_inputs_realize_structural_goldstone_spectrum_explanation, zero_momentum_pair_inputs_realize_source_structural_goldstone_spectrum_explanation, self_energy_and_vertex_structure_establish_zero_energy_pair_mode, zero_momentum_pair_exhibits_nonvacuous_broken_phase_and_ladder_mode, zero_momentum_pair_realizes_every_shared_goldstone_spectrum_claim, zero_momentum_pair_model_inputs_establish_theory_model_grounding, zero_momentum_pair_establishes_theory_model_grounded_goldstone_spectrum, grounded_zero_momentum_pair_spectrum_transfers_every_shared_claim, zero_momentum_result_and_local_inputs_make_dispersion_setup, perturbative_continuation_yields_gapless_collective_branch, collective_dispersion_retains_equation_six_eleven, current_zero_mode_and_local_inputs_make_charge_cloud_setup, conserved_current_uses_nonlocal_collective_charge_cloud, zero_mode_result_and_local_coulomb_inputs_make_plasma_setup, zero_momentum_pair_and_coulomb_inputs_make_plasma_setup, coulomb_plasma_setup_distinguishes_before_and_after_spectra, coulomb_calculation_realizes_shared_mode_conversion_calculation, plasma_setup_and_conversion_bridge_establish_plasma_shift, coulomb_calculation_removes_zero_frequency_pole, coulomb_calculation_establishes_total_charge_limit, coulomb_calculation_retains_equation_eight_eleven, selected_nambu_routes_retain_central_printed_formulas, selected_nambu_routes_retain_two_component_and_central_printed_formulas, coulomb_polarization_establishes_shared_mode_conversion, coulomb_polarization_exhibits_nonvacuous_shared_mode_conversion, coulomb_polarization_realizes_mechanistic_mode_conversion_explanation, matched_vertex_zero_mode_and_coulomb_resummation_realize_source_mechanistic_mode_conversion_explanation, broken_phase_goldstone_and_coulomb_conversion_realize_shared_route, coulomb_polarization_route_exhibits_nonvacuous_two_spectrum_conversion, broken_phase_goldstone_and_coulomb_conversion_realizes_every_shared_claim, coulomb_plasma_setup_realizes_selected_mode_conversion_setup, coulomb_coupled_model_inputs_establish_theory_model_grounding, broken_phase_goldstone_and_coulomb_conversion_establish_theory_model_grounded_conversion, grounded_broken_phase_conversion_transfers_every_shared_claim, coulomb_polarization_shifts_collective_mode_to_plasma_frequency, approximation_scope_preserves_open_corrections, matrix_ward_neutral_pair_and_coulomb_resummation_realize_source_sensitive_mode_conversion, plasma_shift_retains_imported_response_calculation, higher_field_and_beyond_hartree_fock_extensions_remain_open, direction_is_nonzero, probe_is_nonzero, probe_is_transverse, response_control_retains_equation_five_nine, response_control_retains_the_remaining_terms, response_control_is_gauge_invariant, response_family_current_is_computed, response_family_has_an_actual_london_limit, response_family_has_nonvacuous_screening, correction_family_has_the_qualified_weak_coupling_order, nonzero_transverse_corrections_preserve_gauge_invariance_and_screening, steep_correction_family_has_the_same_asymptotic_order, asymptotic_order_is_not_a_selected_finite_coupling_error_bar, equation_five_nine_does_not_control_an_unchecked_cnumber_term, equation_five_nine_does_not_control_an_unchecked_polarization_term, scalar_longitudinal_projection_does_not_establish_tensor_cancellation, cancellation_at_zero_wavevector_does_not_test_a_finite_gauge_mode, gauge_invariance_does_not_supply_a_meissner_london_limit
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.
selfConsistentGap
Logical kind: nonperturbativeSelfConsistency.
Required predecessor routes: none.
Ordered inference steps: stateGapSetup, retainTwoComponentFormulas, supplyGapCalculation, retainGapFormula, supplyGapInterpretation, deriveNonperturbativeSolution, deriveFiniteGap.
Exported conclusions: nonperturbativeSolution, finiteGap, twoComponentFormulas, gapFormula.
gaugePhaseFamily
Logical kind: gaugeRelatedBrokenRepresentation.
Required predecessor routes: none.
Ordered inference steps: stateGaugePhaseSetup, retainGaugePhaseFormula, realizeBrokenPhase, stateSelectedRepresentatives.
Exported conclusions: phaseSetup, brokenPhase, representatives, phaseFormula.
wardIdentity
Logical kind: matchedVertexIdentity.
Required predecessor routes: selfConsistentGap.
Ordered inference steps: stateWardLocalSetup, assembleWardSetup, supplyWardCalculation, deriveWardIdentity, retainWardFormula, deriveConservingCurrent.
Exported conclusions: wardSetup, wardIdentity, conservingCurrent, wardFormula.
gaugeInvariantMeissner
Logical kind: gaugeRestoredLinearResponse.
Required predecessor routes: gaugePhaseFamily, wardIdentity.
Ordered inference steps: stateMeissnerLocalSetup, assembleMeissnerSetup, supplyMeissnerCalculation, deriveLongitudinalCancellation, retainCancellationFormula, deriveVanishingGaugeResponse, retainTransverseResponse, stateMeissnerBridge, deriveGaugeInvariantMeissner, retainCorrectedResponseInvariance, deriveRepresentativeAgreement.
Exported conclusions: longitudinalCancellation, vanishingGaugeResponse, retainedTransverseResponse, meissnerBridge, invariantMeissner, responseInvariant, representativeAgreement, cancellationFormula.
zeroMomentumCollective
Logical kind: homogeneousPairMode.
Required predecessor routes: gaugePhaseFamily, wardIdentity.
Ordered inference steps: stateZeroModeLocalSetup, assembleZeroModeSetup, supplyZeroModeCalculation, realizeLadderSpectrumBridge, deriveZeroModeSpectrum.
Exported conclusions: ladderBridge, zeroModeSpectrum.
finiteMomentumDispersion
Logical kind: controlledDispersion.
Required predecessor routes: zeroMomentumCollective.
Ordered inference steps: stateDispersionLocalSetup, assembleDispersionSetup, supplyDispersionCalculation, deriveCollectiveBranch, retainDispersionFormula.
Exported conclusions: collectiveBranch, dispersionFormula.
quasiparticleChargeCloud
Logical kind: nonlocalConservedCharge.
Required predecessor routes: wardIdentity, zeroMomentumCollective.
Ordered inference steps: stateChargeCloudLocalSetup, assembleChargeCloudSetup, supplyChargeCloudCalculation, deriveNonlocalChargeExchange.
Exported conclusions: chargeCloud.
coulombPlasmaShift
Logical kind: coulombPolarizationConversion.
Required predecessor routes: zeroMomentumCollective.
Ordered inference steps: statePlasmaLocalSetup, assemblePlasmaSetup, supplyPlasmaCalculation, realizePlasmaBridge, derivePlasmaShift, retainPlasmaFormula, removeZeroFrequencyPole, deriveChargeEigenstateLimit.
Exported conclusions: plasmaBridge, plasmaShift, zeroPoleRemoval, chargeLimit, plasmaFormula.
approximationBoundary
Logical kind: unresolvedApproximationScope.
Required predecessor routes: none.
Ordered inference steps: stateApproximationScope, retainHigherFieldScope, retainNeglectedTermScope, retainBeyondHartreeFockScope.
Exported conclusions: higherFieldScope, neglectedTermScope, hartreeFockScope.