metric_from_rrf
metric_from_rrf constructs a metric tensor by adding a diagonal term k psi(x) to the Minkowski eta bilinear form. Workers building perturbed spacetimes in scalar-tensor or recognition-based gravity cite it for explicit coordinate expressions. The body assembles the g component directly and verifies symmetry via a two-case split on index equality.
claimThe metric tensor satisfies $g(x,up,low) = eta(x,up,low) + k psi(x)$ when the two indices in low coincide and $g(x,up,low) = eta(x,up,low)$ otherwise, where eta returns the Minkowski values $-1$ (time) or $+1$ (space) on the diagonal and zero off-diagonal.
background
The MetricTensor structure packages a bilinear form g with a symmetry axiom that equates evaluation on an index pair and its swap. The eta function supplies the flat Minkowski bilinear form, nonzero only on matching indices and carrying the signature diag(-1,1,1,1). This definition lives inside the Relativity.Geometry.Metric module, which imports tensor and derivative support to express local metric components.
proof idea
The definition populates g by summing the eta form (applied at zero up-index) with the perturbation k psi(x) on equal indices. Symmetry follows by unfolding eta, dsimp, then case analysis on index equality; each branch rewrites the conditional to equate the two sides.
why it matters in Recognition Science
The construction supplies a concrete perturbed metric inside the relativity geometry layer, ready for use in gravity and cosmology modules though no direct dependents are recorded yet. It preserves the four-index structure required by the eight-tick octave while allowing scalar modifications, consistent with the D=3 spatial setting of the forcing chain.
scope and limits
- Does not verify that the resulting metric obeys the Einstein equations.
- Does not compute curvature tensors or Christoffel symbols from g.
- Does not link psi to the phi-ladder or recognition composition law.
- Does not guarantee preservation of Lorentz signature for arbitrary psi and k.
formal statement (Lean)
35noncomputable def metric_from_rrf (psi : (Fin 4 → ℝ) → ℝ) (k : ℝ) : MetricTensor :=
proof body
Definition body.
36 { g := fun x _ low =>
37 eta x (fun _ => 0) low + k * psi x * (if low 0 = low 1 then 1 else 0)
38 symmetric := by
39 intro x up low
40 unfold eta
41 dsimp
42 by_cases h : low 0 = low 1
43 · have h_rev : low 1 = low 0 := h.symm
44 rw [if_pos h, if_pos h, if_pos h_rev, if_pos h_rev]
45 rw [h]
46 · have h_rev : low 1 ≠ low 0 := fun heq => h heq.symm
47 rw [if_neg h, if_neg h, if_neg h_rev, if_neg h_rev] }
48