Formal reconstruction - source-grounded physical definitions - explicit assumptions - checked inference routes
Mermin-Wagner 1966
A reconstruction derived directly from proposition-valued Lean definitions and checked theorems
Definitions, structures, and assumptions
Structures, classes, and inductive alternatives
- inductive
- structureProof-free physical indices selected by one infrared no-order route. The expectation calculation and its interpretation bridge remain relations on the model rather than fields of this constraint.
- structureNeutral proposition-valued semantics for the selected no-order route.
- structureThe shared physical constraint paired with one typed paper-local derivation. The derivation token is proof-free; its realization relation is supplied by the paper and is not reconstructed from the shared no-order endpoint.
- structurePaper-local theory and world interpretations of the shared claims.
- structureThe selected, proof-free physical data of one infrared no-order route.
- structureThe containing theory is distinct from the selected calculation model.
- structureThe represented physical system is distinct from theory and model.
- structureThe physical phenomenon explained by the route: the selected charged order is infrared-suppressed and its selected symmetry is unbroken. The phenomenon stores neither the paper-local calculation nor any claim about other order.
- 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
- inductiveA finite periodic spin box or its selected infinite-volume description.
- inductiveThe source first takes infinite volume and only then removes the field.
- inductive
- inductive
- inductive
- inductiveA typed source token for the finite-volume Bogoliubov calculation, its thermodynamic transfer, the low-dimensional infrared estimate, and the ordered small-field limit. It is deliberately distinct from the shared no-order endpoint.
- structureThe physical readouts used in the letter. `exchangeSecondMoment` represents the sum of `R^2 |J(R)|`; the separate convergence relation retains the footnote's weakening of finite range. Mode readouts are indexed by a real wave-number magnitude, while `finiteInfraredSum` and `infiniteInfraredIntegral` retain the Brillouin-zone sum and integral.
- inductiveUniform magnetization and the alternating two-sublattice order channel.
- inductiveRegimes explicitly separated by the source's scope discussion.
- structureThe finite, genuinely noncommutative operator data on journal p. 1134. The matrix dimension is the dimension of the selected finite-spin Hilbert space, not the number of lattice sites.
- inductiveCartesian and ladder operators appearing in the finite Heisenberg model.
- structure
- structureOne observable family and its two approach filters, without stored limit results.
- structureProof-free semantics for a selected physical system, two distinct limiting operations, an observable, a candidate result, and its separate source-level certification.
- structureThe actual sufficient premises of one argument, separate from its conclusion. `Sound` is an explicit logical obligation, not a proof field. A false premise is not the same thing as an unavailable proof, and neither relation represents the empirical validity of an underlying physical theory.
- structure
- structure
- structure
- structure
Definitions and domain choices
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe established result is output-led: it stores no calculation contract.
- definition
- definition
- definition
- definitionStructural explanation retaining one realized paper-local derivation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionSource-sensitive explanation retains the ordinary route together with one independently realized paper-local derivation token.
- definitionOrdinary structural explanation keeps exactly the selected infrared route and the resulting nonvacuous no-order phenomenon, without paper-local provenance.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe real order expectation tends to zero in the selected infrared limit.
- definitionDirect, inhabited output semantics, with other-order data left unconstrained.
- definition
- definitionThe physical interpretation bridge is separate from the calculation.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe exact physical indices selected by this infrared no-order route.
- definitionThe selected physical indices paired with one paper-local derivation.
- definitionThe selected infrared-suppressed, unbroken-symmetry phenomenon.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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
- 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.
- 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
- definitionFinite range or the weaker second-moment condition controls the exchange. In either branch the reported moment must equal its actual weighted sum.
- definition
- definitionThe source's explicitly stated anisotropic exception: `J_y = J_z != J_x`, with an aligning field in the `z` direction. Its calculation is separate from the isotropic theorem.
- definitionThe separate calculation asserted for the source's axial exception.
- definitionThe source's qualified anisotropic aligning-field scope.
- definitionThe source's inner-product and Schwarz-inequality derivation of (3).
- definitionEquation (3), written without division or an implicit existence claim.
- definitionPeriodic Bravais boxes with `J(0) = 0` and even exchange `J(-R) = J(R)`.
- definitionThe separate purely classical-spin argument asserted in the source.
- definitionThe similar, but distinct, crystalline no-order argument asserted on p. 1135.
- definitionThe domain-inclusive upper estimate underlying corrected (9). We use its nonstrict closure, retaining the zero mode where the field term is exact. This is not a claim that the author's printed strict sign holds there.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (11), retaining the finite Brillouin-zone infrared sum.
- definitionEquation (14), corrected by the author's erratum on p.1307: the arctangent receives the positive one-half power, on the same nondegenerate domain.
- definitionEquation (13) on its positive-omega, nonzero-field domain. Multiplying out the denominator does not extend the source's ratio formula to omega = 0.
- definitionEquation (12), with the spin-density factor `1/rho` made explicit.
- definition
- definition
- definition
- definition
- definition
- definition
- definitionLiteral extra field factor in the original (2), removed by the erratum.
- definition
- definition
- definitionThe finite calculation from (3), (8)-(10) to the uniform estimate (11).
- definitionEquation (8) after choosing `C = S_+(k)` and `A = S_-(-k-K)`. The strictly positive denominator is retained explicitly; the product form avoids a totalized inverse at a zero denominator.
- definitionAll finite mode, denominator, and spin-sum inputs used before (11).
- definitionA finite range bounds the support of the actual exchange couplings.
- definitionFootnote 7 requires convergence to the actual reported exchange moment.
- definitionThe finite-box package needed for the thermodynamic passage. It retains the finite mode bound, denominator bound, spin sum rule, and the uniform equation-(11) family as distinct inputs.
- definitionEvery momentum used by the source calculation lies in the first zone.
- definitionThe source's scale `omega = S(S+1) k_0^2 sum_R R^2 |J(R)|`.
- definition
- definition
- definitionThe scoped infrared evaluation of equation (12), including the author erratum. Only the dimension-specific estimates are imported. Their actual zero-field limit and the absence of spontaneous order are derived afterward. The common coefficient is for the selected temperature, not a claim of uniform control across different temperatures.
- definition
- definition
- definition
- definitionA two-orientation macroscopic control, not a short-range Heisenberg model.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe common positive-temperature and exchange scope before isotropy.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- 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 susceptibility is the actual thermodynamic field derivative near zero.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe one-dimensional scaling in (2), with its field-factor erratum.
- definitionExistence and positivity of the three thermal operator readouts.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquations (4)-(6), retaining the actual noncommuting operator `B`.
- definitionThe omitted equal-energy pairs and exact spectral inner product.
- definitionFinite direct and reciprocal lattices have the same number of sites.
- definitionCartesian spin observables in the fixed Hilbert inner product, with local commutators, ladder operators, and the spin Casimir (original pp. 1134-1135). Hermiticity is not implied by these algebraic relations.
- definitionThe exact finite Gibbs state in a complete energy basis of the selected Hamiltonian. The spin-operator coordinates stay fixed while this basis may depend on both the ordering channel and the field (original p. 1134).
- definitionAll finite operator and Fourier input actually used by equation (8).
- definitionEquation (7), including both exchange and the selected ordering field.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionColumns are energy eigenvectors in the fixed operator coordinates. Completeness and diagonalization are explicit Gibbs-state requirements.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionThe selected field really is uniform or takes both sublattice signs.
- definitionThe positive-temperature, low-dimensional isotropic source scope.
- definition`C=S_+(k)` and `A=S_-(-k-K)` are the operators used in (8).
- definitionScalar inequality readouts are expectations of those exact operators.
- definitionThe source's forward and inverse spin and exchange Fourier transforms.
- definitionAll thermal and specialized operator hypotheses preceding equation (8).
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionEquation (10) and the elementary spin bound used after the mode sum.
- definitionBoth successive limits refer to one finite-volume magnetic family.
- definition
- definitionThe antiferromagnetic channel has a two-sublattice sign taking both values `+1` and `-1`, as in the source's `exp(i K R)` prescription.
- definitionThe mathematical preservation bridge from equation (11) to (12).
- definitionJournal p. 1134: the magnetic readout is the actual infinite-volume limit before h goes to zero.
- definitionThe two-dimensional small-field scaling stated in equation (1).
- definitionThe uniform channel has `K = 0` and no alternating sublattice sign.
- definition
- definitionIndependently assigned scalar readouts, deliberately lacking actual volume convergence.
- definition
- definitionThe old empty-list test misses the actual two-dimensional lattice origin.
- definition
- definitionThe source's summand is |R|^2 times the absolute exchange coupling.
- definitionSelected finite and limiting descriptions. Actual magnetization convergence is retained separately in ThermodynamicEquationTransferAt; description tags alone are not a thermodynamic-limit realization.
- definitionGibbs weights alone do not exclude equal-energy spectral pairs.
- definitionPositive normalization data do not establish the actual Boltzmann weight.
- definitionA named periodic spin box does not determine its Hamiltonian.
- definitionFourier labels alone do not select `C=S_+(k)` and `A=S_-(-k-K)`.
- definitionOne site already distinguishes a selected spin from its Fourier image.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionPairwise lattice displacement in the chosen Bravais coordinates.
- definitionSquared lattice displacement in the model's integer Bravais coordinates.
- definition
- definitionThe actual dot product in the source's complex Fourier phases.
- definitionThe magnetic order parameter witnesses a moved state of spin rotation.
- definition
- definition
- definitionThe exact paper-local premises retained by the Mermin-Wagner token.
- definitionThe one-spin Gibbs polarization, repeated as the per-spin readout of a noninteracting family. This limit control does not construct every finite lattice operator used in the complete Mermin-Wagner route.
- definition
- definitionA concrete one-site, one-state box used only for independent boundaries.
- definition
- definitionMatrix multiplication is essential: these operators do not commute.
- definitionA positive named interaction radius need not bound actual J(R) support.
- definition
- definitionCompatibility view of the isotropic argument's scope, not invalidity of a physical theory.
- definitionExplicit spin-half matrices witness that the operator carrier is physical.
- definition
- definition
- definitionMermin-Wagner's shared context selects the thermodynamic spin system, the spin-rotation symmetry, one magnetic channel, and the post-thermodynamic positive small-field limit. The nonmagnetic order readout is retained.
- definitionPaper-local interpretation of the shared route in the selected spin model.
- definitionJournal p. 1134 defines both magnetic channels through a positive-field limit of the already infinite-volume magnetization. The reversed order is outside this source-certified procedure; this does not claim that it cannot exist.
- definitionA nonnegative reported moment need not equal the actual weighted sum.
- definitionThe physical origin has one zero coordinate in every spatial dimension.
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- definitionInner limits need only hold eventually along the outer physical approach.
- definition
- definition
- definition
- definition
- definitionThe paper can state a candidate result in an admissible order without having proved that its limiting calculation actually attains that result.
- definitionAn established ordered value retains the whole selected physical setup, the particular value, and an independently supplied source-level realization.
- definitionA meaningful ordered comparison has two genuinely distinct operations.
- 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
- definition
- definition
- definition
- definitionUniform finite-volume control does not itself prove that the property is closed under the selected thermodynamic limit. That closure is this bridge.
- definition
- 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
- 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
- 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
- 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
- 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
- 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
- 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
- constructor
- definition
- checked statement
- 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
- 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
- constructor
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- 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
- 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
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- definition
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- inductive
- definition
- instance
- definition
- definition
- definition
- definition
- constructor
- definition
- checked statement
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- inductive
- definition
- instance
- constructor
- definition
- checked statement
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- definition
- structure
- definition
- instance
- definition
- definition
- checked statement
- definition
- definition
- definition
- definition
- checked statement
- checked statement
- constructor
- definition
- checked statement
- checked statement
- definition
- checked statement
- definition
- definition
- definition
- checked statementThe certified Gibbs source atom supplies real normalized probabilities.
- checked statementThe certified average atom also retains Gibbs and spectral source physics.
- checked statementThe setup atom retains the physical origin and actual operator equations.
- recursor
- definition
- checked statement
- checked statement
- checked statementThe certified source-scope atom contains actual lattice-exchange physics.
- checked statement
- inductive
- definition
- instance
- 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
- definition
- definition
- definition
- checked statement
- recursor
- definition
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- constructor
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- definition
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- checked statement
- checked statement
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- instance
- definition
- definition
- definition
- definition
- definition
- definition
- definition
- checked statement
- definition
- definition
- checked statement
- checked statement
- definition
- checked statement
- checked statement
- checked statement
- 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 statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA parameter/readout control, not a constructed anisotropic Heisenberg ensemble.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementA legitimate finite box need not carry the actual spin-S matrix algebra.
- checked statementThe finite calculation cannot be applied without its actual inputs.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementThe paper-local Bogoliubov and ordered-limit chain realizes a source-sensitive structural explanation of the shared infrared no-order phenomenon.
- checked statementThe exact two-channel conclusion stated in the abstract and on p. 1133.
- checked statement
- checked statementUniqueness of the post-thermodynamic small-field limit removes the order.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementAn actual one-state Gibbs ensemble is nonvacuously inhabited.
- checked statement
- checked statement
- checked statementThe operator-average source atom carries the original Gibbs construction.
- checked statement
- checked statementEvery certified ordering setup retains the actual operator construction.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementChoosing the correct ladder operators does not calculate their averages.
- checked statementThe corrected squared numerator and computed denominator give (8).
- checked statement
- checked statement
- checked statementThe source chain first establishes the infinite-volume inequality and the appropriate dimension-specific infrared bounds, then obtains suppression.
- checked statementThe completed source route retains both the zero physical order parameter and the certified infinite-volume-then-zero-field limit that produced it.
- checked statementA Hermitian observable has a real thermal average in the selected Gibbs state, including when the energy basis is not the fixed spin basis.
- checked statementReconstruct the actual Hamiltonian, not a second independently assigned diagonal matrix in the fixed spin coordinates.
- checked statement
- checked statementThe same thermal expectation is a fixed-coordinate trace. The density matrix uses the selected eigenvectors as well as the Boltzmann weights.
- checked statement
- checked statementThe stated Boltzmann weights are genuinely positive and normalized.
- checked statement
- checked statement
- checked statement
- checked statementThe magnetic theorem retains genuine support control or an actual sum.
- checked statement
- checked statementAll three Cartesian spin averages are real; the ladder operators are instead related by adjunction and need not themselves be Hermitian.
- checked statementThe adjoints needed for the Bogoliubov substitution are consequences of Cartesian Hermiticity and the actual ladder formulas, not additional readouts.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statementBoth no-order conclusions retain the source's genuine exchange condition.
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
- checked statement
Axioms and trust boundaries
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
- axiom / trust boundary
Constructors, projections, and other meaning dependencies
- 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
- 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
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- recursor
- constructor
- constructor
- constructor
- constructor
- recursor
- constructor
- constructor
- recursor
- constructor
- constructor
- constructor
- 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
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
- external type boundary
Physical definitions and checked implications
OrderChannel (inductive)
Uniform magnetization and the alternating two-sublattice order channel.
Description (inductive)
A finite periodic spin box or its selected infinite-volume description.
Regime (inductive)
Regimes explicitly separated by the source's scope discussion.
Model (structure)
The physical readouts used in the letter. `exchangeSecondMoment` represents the sum of `R^2 |J(R)|`; the separate convergence relation retains the footnote's weakening of finite range. Mode readouts are indexed by a real wave-number magnitude, while `finiteInfraredSum` and `infiniteInfraredIntegral` retain the Brillouin-zone sum and integral.
AdmissibleExchange (def)
Finite range or the weaker second-moment condition controls the exchange. In either branch the reported moment must equal its actual weighted sum.
AxialAnisotropicException (def)
The source's explicitly stated anisotropic exception: `J_y = J_z != J_x`, with an aligning field in the `z` direction. Its calculation is separate from the isotropic theorem.
SourceScope (def)
The positive-temperature, low-dimensional isotropic source scope.
MagneticSourceScopeWithoutIsotropy (def)
The common positive-temperature and exchange scope before isotropy.
AxialAnisotropicSourceScope (def)
The source's qualified anisotropic aligning-field scope.
UniformOrderingChannelAt (def)
The uniform channel has `K = 0` and no alternating sublattice sign.
StaggeredOrderingChannelAt (def)
The antiferromagnetic channel has a two-sublattice sign taking both values `+1` and `-1`, as in the source's `exp(i K R)` prescription.
BravaisPeriodicExchangeSetupAt (def)
Periodic Bravais boxes with `J(0) = 0` and even exchange `J(-R) = J(R)`.
FirstBrillouinZoneAt (def)
Every momentum used by the source calculation lies in the first zone.
OperatorAveragesExistAt (def)
Existence and positivity of the three thermal operator readouts.
BogoliubovInequalityAt (def)
Equation (3), written without division or an implicit existence claim.
BogoliubovCalculationAt (def)
The source's inner-product and Schwarz-inequality derivation of (3).
FiniteModeBogoliubovBoundAt (def)
Equation (8) after choosing `C = S_+(k)` and `A = S_-(-k-K)`. The strictly positive denominator is retained explicitly; the product form avoids a totalized inverse at a zero denominator.
DenominatorUpperBoundAt (def)
The domain-inclusive nonstrict upper estimate underlying corrected (9), retaining zero-mode equality rather than extending the printed strict sign to that boundary.
SpinSumRuleAt (def)
Equation (10) and the elementary spin bound used after the mode sum.
EquationElevenAt (def)
Equation (11), retaining the finite Brillouin-zone infrared sum.
EquationTwelveAt (def)
Equation (12), with the spin-density factor `1/rho` made explicit.
InfraredScale (def)
The source's scale `omega = S(S+1) k_0^2 sum_R R^2 |J(R)|`.
EquationThirteenAt (def)
Equation (13) on its positive-omega, nonzero-field domain. Multiplying out a denominator does not extend the ratio formula to zero exchange.
EquationFourteenAt (def)
Corrected equation (14) uses the positive square-root infrared ratio. The original erratum on p. 1307 and the nondegenerate domain are explicit.
TwoDimensionalSmallFieldBoundAt (def)
The two-dimensional small-field scaling stated in equation (1).
OneDimensionalSmallFieldBoundAt (def)
The corrected one-dimensional scaling in (2), with a common coefficient on a positive small-field neighborhood.
finiteVolumeContext (def)
Finite-family and uniform-bound bookkeeping. Actual magnetization convergence is retained separately in the thermodynamic-transfer contract.
FiniteVolumeBogoliubovPackageAt (def)
The finite-box package needed for the thermodynamic passage. It retains the finite mode bound, denominator bound, spin sum rule, and the uniform equation-(11) family as distinct inputs.
FiniteModeInputsAt (def)
All finite mode, denominator, and spin-sum inputs used before (11).
FiniteEstimateCalculationAt (def)
The finite calculation from (3), (8)-(10) to the uniform estimate (11).
ThermodynamicEquationTransferAt (def)
Actual convergence of finite magnetizations to the thermodynamic readout, together with the preservation bridge from equation (11) to (12).
LowDimensionalInfraredCalculationAt (def)
The scoped calculation supplies the dimension-specific estimates, not their vanishing limit. Lean derives that limit at fixed positive temperature and then identifies spontaneous magnetization through the actual successive limits.
SpontaneousLimitAt (def)
The selected spontaneous magnetization is obtained by actual volume-then-field limits of one finite-volume family.
AxialAnisotropicNoOrderCalculationAt (def)
The separate calculation asserted for the source's axial exception.
CrystallineComparisonCalculationAt (def)
The similar, but distinct, crystalline no-order argument asserted on p. 1135.
ClassicalSpinComparisonCalculationAt (def)
The separate purely classical-spin argument asserted in the source.
finite_estimate_inputs_establish_bogoliubov_package (theorem)
The finite calculation cannot be applied without its actual inputs.
source_chain_establishes_infrared_bounds_and_suppression (theorem)
The source chain first establishes the infinite-volume inequality and the appropriate dimension-specific infrared bounds, then obtains suppression.
no_magnetic_order_from_source_chain (theorem)
Uniqueness of the post-thermodynamic small-field limit removes the order.
neither_ferromagnetic_nor_antiferromagnetic (theorem)
The exact two-channel conclusion stated in the abstract and on p. 1133.
sourceValidity (def)
The compatibility interface records a restricted argument scope, not invalidity of an underlying theory outside that scope.
isotropicNoOrderArgument (def)
A shared scoped argument with the actual isotropic, finite-volume, thermodynamic, infrared, and spontaneous-limit premises. Its physical conclusion is zero magnetic order; the_isotropic_argument_is_sound uses the complete checked source chain.
Outside an argument's scope is not a refutation
On p. 1135, the source's axial exception has J_y = J_z != J_x and a z-aligning field. Its separate calculation can establish the same no-order conclusion despite failure of the isotropic premises. the_axial_exception_can_establish_the_conclusion_outside_isotropic_premises checks that implication; an_axial_zero_order_readout_is_outside_the_isotropic_argument supplies the inhabited parameter/readout control used in the twenty-third fidelity boundary. This is not a complete anisotropic Heisenberg ensemble. Failed sufficient premises alone establish neither magnetic order nor inconclusiveness over a class of systems.
magneticBreakingContext (def)
The magnetic order parameter witnesses a moved state of spin rotation.
toInfraredOrderSuppressionContext (def)
Mermin-Wagner's shared context selects the thermodynamic spin system, the spin-rotation symmetry, one magnetic channel, and the post-thermodynamic positive small-field limit. The nonmagnetic order readout is retained.
toInfraredOrderSuppressionInterpretation (def)
Paper-local interpretation of the shared route in the selected spin model.
Actual limits and source certification have different roles
The source defines magnetization in the infinite-volume system before sending the positive field to zero. The Lean realization now connects those two stages to the same finite-volume readout; an assigned thermodynamic value alone cannot supply the connection.
m_infinity(h) -> m_sp as h->0+.
Both approach filters are nontrivial; the inner limit uses the same finite-volume magnetization.
p_+(b)>0; p_-(b)>0; p_+(b)+p_-(b)=1; s(b)=p_+(b)-p_-(b).
m_N(h)=s((N+1)h); m_N(0)=0.
lim_(h->0+) lim_(N->infinity) m_N(h)=1; lim_(N->infinity) lim_(h->0+) m_N(h)=0.
This two-phase control is not a short-range Heisenberg realization of the theorem's full hypotheses.
Both actual iterated limits equal 0.
The source certifies volume before field, not the reverse; lack of certification does not imply noncommutation.
The finite-volume limit is 0, so this assignment does not realize the claimed thermodynamic limit.
Corrected estimates, actual response, and logical boundaries
The original article and the author's original erratum are separate archived sources. The infrared calculation, small-field deduction, and susceptibility response have separate formal roles. Neither a named susceptibility flag nor the desired zero-field limit is an input to the estimate-to-suppression deduction.
The corrections are anchored to Physical Review Letters 17, 1307 (1966). The logical consequences below do not reconstruct every microscopic finite-spin Hamiltonian or prove the imported spin-sum and integral calculations.
d=1: |m(h)|^3 T^2 < C^3 |h|; d=2: |m(h)| sqrt(T) sqrt(|log |h||) < C.
Each bound implies m(h)->0 as h->0+; this limit is derived, not part of the infrared-calculation input.
Equation (2) uses the author's erratum, PRL 17, 1307; uniformity across different temperatures is not asserted.
dimension_specific_bounds_force_zero_field_limit supplies the new dependency between the two source claims. The coefficient cannot vary independently with the field.For h>0, chi_c(h)=m_c'(h)=1/(8 sqrt(h)(1+sqrt(h))^2).
Both corrected bounds hold at T=1, with r=C=1; m_c(h)->0 while chi_c(h)->infinity.
Susceptibility requires an actual derivative eventually near zero; this response is not a microscopic Heisenberg construction.
HasDerivAt. Uniqueness of the actual derivative excludes a simultaneous finite susceptibility limit, without reading a totalized derivative at the endpoint.At T=0 both estimate forms hold but the positive-field limit is 1/4.
The uncorrected extra-field form |h m(h)|^3 T^2 < C^3 |h| permits this nonzero limit at T=1.
Allowing a different coefficient for every field does not supply one common two-dimensional bound.
The denominator estimate uses <=, retaining zero-mode equality. Ratio formulas (13)-(14) require omega>0, h!=0, and m(h)!=0.
The corrected arctangent argument is sqrt(omega/|h m(h)|), not its reciprocal.
Zero-exchange normalized spin-half readouts have m(h)>0 at positive h and m(h)->0; the positive-omega ratio formulas do not apply there.
U†H(channel,h)U=diag(E_i), A_E=U†AU.
w_i=exp(-beta E_i)/Z; <A>=sum_i w_i (A_E)_{ii}=Tr[A U diag(w_i) U†].
(A,B)=sum_{E_i != E_j} conjugate((A_E)_{ij})(B_E)_{ij}(w_i-w_j)/(E_j-E_i).
S_+=S_x+iS_y, S_-=S_x-iS_y imply S_+†=S_- and S_-†=S_+.
A†=A implies Im<A>=0 in the selected Gibbs state.
Diagnostic D=diag(2,1): S'_a=D S_a D-1 retains commutators and the Casimir,
but psi=(3/5,4i/5) has norm squared 1 and <psi|S'_x|psi>=9i/25.
With transverseSpinWeight=anticommutatorMean and D>0, the Bogoliubov inequality gives (1/2) transverseSpinWeight D >= N^2 k_B T m_N^2.
These are readouts of the selected thermal operators; the complete finite spin-sum and integral calculations remain explicit inputs.
selected_readouts_and_bogoliubov_derive_the_finite_mode_bound uses the corrected squared numerator and the same magnetization and denominator throughout.At T=3 both corrected estimates hold with r=C=1, and each library theorem independently derives m(h)->0.
For h>0 the actual derivative is 1/(3(1+h)^2), tending to 1/3; divergent susceptibility is excluded.
The client uses paper-local public lemmas without production diagnostic witnesses; no new framework or microscopic realization is claimed.
scripts/CheckIndependentReuse.lean. Four audited public-API dependencies test the two limit deductions, the logarithmic weight, and derivative-limit incompatibility.Source-ordered inference routes
magneticNoOrder
Logical kind: bogoliubovInfraredSuppression.
Required predecessor routes: none.
Ordered inference steps: stateSourceScope, selectOrderingChannels, stateOperatorAverages, supplyBogoliubovCalculation, deriveBogoliubovInequality, supplyFiniteModeInputs, supplyFiniteEstimateCalculation, deriveFiniteBogoliubovPackage, supplyThermodynamicTransfer, deriveInfiniteVolumeEquation, supplyInfraredCalculation, deriveDimensionSpecificBounds, deriveMagneticOrderSuppression, stateSpontaneousLimit, deriveFerromagneticAbsence, deriveAntiferromagneticAbsence, deriveBothMagneticOrdersAbsent.
Exported conclusions: dimensionSpecificBounds, ferromagneticAbsence, antiferromagneticAbsence, bothMagneticOrdersAbsent.
scopeQualifications
Logical kind: sourceScopeAssessment.
Required predecessor routes: none.
Ordered inference steps: stateSecondMomentQualification, stateAxialAnisotropicScope, supplyAxialAnisotropicCalculation, deriveAxialMagneticOrderAbsence, stateOtherOrderAndSusceptibilityCaveat, supplyCrystallineComparisonCalculation, supplyClassicalSpinComparisonCalculation, retainQualifiedScopeConclusion.
Exported conclusions: secondMomentQualification, axialMagneticOrderAbsent, otherOrderAndSusceptibilityCaveat, crystallineComparisonCalculation, classicalSpinComparisonCalculation, qualifiedScopeConclusion.
Exhaustive Lean semantic ledger
Checked paper-local theorems: admissible_exchange_has_the_actual_reported_moment, an_actual_exchange_moment_is_nonnegative, source_scope_retains_physical_exchange_support_or_convergence, positive_fields_are_eventually_below_any_fixed_radius, positive_small_fields_are_eventually_in_the_source_range, the_one_dimensional_bound_forces_zero_magnetization, the_two_dimensional_logarithmic_weight_diverges, the_two_dimensional_bound_forces_zero_magnetization, the_sqrt_log_weight_is_bounded_after_the_field_factor, divergent_susceptibility_excludes_a_finite_susceptibility_limit, source_spin_ladders_are_mutual_adjoints, source_gibbs_weights_are_positive_and_normalized, source_gibbs_energy_coordinates_reconstruct_the_hamiltonian, source_gibbs_thermal_average_is_the_fixed_coordinate_trace, source_gibbs_average_of_hermitian_observable_is_real, source_spin_components_have_real_thermal_averages, ordering_setup_retains_heisenberg_hamiltonian_spin_algebra_and_fourier, operator_averages_retain_gibbs_spectral_inner_product_and_selected_readouts, selected_readouts_and_bogoliubov_derive_the_finite_mode_bound, dimension_specific_bounds_force_zero_field_limit, finite_volume_and_small_field_limits_define_one_magnetic_result, source_scope_and_limit_establish_ordered_magnetization_value, ordered_magnetization_value_exposes_source_limit, an_established_magnetic_order_retains_the_actual_finite_volume_family, source_ordered_magnetization_limit_does_not_certify_reverse, spontaneous_limit_realizes_selected_volume_then_field_order, finite_second_moment_is_an_admissible_exchange_scope, axial_anisotropic_calculation_establishes_qualified_no_order, equation_twelve_from_finite_volume_route, finite_estimate_inputs_establish_bogoliubov_package, source_chain_establishes_infrared_bounds_and_suppression, no_magnetic_order_from_source_chain, source_chain_establishes_ordered_magnetic_absence, neither_ferromagnetic_nor_antiferromagnetic, two_channel_no_order_retains_physical_exchange_assumption, the_isotropic_argument_is_sound, the_axial_exception_can_establish_the_conclusion_outside_isotropic_premises, source_result_is_regime_restricted, spontaneous_magnetic_breaking_implies_nonzero_order, source_chain_blocks_spontaneous_magnetic_breaking, infrared_order_suppression_model_retains_paper_semantics, magnetic_scope_and_ordering_make_shared_infrared_setup, infrared_bounds_realize_shared_magnetic_expectation_suppression, spontaneous_limit_realizes_shared_no_breaking_bridge, mermin_wagner_inputs_make_shared_infrared_route_applicable, mermin_wagner_source_inputs_realize_source_structural_infrared_order_suppression_explanation, mermin_wagner_route_establishes_shared_infrared_no_order, mermin_wagner_route_exhibits_nonvacuous_infrared_order_suppression, magnetic_infrared_model_inputs_establish_theory_model_grounding, mermin_wagner_route_establishes_grounded_shared_infrared_no_order, grounded_mermin_wagner_infrared_no_order_transfers_every_shared_claim, the_two_gibbs_weights_are_positive_and_normalized, polarization_is_a_genuine_bounded_gibbs_expectation, polarization_has_the_stable_exponential_form, polarization_is_continuous, zero_bias_has_zero_polarization, an_unbounded_positive_bias_selects_the_up_orientation, every_finite_two_phase_system_has_zero_field_limit_zero, a_fixed_positive_field_selects_a_phase_at_infinite_volume, the_actual_two_phase_family_has_distinct_iterated_magnetizations, critical_response_at_zero, critical_response_magnitude, critical_response_is_bounded, critical_response_at_positive_field, critical_response_is_odd, critical_response_is_at_most_the_sqrt_scale, critical_response_satisfies_the_one_dimensional_bound, critical_response_satisfies_the_two_dimensional_bound, critical_response_has_zero_positive_field_limit, the_positive_field_critical_derivative_is_computed, the_actual_critical_susceptibility_diverges, the_critical_response_has_an_actual_divergent_derivative, both_source_bounds_and_zero_order_allow_infinite_susceptibility, ordered_response_magnitude_at_nonzero_field, ordered_response_at_positive_field, ordered_response_has_a_nonzero_positive_field_limit, ordered_response_does_not_have_zero_positive_field_limit, zero_temperature_bounds_do_not_suppress_the_ordered_response, the_printed_extra_field_allows_a_nonzero_ordered_response, field_dependent_coefficients_do_not_supply_the_source_bound, both_corrected_bounds_allow_an_actual_infinite_susceptibility, empty_list_origin_does_not_exclude_physical_on_site_exchange, one_site_source_box_retains_actual_lattice_and_reciprocal_data, spin_half_matrices_realize_noncommutative_physical_spin_algebra, finite_reciprocal_box_does_not_supply_spin_fourier_transform, finite_bravais_box_does_not_supply_noncommutative_spin_algebra, periodic_spin_box_does_not_supply_heisenberg_hamiltonian, positive_partition_function_does_not_supply_gibbs_weights, one_state_source_gibbs_ensemble_is_nonvacuous, reciprocal_mode_does_not_supply_selected_ladder_operators, selected_ladder_operators_do_not_supply_thermal_scalar_readouts, gibbs_ensemble_does_not_supply_degenerate_pair_exclusion, finite_zero_magnetization_does_not_imply_thermodynamic_no_order, independently_assigned_finite_and_infinite_values_do_not_realize_a_thermodynamic_limit, the_noninteracting_control_uses_normalized_spin_half_weights, the_noninteracting_control_has_an_actual_thermodynamic_family, the_noninteracting_control_has_actual_zero_field_suppression, the_noninteracting_control_has_both_actual_magnetic_limit_orders, source_selected_magnetic_limit_does_not_certify_reversed_order, no_magnetic_order_does_not_exclude_other_order_or_susceptibility, magnetic_no_order_does_not_imply_no_other_order_or_finite_susceptibility, finite_second_moment_without_isotropy_does_not_forbid_magnetic_order, positive_range_label_does_not_bound_exchange_couplings, nonnegative_reported_moment_does_not_supply_actual_exchange_sum, axial_exception_is_distinct_from_isotropic_and_generic_anisotropy, an_axial_zero_order_readout_is_outside_the_isotropic_argument, finite_exchange_support_does_not_repair_a_wrong_reported_moment, the_noninteracting_positive_field_response_is_positive, zero_exchange_does_not_force_zero_magnetization_at_nonzero_field.
Checked route-realization theorems: spontaneous_atom_retains_common_finite_volume_and_field_limits, source_scope_atom_retains_physical_exchange_support_or_convergence, ordering_atom_retains_dimension_correct_origin_and_source_operators, operator_average_atom_retains_source_gibbs_and_bogoliubov_construction, operator_average_atom_proves_positive_normalized_boltzmann_weights, every_source_claim_has_semantics, magnetic_no_order_route_is_semantically_realized, scope_qualifications_route_is_semantically_realized, route_semantic_realization_is_exhaustive.
Checked source-map theorems: argument_wellFormed, argument_auditable, routes_wellFormed, routes_have_exact_predecessor_graph, source_calculations_and_scope_inputs_are_premise_free, source_qualification_inputs_are_premise_free, result_steps_apply_exact_physical_predecessors, scope_qualifications_form_an_independent_route.
Semantic atoms: sourceScopeHolds, orderingChannelsAreSelected, operatorAveragesExist, bogoliubovCalculationHolds, bogoliubovInequalityHolds, finiteModeInputsHold, finiteEstimateCalculationHolds, finiteBogoliubovPackageHolds, thermodynamicTransferHolds, infiniteVolumeEquationHolds, infraredCalculationHolds, dimensionSpecificBoundsHold, magneticOrderExpectationIsSuppressed, spontaneousLimitHolds, ferromagneticOrderIsAbsent, antiferromagneticOrderIsAbsent, bothMagneticOrdersAreAbsent, secondMomentQualificationHolds, axialAnisotropicScopeHolds, axialAnisotropicCalculationHolds, axialMagneticOrderIsAbsent, otherOrderAndSusceptibilityRemainPossible, crystallineComparisonCalculationHolds, classicalSpinComparisonCalculationHolds, qualifiedScopeConclusionHolds.
Source claims: sourceScope, orderingChannels, operatorAverages, bogoliubovCalculation, bogoliubovInequality, finiteModeInputs, finiteEstimateCalculation, finiteBogoliubovPackage, thermodynamicTransfer, infiniteVolumeEquation, infraredCalculation, dimensionSpecificBounds, magneticOrderSuppression, spontaneousLimit, ferromagneticAbsence, antiferromagneticAbsence, bothMagneticOrdersAbsent, secondMomentQualification, axialAnisotropicScope, axialAnisotropicCalculation, axialMagneticOrderAbsent, otherOrderAndSusceptibilityCaveat, crystallineComparisonCalculation, classicalSpinComparisonCalculation, qualifiedScopeConclusion.
Source-ordered inference steps: stateSourceScope, selectOrderingChannels, stateOperatorAverages, supplyBogoliubovCalculation, deriveBogoliubovInequality, supplyFiniteModeInputs, supplyFiniteEstimateCalculation, deriveFiniteBogoliubovPackage, supplyThermodynamicTransfer, deriveInfiniteVolumeEquation, supplyInfraredCalculation, deriveDimensionSpecificBounds, deriveMagneticOrderSuppression, stateSpontaneousLimit, deriveFerromagneticAbsence, deriveAntiferromagneticAbsence, deriveBothMagneticOrdersAbsent, stateSecondMomentQualification, stateAxialAnisotropicScope, supplyAxialAnisotropicCalculation, deriveAxialMagneticOrderAbsence, stateOtherOrderAndSusceptibilityCaveat, supplyCrystallineComparisonCalculation, supplyClassicalSpinComparisonCalculation, retainQualifiedScopeConclusion.
Independent argument routes: magneticNoOrder, scopeQualifications.
Argument-route classifications: bogoliubovInfraredSuppression, sourceScopeAssessment.
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.
magneticNoOrder
Logical kind: bogoliubovInfraredSuppression.
Required predecessor routes: none.
Ordered inference steps: stateSourceScope, selectOrderingChannels, stateOperatorAverages, supplyBogoliubovCalculation, deriveBogoliubovInequality, supplyFiniteModeInputs, supplyFiniteEstimateCalculation, deriveFiniteBogoliubovPackage, supplyThermodynamicTransfer, deriveInfiniteVolumeEquation, supplyInfraredCalculation, deriveDimensionSpecificBounds, deriveMagneticOrderSuppression, stateSpontaneousLimit, deriveFerromagneticAbsence, deriveAntiferromagneticAbsence, deriveBothMagneticOrdersAbsent.
Exported conclusions: dimensionSpecificBounds, ferromagneticAbsence, antiferromagneticAbsence, bothMagneticOrdersAbsent.
scopeQualifications
Logical kind: sourceScopeAssessment.
Required predecessor routes: none.
Ordered inference steps: stateSecondMomentQualification, stateAxialAnisotropicScope, supplyAxialAnisotropicCalculation, deriveAxialMagneticOrderAbsence, stateOtherOrderAndSusceptibilityCaveat, supplyCrystallineComparisonCalculation, supplyClassicalSpinComparisonCalculation, retainQualifiedScopeConclusion.
Exported conclusions: secondMomentQualification, axialMagneticOrderAbsent, otherOrderAndSusceptibilityCaveat, crystallineComparisonCalculation, classicalSpinComparisonCalculation, qualifiedScopeConclusion.