raiseIndex
This definition supplies the identity map on abstract tensor indices for the ILG action scaffold. It would be cited when simplifying index manipulations inside the Einstein-Hilbert term or field kinetic terms. The implementation is a direct one-line identity equipped with the simp attribute.
claimThe map that raises an abstract tensor index is the identity function on natural numbers: for any index symbol represented by a natural number $n$, raiseIndex$(n) := n$.
background
The module re-exports geometry and field types for constructing the ILG action. Index is introduced locally as the abbreviation Nat, serving as a symbolic placeholder for tensor indices rather than a concrete coordinate label. The upstream PeriodicTable.Index supplies a separate structure carrying rail and block data for electron counting, but the present declaration uses only the local Nat convention.
proof idea
One-line definition that returns the input unchanged, annotated with @[simp] for automatic reduction in surrounding expressions.
why it matters in Recognition Science
It supplies the minimal placeholder required before index-raising operations can appear inside EHAction and S_EH. The declaration sits inside the relativity re-export layer that prepares geometry for the Recognition Science forcing chain, where D = 3 and the eight-tick octave are ultimately imposed. No downstream theorems yet reference it, indicating the scaffold remains open for metric-dependent lifting rules.
scope and limits
- Does not encode metric-dependent index raising or lowering.
- Does not assume a specific spacetime dimension or signature.
- Does not interact with the phi-ladder or J-cost functions.
- Does not discharge any hypothesis about tensor contraction.
formal statement (Lean)
56@[simp] def raiseIndex (μ : Index) : Index := μ