Definition Universe and Kernel Order

Abstract

Definitions form a dependent universe ordered by their equality kernels.

Theorem 1.1 (The definition universe carries its kernel and higher-order constructors).

$$\begin{gathered} \mathrm{Def}\left(X\right)={\Sigma }_{D:U}X\to D, \\ \ker \left(d\right)=\mathrm{SetoidKer}\left(d\right),\mathrm{Im}\left(d\right)=\mathrm{range}\left(d\right), \\ \mathrm{DefinitionEquivalent}\left(d,e\right)\iff \ker \left(d\right)=\ker \left(e\right),\mathrm{DefinitionRefines}\left(d,e\right)\iff \ker \left(e\right)\subseteq \ker \left(d\right), \\ \mathrm{DefinitionEquivalent}\left(d,e\right)\iff (\mathrm{DefinitionRefines}\left(d,e\right)\wedge \mathrm{DefinitionRefines}\left(e,d\right)),(\mathrm{Im}\left(d\right)=\mathrm{univ})\iff \mathrm{Surjective}\left(d\right), \\ \mathrm{MetaDef}\left(X\right)=\mathrm{Def}\left(\mathrm{Def}\left(X\right)\right),\mathrm{Generator}\left(X,S\right)=S\to \mathrm{Def}\left(X\right), \\ \mathrm{Transformer}\left(X,Y\right)=\mathrm{Def}\left(X\right)\to \mathrm{Def}\left(Y\right),\mathrm{Method}\left(X\right)=\mathrm{DState}\left(X\right)\times \mathrm{Residual}\left(X\right)\to \mathrm{Def}\left(X\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/DefinitionEscape/DefinitionUniverseKernel.definition_universe_kernel (✓ std3). ∎

Source. Repository-derived.

Commentary.

A definition on X is a dependent pair: its first projection is a codomain in the same universe and its second projection is the canonical Concept readout from X. Its kernel is delegated to Setoid.ker and its realized image to Set.range.

Conceptual equivalence is literal equality of source kernels. The coarse-to-fine relation reverses kernel inclusion, so equality holds exactly when both directed refinements hold. The realized image is universal exactly when the packaged readout is surjective.

MetaDef applies the same Sigma construction to Def X. Generators are S-indexed families, transformers map one definition universe to another, and a method consumes the paired definition and residual states to choose the next packaged definition.

The repository’s Refines relation is factorization rather than raw kernel inclusion. Separate bridge declarations apply the accepted concept-kernel order duality only for surjective readouts, where the two notions coincide. Boolean examples witness both a proper refinement and a realized image that omits a coordinate.

References

• Truth anchor: D5/S3/ConceptDynamics/DefinitionEscape/DefinitionUniverseKernel.definition_universe_kernel
• Dependency: D5/S3/ConceptDynamics/Interventions/RedundantAppealDefectPersistence
• Dependency: D5/S3/ConceptDynamics/Refinement/ConceptKernelOrderDuality