idMorphism
plain-language theorem explainer
Every reference structure carries an identity morphism: symbols and objects map to themselves, and reference cost is unchanged. Category-style arguments about composition of aboutness use this unit. The construction is immediate: identity maps plus reflexivity of ≤ on costs.
Claim. For any reference structure $R$ on symbol type $S$ and object type $O$ (a nonnegative cost $R(s,o)$ of $s$ pointing to $o$), there is a reference morphism $R \to R$ given by the identity on symbols, the identity on objects, and the inequality $R(s,o) \le R(s,o)$ for all $s,o$.
background
The module formalizes the Physics of Reference: aboutness as cost-minimizing compression. A configuration $S$ (symbol) points to $O$ (object) when the ledger link between them minimizes $J$-cost. The core object is a reference structure: a map $\mathrm{cost}: S \to O \to \mathbb{R}$ with $\mathrm{cost}(s,o) \ge 0$.
A reference morphism $R_1 \to R_2$ is a pair of maps on symbols and objects that does not raise reference cost: $R_2(\mathrm{map}_S s, \mathrm{map}_O o) \le R_1(s,o)$. Cost may fall (compression) but never increase. This is the arrow type for the algebra of aboutness, parallel to cost-algebra automorphisms and Peano homomorphisms elsewhere in the foundation stack.
Upstream, reflexivity of $\le$ on the relevant ordered carriers (including arithmetic-from-logic and signed-orbit order) supplies the trivial cost inequality for identical pairs.
proof idea
Definitional construction, not a tactic proof. Fill the three fields of a reference morphism $R \to R$: set both symbol and object maps to the ordinary identity function; discharge $\mathrm{cost_le}$ by $\mathrm{le_refl}$ on each pair $(s,o)$, so $R(s,o) \le R(s,o)$. No appeal to the Recognition Composition Law or to $J$-uniqueness is required.
why it matters
Gives the monoidal unit for reference morphisms in the Algebra of Aboutness. The module lists composition theorems (products, sequences) and triangle inequality for chained reference; identity is the missing unit so those arrows form a category-like structure rather than a bare semigroup of maps.
It sits with the main results on forced symbols from $J>0$ objects, ratio-induced reference from $J(x)=\frac12(x+1/x)-1$, representation equivalence at mutual cost zero, and the effectiveness principle for near-balanced configurations. No downstream uses are recorded yet; the next declaration in-file is composition of reference morphisms, the natural consumer.
Framework-wise this is structural scaffolding for reference-as-compression, not a forcing-chain step (T5–T8). It does not derive $\phi$, eight-tick structure, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.