Struct LaneLawFile 

pub struct LaneLawFile {
    pub label: String,
    pub theorem: String,
    pub module: String,
    pub content: String,
}

One emitted lane law: a single hashed Lean module hosting the universal twin theorem, exposed as its own non-default lean_lib.

Fields

label: String

fn.law label for surfacing (dispatchNumberOrErr.fromIntRoundtrip).

theorem: String

Twin theorem name (<fn>_law_<law>_universal).

module: String

Module = file stem = lib name, content-hashed so a stale .olean under an old name is unreachable.

content: String

Full .lean source. Contains NO sorry token.