lowerIndex
plain-language theorem explainer
The lowerIndex definition supplies an identity map on abstract tensor indices for symbolic raising and lowering in the ILG action formalism. Researchers assembling relativistic Lagrangians in Recognition Science reference it when constructing the Einstein-Hilbert term or kinetic contributions without metric contraction. It is realized as a direct identity on the Nat-based Index type and carries a simp attribute for automatic reduction.
Claim. The index lowering map acts as the identity: for an abstract index $μ ∈ ℕ$, one has $μ^♭ = μ$.
background
The module re-exports geometry and field types to support the integrated Lagrangian in ILG. The Index type is an abbreviation for the natural numbers, used as symbolic labels for tensor components. Upstream results include the Kronecker delta on Fin n from Cost.Ndim.Connections, the identity event at J-cost minimum from ObserverForcing, and nuclear density tiers from NucleosynthesisTiers that place physical quantities on discrete φ-ladders.
proof idea
The definition is a one-line identity lowerIndex μ := μ, annotated with simp to enable automatic simplification during index algebra.
why it matters
This placeholder supports construction of the Einstein-Hilbert action and field terms inside the Relativity.ILG.Action module. It aligns with the Recognition Science forcing chain at T8 (D = 3) and the Recognition Composition Law by keeping index notation symbolic until metric structure is introduced. It touches the open question of embedding full metric compatibility into the discrete φ-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.