The ordered-ring interface telescope is byte-identical over Real and over the axiom-free Int development

Identifier: F:ordered-ring-interface-is-the-same-over-the-axiom-free-integers
Proof route: kernel-lean
External status: unknown
Axiom footprint: Empty

Recorded description

The 30 binder types of the ordered-ring interface telescope, computed by abstracting each declaration's type over the earlier telescope entries, render byte-identically whether they are read off the axiomatized Real package (30 axioms, this repository's whole remaining trusted surface) or off the constructed Int development (30 theorems, measured trusted surface 0). So the axiom ledger's 30 SHA-256 type pins can be carried by a development that assumes nothing.

Formal statement

For the ordered-ring signature S over an environment E, let T(S) be the 30-entry sequence T(S)[i] = abstract_consts(ty_E(S.decl[i]), S.decl[0..i]), i.e. each declaration's type with every earlier interface entry replaced by its de Bruijn binder. Claim: render_lean(T(RingSignature.of Real)[i]) = render_lean(T(RingSignature.of Int)[i]) as UTF-8 byte strings, for all i < 30, where Real is build_arith_prelude (30 Declaration::Axiom) and Int is build_int_prelude (30 proved declarations, trusted surface 0).

Dependencies

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

2 direct dependencies 0 direct dependents

Evidence

ordered-ring-interface-is-the-same-over-the-axiom-free-integers-1

Kind: kernel-term
Status: checked

Supports: The finding itself: all 30 binder types agree, and none differ. The example's exit status depends on it (`--require-identical` exits 1 on any difference), so this row cannot pass on a run that found a difference.

Checker command

out=$(cargo run --release -q -p axeyum-solver --features full --example ring_interface_pin -- --require-identical 2>&1) && test "$(printf "%s\n" "$out" | grep -Ec 'ring interface telescope: 30 binders, 30 identical, 0 differing')" -ge 1

Evidence notes

Anchored on the count line the example computes from the comparison, not on prose. Mutated output (any binder differing) changes '30 identical, 0 differing' and the pattern stops matching; the command also exits nonzero. Verified discriminating by scripts/new-fact.py.

ordered-ring-interface-is-the-same-over-the-axiom-free-integers-2

Kind: kernel-term
Status: checked

Supports: Coverage of the `Real` side: 30 rows were actually emitted from the axiomatized package, so 'identical' is not the identity of an empty comparison.

Checker command

out=$(cargo run --release -q -p axeyum-solver --features full --example ring_interface_pin -- --require-identical 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^real\s')" = 30

Evidence notes

Anchored on the row population of the `real` source column. This is a POPULATION check, declared as such (--allow-population-only): it catches the `Real` telescope disappearing from the comparison, not a value changing inside a row that is still there. Row 1 is what catches the values.

ordered-ring-interface-is-the-same-over-the-axiom-free-integers-3

Kind: kernel-term
Status: checked

Supports: Coverage of the `Int` side, symmetrically — and the two together are what make the zero above a comparison of two populated telescopes rather than of one against itself.

Checker command

out=$(cargo run --release -q -p axeyum-solver --features full --example ring_interface_pin -- --require-identical 2>&1) && test "$(printf "%s\n" "$out" | grep -cE '^int\s')" = 30

Evidence notes

As row 2, for the `int` source column.

Provenance

{
  "date": "2026-08-18",
  "established_by": "agent-shrink-control",
  "source": "ADR-0515; crates/axeyum-solver/examples/ring_interface_pin.rs, crates/axeyum-solver/src/reconstruct/arithmetic/ordered_ring.rs (ring_interface_telescope)"
}