Pipeline-generated

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.

Oriented Lorentzian fields, observers and coordinate conventions — Examples

1 · Prerequisites

2 · Summary

Scope

This companion computes the Lorentzian Hodge star on one constant two-form in oriented Minkowski four-space. It checks the two-form sign $⋆_{g}^{2} = - id$ and the electric/magnetic scalar contractions using the conventions proved on emg-mg01. The example is a mathematical calculation; it records no observation and assumes no Maxwell model.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: AI-adaptedVerification: AI-adaptedverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)Open item page →

Lorentz star square and constant two-form

Example

On $R^{4}$ take the metric $g = diag (- 1, 1, 1, 1)$ , the orientation $d x^{0} \land d x^{1} \land d x^{2} \land d x^{3}$ , and the time-orientation field $N : = \partial_{0}$ . Then $n : = \partial_{0}$ is an observer because $g (n, n) = - 1$ and $g (n, N) = - 1 < 0$ . For constants $c > 0$ and $E_{0}, B_{0} \in R$ , let

$F = - \frac{E_{0}}{c} d x^{0} \land d x^{1} + B_{0} d x^{2} \land d x^{3} .$

This constant two-form has

$⋆_{g} F = \frac{E_{0}}{c} d x^{2} \land d x^{3} + B_{0} d x^{0} \land d x^{1}, ⋆_{g}^{2} F = - F,$

$F_{a b} F^{a b} = 2 (B_{0}^{2} - E_{0}^{2} / c^{2}), F \land F = - \frac{2 E_{0} B_{0}}{c} {v o l}_{g} .$

The calculation concerns the mathematical Lorentzian Hodge operator and a smooth two-form. It does not assert that a physical field was measured or that a Maxwell model was adopted.

Facts & Assumptions

Given: The oriented Minkowski metric and two-form in the Example, with real $E_{0}, B_{0}$ and $c > 0$ .

[F1]

In an oriented orthonormal coframe, $⋆_{g} e^{01} = - e^{23}$ , $⋆_{g} e^{23} = e^{01}$ , and $⋆_{g}^{2} = - id$ on two-forms. (Lorentzian exterior calculus and Hodge star)

[F2]

The component formula for the exterior derivative is $(d F)_{a b c} = 3 \partial_{[a} F_{b c]}$ . (The exterior derivative by the invariant vector-field formula, The local coordinate formula for the exterior derivative)

[F3]

The wedge product is graded-commutative, so two-forms commute under $\land$ . (Differential forms form a graded commutative algebra)

[F4]

Index raising uses the inverse Lorentz metric of the Example. (The inverse metric, musical isomorphisms and index raising)

[A1]

The constants are formal real parameters; no physical unit or empirical value is used.

Verification

1.1F1givenA1algebra

Under the formal-parameter assumption [A1], apply [F1] to $d x^{0} \land d x^{1}$ and $d x^{2} \land d x^{3}$ . Linearity gives $⋆_{g} F = (E_{0} / c) d x^{2} \land d x^{3} + B_{0} d x^{0} \land d x^{1}$ . Applying [F1] again gives $⋆_{g}^{2} F = (E_{0} / c) d x^{0} \land d x^{1} - B_{0} d x^{2} \land d x^{3} = - F$ .

1.2givenF4algebra

By [F4] and the diagonal metric, $F^{01} = E_{0} / c$ and $F^{23} = B_{0}$ . Antisymmetry counts the $01$ and $23$ pairs twice, so $F_{a b} F^{a b} = 2 (- E_{0}^{2} / c^{2} + B_{0}^{2})$ .

2.1F2F3givenalgebra∎

The only nonzero wedge contribution is the cross term between $- (E_{0} / c) d x^{0} \land d x^{1}$ and $B_{0} d x^{2} \land d x^{3}$ . By [F3] it occurs twice and equals $- 2 E_{0} B_{0} {v o l}_{g} / c$ . The coefficients of $F$ are constant, so [F2] also gives $d F = 0$ . These are mathematical identities, with no Maxwell or empirical premise.