soulExports
plain-language theorem explainer
This definition assembles a two-element list of SoulInvariantExport records that package the canonical virtue signature and the strict positivity of recognition energy for soul characters. An auditor or exporter working on ethical invariants in Recognition Science would cite it when building the JSON payload for downstream serialization. The definition is a direct list literal that supplies hardcoded name, description, and proof-reference strings for each item.
Claim. Let soulExports be the list whose first entry records the canonical VirtueSignature (with its family-loading vector and nonzero sigma effect) and whose second entry records the theorem that every SoulCharacter state has strictly positive recognition energy.
background
SoulInvariantExport is the structure { name : String, description : String, proof : String } used to bundle named invariants for export. The present definition lives in Exports.Virtues and draws its two entries from upstream results: VirtueSignature (a record carrying a Fin 4 family-loading vector and a real sigma_effect, unique for the Love virtue) and the theorem energy_pos from OscillatoryDynamicsDeep (which states 0 < energy_level n for every natural n, proved by unfolding to a product of positive terms involving omega and phi^5).
proof idea
The definition is a direct list literal that constructs two SoulInvariantExport records by supplying the strings for name, description, and the fully qualified proof identifier; no tactics or lemmas are applied beyond the literal construction.
why it matters
soulExports populates the soul_invariants field of exportPayload, the top-level JSON object that serializes all collected virtue and character invariants. It therefore completes the export path for properties derived from the Recognition Science forcing chain (T5 J-uniqueness and T6 phi fixed point) and from the oscillatory energy positivity result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.