Alphabeta Math
PostulateStatement: Literature-sourcedProof: Not applicablePipeline-generatedprecheck passjudge pass (gpt-6-luna)‡ sources checked 2026-11-04
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Type Iia Romans Massive Supergravity Action

Physical scope

Source-reported two-derivative massive IIA bosonic action in the field-strength, component, and normalization basis of Bergshoeff et al. (1996), Eq. (2.13). No conversion to the Graña democratic RR basis, Hamilton massless convention, kappa_0, or alpha-prime normalization is asserted.

Postulate

Adopt the source-reported two-derivative ten-dimensional massive IIA bosonic action in the field and normalization basis of Bergshoeff et al., Eq. (2.13). It is formulated on an oriented smooth ten-dimensional manifold M10, or an oriented smooth coordinate patch in such a manifold, with a smooth Lorentzian metric g of signature (−+⋯+), a smooth real dilaton σ:M10→R, and smooth real potentials A∈Ω1(M10), B∈Ω2(M10), and C∈Ω3(M10). Here g is the string-frame metric variable used in Eq. (2.13); no other metric frame or frame conversion is part of this item. “Two-derivative” means that the displayed density has no term with more than two spacetime derivatives of the fields. The Romans parameter m∈R is constant. For coordinates xM, M=0,…,9, use the source's form-component convention Q=QM1…MqdxM1∧⋯∧dxMq, with summation over all ordered indices and no factor 1/q!. For a q-form Q, define ∣Q∣2:=QM1…MqQM1…Mq/q!, raising indices with g; this is a signed Lorentzian contraction and need not be nonnegative. In the displayed scalar curvature, use ΓPMN=12gPQ(∂MgNQ+∂NgMQ−∂QgMN),RPQMN=∂MΓPNQ−∂NΓPMQ+ΓPMRΓRNQ−ΓPNRΓRMQ,RQN=RPQPN,R=gQNRQN. Set H=3 dB,F=2 dA+mB,G=4 dC+24 A∧dB+6m B∧B. The source-basis string-frame Lagrangian density is L=−g{e−2σ[R+4∣dσ∣2−13∣H∣2]−∣F∣2−112∣G∣2−12m2}+19ϵ[dC∧dC∧B+m dC∧B3+920m2B5], where g:=det⁡(gMN) in −g, and ϵM1…M10 is the alternating contravariant coordinate density normalized by ϵ01…9=+1 in positively oriented coordinates, not a tensor raised with g. In particular, the first topological term uses the explicit source contraction 19ϵM1…M10∂M1CM2M3M4 ∂M5CM6M7M8 BM9M10, as in Eq. (2.4); the remaining top-form products use the same component and orientation conventions. No overall 1/(2κ02) is inserted. No α′ normalization or identification of m with the F0 in the separate Graña massive-RR convention is supplied. Fermions are set to zero. This is a source-reported low-energy action, not a derivation from string theory.

Use natural units, length-valued target coordinates, dimensionless metric, dilaton, and coordinate components of B,A,C; then m,H,F,G have component dimension length−1, and each term in the local density has dimension length−2. Because the source prints no overall gravitational coupling, this statement does not assign a dimensionless normalization to the integrated action.

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources