exportPayload
plain-language theorem explainer
exportPayload defines a JSON object packaging the exported virtues and soul invariants under a fixed version string. Researchers integrating the Recognition Science ethics layer with external tools would cite this when serializing framework outputs. The definition is a direct construction via Json.mkObj applied to the precomputed lists from virtueExports and soulExports.
Claim. The export payload is the JSON object with fields $version = ``1.0.0''$, $virtues = toJson(virtueExports)$, and $soul_invariants = toJson(soulExports)$.
background
In the Exports.Virtues module, virtueExports is a list of VirtueExport entries, each carrying a name such as Love together with references to conservation, cadence, and gauge proofs drawn from the ethics layer. soulExports is a parallel list of SoulInvariantExport records that include canonical virtue signatures and energy positivity statements for SoulCharacter states. The local setting assembles these pre-defined lists into a single serializable payload for downstream consumption in the Recognition Science framework.
proof idea
The definition is a direct one-line construction that applies Json.mkObj to a three-element list containing the version string, the JSON serialization of virtueExports, and the JSON serialization of soulExports.
why it matters
This definition supplies the payload consumed by the main entry point that prints the serialized exports. It supports the framework's ethics layer by making virtues such as Love and soul invariants such as energy positivity accessible outside the core formalization, aligning with the Recognition Science goal of exporting conserved quantities and character properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.