QIQTH.KGStressConservation

← all sections · ← HregExplicitKG · KMSCorrelation →

KGStressConservation · entries 448–468 of 1000

Definition 448 (kgKinetic).  source ↗

The KG kinetic (0,2) tensor K_{ab} = ∂_a φ · ∂_b φ.

Used by div02_kgStress_eq, covDeriv02_kgKinetic, div02_kgKinetic_eq, div02_kgStress_conserved, div02_kgStress_conserved_of_KG, kg_conserv, kg_conserv_of_contDiff.

Definition 449 (kgLagr).  source ↗

The KG Lagrangian scalar L = g^{αβ} ∂_α φ ∂_β φ + m² φ² (the combination appearing inside the trace term of the stress tensor; the sign makes ∇^μ T_{μν} = 0 close against the equation of motion □φ = m²φ).

Used by kgLagr_contDiff, kgStress_contDiff, kgStress, div02_kgStress_eq, div02_kgStress_conserved, div02_kgStress_conserved_of_KG, kg_conserv, kg_conserv_of_contDiff, and 3 more.

Definition 450 (kgStress).  source ↗

The Klein–Gordon stress tensor T_{ab} = ∂_a φ ∂_b φ − ½ g_{ab} L.

Used by kgStress_contDiff, hreg_kg, div02_kgStress_eq, div02_kgStress_conserved, div02_kgStress_conserved_of_KG, kg_conserv, kg_conserv_of_contDiff, qiqt_gr_freefield_complete, and 12 more.

Lemma 451 (div02_kgStress_eq).  source ↗

Conservation SPLIT. The covariant divergence of the KG stress tensor reduces to the kinetic divergence minus half the Lagrangian gradient: ∇^μ T_{μν} = ∇^μ K_{μν} − ½ ∂_ν L. The scalar/metric term ½ g_{μν} L is handled by metric compatibility (div02_scalar_metric, the same mechanism that makes Λ·g covariantly constant); what remains — the kinetic identity ∇^μ K_{μν} = ½ ∂_ν L — is the Klein–Gordon equation of motion in disguise (the next brick). This is the first step of discharging the conserv input of the free-field QIQT→GR surface.

Proof. By pd_const_mul, mul, div02_add, div02_scalar_metric. $\square$

Used by div02_kgStress_conserved.

Definition 452 (kgHess).  source ↗

The covariant Hessian of the scalar φ: (∇∇φ)_{ρμ} = ∂_ρ ∂_μ φ − Γ^σ_{ρμ} ∂_σ φ (the covariant derivative of the gradient covector ∂φ). It is symmetric in ρ μ (torsion-free connection), which the kinetic identity will use.

Used by covDeriv02_kgKinetic, boxField, div02_kgKinetic_eq, div02_kgStress_conserved, hHessGrad_eq.

Lemma 453 (covDeriv02_kgKinetic).  source ↗

Leibniz/product rule for the kinetic tensor. The covariant derivative of K_{μν} = ∂_μφ ∂_νφ factors through the covariant Hessian: (∇_ρ K)_{μν} = (∇∇φ)_{ρμ} ∂_νφ + ∂_μφ (∇∇φ)_{ρν}. Each Christoffel term in covDeriv02 regroups (by Finset.sum_mul/Finset.mul_sum) into exactly one of the two Hessians, leaving the partial-derivative Leibniz term (pd_mul). This is the second brick of the conserv discharge: contracting it with g^{μρ} and using □φ = m²φ + Hessian symmetry will give ∇^μ K_{μν} = ½ ∂_ν L, closing conservation via div02_kgStress_eq.

Proof. By pd_mul, christoffel. $\square$

Used by div02_kgKinetic_eq.

Definition 454 (boxField).  source ↗

The d’Alembertian □φ = g^{μρ} (∇∇φ)_{ρμ} (the covariant Laplace–Beltrami of the scalar φ).

Used by div02_kgKinetic_eq, div02_kgStress_conserved, div02_kgStress_conserved_of_KG, kg_conserv, kg_conserv_of_contDiff, qiqt_gr_freefield_complete, qiqt_gr_freefield_complete_covCong, qiqt_gr_explicit_kg, and 9 more.

Lemma 455 (div02_kgKinetic_eq).  source ↗

Kinetic divergence in Hessian form. Contracting the Leibniz rule (covDeriv02_kgKinetic) with the inverse metric splits the kinetic divergence into the □φ piece and a Hessian-gradient piece: ∇^μ K_{μν} = (□φ) ∂_νφ + g^{μρ} ∂_μφ (∇∇φ)_{ρν}. The first piece is exactly where the Klein–Gordon equation □φ = m²φ enters; the second is ½ ∂_ν of the kinetic part of L (by Hessian symmetry + metric compatibility) — the two facts that, with div02_kgStress_eq, close ∇^μ T_{μν} = 0. This is the third brick of the conserv discharge.

Proof. By covDeriv02, covDeriv02_kgKinetic. $\square$

Used by div02_kgStress_conserved.

Lemma 456 (div02_kgStress_conserved).  source ↗

KG STRESS-TENSOR CONSERVATION (final assembly), conditional on the two physical/geometric facts. For the explicit Klein–Gordon field, ∇^μ T_{μν} = 0 follows from exactly: * hKG — the equation of motion □φ = m²φ (boxField φ = m²·φ); and * hHessGrad — the Hessian-gradient identity g^{μρ} ∂_μφ (∇∇φ)_{ρν} = ½ ∂_ν(g^{αβ}∂_αφ ∂_βφ), the one place metric compatibility (metric_compat, ∇g = 0) + Hessian symmetry (kgHess_symm) enter. Given these, the split (div02_kgStress_eq) + contraction (div02_kgKinetic_eq) collapse algebraically: ∇^μ T_{μν} = (□φ − m²φ) ∂_νφ = 0. …

Proof. By pd_add, pd_const_mul, mul, pd_mul, div02_kgStress_eq, div02_kgKinetic_eq. $\square$

Used by div02_kgStress_conserved_of_KG.

Lemma 457 (pd_metric_inv_identity).  source ↗

Differentiated inverse relation (∂(g·gi = δ)): for a pointwise inverse metric, differentiating the identity ∑_α g_{μα} gi^{αβ} = δ_μ^β gives ∑_α ∂_ν(g_{μα}) gi^{αβ} + ∑_α g_{μα} ∂_ν(gi^{αβ}) = 0. This is the first step toward inverse-metric compatibility ∇gi = 0 (which then follows by contracting with gi^{λμ} and substituting metric_compat for ∂g), the one geometric fact still needed for hHessGrad.

Proof. By pd_const, mul, pd_sum, pd_mul. $\square$

Used by pd_gi_eq.

Lemma 458 (gi_g_delta).  source ↗

The inverse metric is a left inverse too ∑_μ gi^{aμ} g_{μb} = δ^a_b (from the right-inverse hinv plus symmetry of g and gi). The δ used to extract ∂gi in the inverse-metric compatibility.

Proof. Immediate from the definitions. $\square$

Used by pd_gi_eq.

Lemma 459 (pd_g_eq).  source ↗

∂g in terms of the connection ∂_ν g_{μα} = ∑σ Γ^σ_{νμ} g_{σα} + ∑σ Γ^σ_{να} g_{μσ} — the explicit content of metric compatibility ∇g = 0 (metric_compat), unpacked from the covDeriv02 definition.

Proof. By covDeriv02, metric_compat. $\square$

Used by pd_gi_eq.

Lemma 460 (pd_gi_eq).  source ↗

INVERSE-METRIC COMPATIBILITY ∇gi = 0 (upper-index companion of metric_compat): ∂_ν gi^{λβ} = −∑σ Γ^λ_{νσ} gi^{σβ} − ∑σ Γ^β_{νσ} gi^{σλ}. Contract the differentiated inverse relation (pd_metric_inv_identity) with gi^{λμ}, extract ∂gi^{λβ} via the δ-identity gi_g_delta, substitute pd_g_eq for ∂g, and collapse the two double sums by the δ-contractions ∑α g_{σα}gi^{αβ} = δ_σ^β (hinv) and ∑μ gi^{λμ}g_{μσ} = δ^λ_σ (gi_g_delta). The last purely-geometric fact needed for hHessGrad.

Proof. By pd_metric_inv_identity, gi_g_delta, pd_g_eq. $\square$

Used by hHessGrad_eq.

Lemma 461 (pd_gradSq_eq).  source ↗

Product-rule expansion of the kinetic-scalar gradient ∂_ν(g^{αβ}∂_αφ∂_βφ). Differentiating term by term (pd_sum twice, pd_mul for the triple product) splits it into the ∂gi term plus the two ∂(∂φ) terms: ∂_ν(∑_{αβ} gi^{αβ}∂_αφ∂_βφ) = ∑_{αβ} ∂_ν(gi^{αβ})∂_αφ∂_βφ + ∑_{αβ} gi^{αβ}(∂_ν∂_αφ)∂_βφ + ∑_{αβ} gi^{αβ}∂_αφ(∂_ν∂_βφ). The first term meets pd_gi_eq (inverse-metric compatibility) and the last two meet the Hessian partials (pd_comm) in the final hHessGrad assembly.

Proof. By mul, PdiffAt_sum, pd_sum, pd_mul. $\square$

Used by hHessGrad_eq.

Lemma 462 (gradSq_cross_symm).  source ↗

The two cross gradient terms are equal R2 = R3: ∑_{αβ} gi^{αβ}(∂_ν∂_αφ)∂_βφ = ∑_{αβ} gi^{αβ}∂_αφ(∂_ν∂_βφ) (swap α ↔ β, gi-symmetry). Used to fold the two ∂(∂φ) terms of pd_gradSq_eq into one in hHessGrad.

Proof. Immediate from the definitions. $\square$

Used by hHessGrad_eq.

Lemma 463 (hessGrad_partial_eq).  source ↗

The Hessian-partial term equals R2 T1 = R2: ∑_{μρ} gi^{μρ}∂_μφ ∂_ρ∂_νφ = ∑_{αβ} gi^{αβ}(∂_ν∂_αφ)∂_βφ (commute the second derivative by pd_comm, then relabel μ↔β, ρ↔α via gi-symmetry). This is the partial-derivative half of the Hessian-gradient identity.

Proof. By pd_comm. $\square$

Used by hHessGrad_eq.

Lemma 464 (hHessGrad_eq).  source ↗

THE HESSIAN-GRADIENT IDENTITY hHessGrad — the last brick of the conserv discharge: g^{μρ}∂_μφ(∇∇φ)_{ρν} = ½ ∂_ν(g^{αβ}∂_αφ∂_βφ). Decompose the LHS = T1 − T2 (Hessian partials minus the Christoffel term) and the RHS = ½(R1+R2+R3) (pd_gradSq_eq). Then T1 = R2 (hessGrad_partial_eq), R2 = R3 (gradSq_cross_symm), and T2 = −½R1 (the Christoffel term: substitute pd_gi_eq into R1, giving R1 = −P − Q; Q = P by α↔β; P = T2 by a triple-sum reindex with christoffel_symm + gi-symmetry). Algebra then closes LHS = R2 − T2 = ½R1 + R2 = ½(R1+R2+R3) = RHS. Feeding this to div02_kgStress_conserved makes KG conservation ∇^μ T_{μν} = 0 unconditional (modulo only the matter equation of motion □φ = m²φ).

Proof. By christoffel, christoffel_symm, pd_gi_eq, pd_gradSq_eq, gradSq_cross_symm, hessGrad_partial_eq. $\square$

Used by div02_kgStress_conserved_of_KG.

Lemma 465 (div02_kgStress_conserved_of_KG).  source ↗

KLEIN–GORDON STRESS-TENSOR CONSERVATION, DISCHARGED — ∇^μ T_{μν} = 0 for the explicit free KG field, axiom-free, modulo ONLY the equation of motion. The Hessian-gradient identity (hHessGrad) is now supplied internally by hHessGrad_eq (built from inverse-metric compatibility pd_gi_eq + the gradient expansion + the symmetry lemmas), so the only remaining hypothesis is hKG : □φ = m²φ — the matter equation of motion, genuine physics. Everything geometric is machine-checked. This DISCHARGES the conserv input of the free-field QIQT→GR surface for the explicit Klein–Gordon stress tensor: conserv = a · (this) = 0.

Proof. By div02_kgStress_conserved, hHessGrad_eq. $\square$

Used by kg_conserv.

Lemma 466 (div02_const_smul).  source ↗

The raised divergence scales out a constant ∇^μ(a·X)_{μν} = a·∇^μ X_{μν} (the connection and metric are linear, a is constant — pd_const_mul + Finset.mul_sum). This is what carries the Einstein coupling a through the conservation law ∇·(a·T) = a·∇·T.

Proof. By pd, pd_const_mul, christoffel, covDeriv02. $\square$

Used by kg_conserv.

Lemma 467 (kg_conserv).  source ↗

THE conserv INPUT OF THE QIQT→GR DERIVATION, IN ITS EXACT FORM, DISCHARGED for the explicit KG field. ∇·(a·T) = 0 with T = kgStress (the free Klein–Gordon stress tensor): the Einstein-coupling constant a scales out (div02_const_smul) and the bare divergence vanishes (div02_kgStress_conserved_of_KG). This is exactly the conserv : ∀ x ν, div02 g gi (fun y a' b => a · T y a' b) ν x = 0 hypothesis consumed by WedgeKMSToGR/qiqt_gr_from_wedge_kms_complete — so the matter-conservation input is now a THEOREM for the explicit free scalar, modulo only the equation of motion □φ = m²φ.

Proof. By div02_kgStress_conserved_of_KG, div02_const_smul. $\square$

Used by kg_conserv_of_contDiff.

Lemma 468 (kg_conserv_of_contDiff).  source ↗

conserv FROM SMOOTHNESS ALONE — the clean drop-in. The same matter-conservation input ∇·(a·T) = 0 (T = kgStress), but with all the pointwise differentiability hypotheses derived from a single ContDiff assumption on the field φ and the metric components g, gi. This is the form actually convenient to plug into WedgeKMSToGR/qiqt_gr_from_wedge_kms_complete: given a smooth free scalar on a smooth (symmetric, invertible) metric satisfying the Klein–Gordon equation □φ = m²φ, the explicit stress tensor is covariantly conserved.

Proof. By pd, PdiffAt, PdiffAt_of_contDiff, mul, sub, add, PdiffAt_sum, PdiffAt_pd, kgKinetic, kgLagr, kg_conserv. $\square$

Used by qiqt_gr_explicit_kg, qiqt_gr_freefield.

← all sections · ← HregExplicitKG · KMSCorrelation →