pith. machine review for the scientific record. sign in
abbrev definition def or abbrev high

Tensor

show as:
view Lean formalization →

A (p,q)-tensor on 4D spacetime maps each point in R^4 to a real-valued array indexed by p contravariant and q covariant indices drawn from Fin 4. Cosmologists building inflation models and relativists constructing Hamiltonians cite this when assembling scalar fields or Ricci tensors. The declaration is a direct type abbreviation with no lemmas or reduction steps.

claimA $(p,q)$-tensor on 4-dimensional spacetime is the function type $T: (x : Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ$ that supplies the components of a multilinear map at each spacetime point.

background

The module supplies scaffolding type abbreviations for tensorial objects in relativity and is explicitly marked as outside the certificate chain. Tensor specializes the general notion to 4D spacetime using Fin 4 for both the coordinate domain and the index sets, matching the Idx abbreviation used elsewhere for spacetime labels. Sibling definitions such as ScalarField, VectorField, BilinearForm, and contract build directly on this structure to define fields, forms, and operations.

proof idea

Direct abbreviation that equates Tensor (p q) to the function type (Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ with no tactics or lemmas applied.

why it matters in Recognition Science

The abbreviation supplies the geometric substrate for 25 downstream declarations, including InflationPredictions (which records n_s ≈ 1 - 2/N and r ≈ 8/N² for J-cost inflation), tensorScalarRatio, amplitude_derivation, and TotalHamiltonian (the spatial integral of the Hamiltonian density over the metric). It anchors the relativity geometry layer that feeds the eight-tick octave and D = 3 spatial structure while remaining outside the main forcing chain.

scope and limits

formal statement (Lean)

  12abbrev Tensor (p q : ℕ) := (Fin 4 → ℝ) → (Fin p → Fin 4) → (Fin q → Fin 4) → ℝ

proof body

Definition body.

  13

used by (25)

From the project-wide theorem graph. These declarations reference this one in their body.