Only one direction of the frame law is an axiom; the converse is free

Identifier: F:top-frame-converse-distributive-law-is-a-theorem
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

In any frame F, JOIN n. (a AND f n) <= a AND (JOIN n. f n). Unlike the distributive law itself this direction needs no frame axiom at all: it holds in every complete lattice, off the two universal properties (supLe, leSup), the two meet projections (infLeLeft, infLeRight) and transitivity. Recording it separately is the point. A textbook states the frame law as an equality and leaves the reader to notice that half of it is free; a record that took the equality as a field would silently demand a theorem from every instance. Here the record's field is the hard direction only, this is the easy one proved once generically, and Top.Frame.frame_law is the two glued together.

Formal statement

theorem Top.Frame.le_inf_sup : ((x0 : Top.Frame) -> ((x1 : Top.Frame.carrier x0) -> ((x2 : ((x2 : AxNat) -> Top.Frame.carrier x0)) -> Top.Frame.le x0 (Top.Frame.sup x0 (fun (x3 : AxNat) => Top.Frame.inf x0 x1 (x2 x3))) (Top.Frame.inf x0 x1 (Top.Frame.sup x0 x2)))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

0 direct dependencies 0 direct dependents

Evidence

kernel-Top.Frame.le_inf_sup

Kind: kernel-term
Status: checked

Supports: Top.Frame.le_inf_sup is admitted by the trusted kernel gate with the type recorded in formal.statement, and Kernel::axiom_footprint reports 0 assumed names.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example top_frame_theorem_inventory -- Top.Frame.le_inf_sup | grep -cE '^theorem[[:space:]]+Top\.Frame\.le_inf_sup[[:space:]]+4[[:space:]]+0[[:space:]]'

Evidence notes

The exit status depends on the finding three times over. top_frame_theorem_inventory exits NON-ZERO when the filter matches nothing (asking for a declaration and finding none is a failure, not an empty report) AND when any printed row carries a nonempty axiom footprint. grep -c then exits 1 printing 0 unless the anchored row is present with the recorded binder count and a footprint column of exactly 0. Anchored with [[:space:]], never a backslash-t: in a scripted (GNU) grep that is a literal t, and 68 checkers in this ledger were wrong for exactly that reason. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY: this binary builds creal underneath Top, which overflows the default debug thread stack. Definition rows need --defs and are off by default, so a caller who forgets that reads a false ABSENT rather than a wrong type.

suite-the_sup_le_slot_is_load_bearing

Kind: exhaustive-enumeration
Status: checked

Supports: The supLe field this theorem is built from is checked, not decorative: rebuilding Top.ballFrame with Top.Opens.le_refl in the supLe slot is REFUSED by Kernel::add_declaration. supLe is the universal property of the countable join and is the only field that could make this direction provable, so a decorative supLe would make the claim vacuous.

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- top_frame::top_frame_tests::the_sup_le_slot_is_load_bearing --test-threads=4 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

The `1 passed` is load-bearing: `cargo test -- <filter>` runs ZERO tests and exits 0 when the filter matches nothing, so a rename would turn this checker green while checking nothing. Requiring the exact count is what makes the exit status depend on the finding. --release is mandatory (the creal prelude overflows the debug thread stack); --test-threads=4 keeps the shared build off the OOM ceiling.

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_top_frame_prelude (crates/axeyum-lean-kernel/src/top_frame.rs)",
  "source": "Lane `frame-carrier`, roadmap W2-21, executing ADR-1602's pointfree recommendation and decided in ADR-1643 (docs/research/09-decisions/adr-1643-the-frame-carrier-is-nat-indexed-and-the-ball-index-is-not-a-nat.md). formal.statement is Kernel::render_lean of the declaration's type, taken verbatim from the unfiltered emit of `top_frame_theorem_inventory --defs`; axiom_footprint is that tool's footprint column, which reads Kernel::axiom_footprint."
}