The rational identity matrix is a left unit for matrix multiplication, on its range

Identifier: F:rat-matmul-id-left
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For a matrix A over the constructed rationals (a function Nat -> Nat -> Rat), a dimension n, and indices i and j WITH i < n, the (i, j) entry of matId * A equals A i j. Rat.matId i j is one when Nat.beq i j and zero otherwise; it carries no dimension argument, because the delta is defined at every index pair and the bound belongs in the theorem rather than in the object. The `i < n` hypothesis is LOAD-BEARING, not decoration: matMul matId A n i j sums matId i t * A t j over t < n, so at a row index outside that range the delta never fires and the entry is zero rather than A i j. Stated pointwise; `funext` is absent from this kernel so an Eq between matrices is not available.

Formal statement

theorem Rat.matMul_id_left : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Rat))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat.lt x2 x1) -> Eq.{1} Rat (Rat.matMul Rat.matId x0 x1 x2 x3) (x0 x2 x3))))))

Dependencies

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

3 direct dependencies 1 direct dependents

Evidence

kernel-Rat.matMul_id_left

Kind: kernel-term
Status: checked

Supports: Rat.matMul_id_left is admitted by the trusted kernel gate with the type recorded in formal.statement. It goes through Rat.sumRange_delta (a sum whose summand vanishes away from one index collapses to the value at that index), proved by induction on the bound with the strict inequality INSIDE the motive so the base case discharges by Nat.not_lt_zero.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- Rat.matMul_id_left 2>/dev/null | grep -cE '^Rat\.matMul_id_left[[:space:]]'

Evidence notes

Verified BOTH directions on this tree. Real name: prints 1, exit 0. A fabricated name prints 0 and exits 1 -- the tool exits non-zero for a filter matching nothing, and `grep -c` (never `-q`, which SIGPIPEs its producer under pipefail) independently asserts the count. Pass ONE name per invocation: this tool consumes only its FIRST name argument and silently ignores the rest, printing a plausible one-row result. `--release` is MANDATORY (debug SIGABRTs on a stack overflow building creal/complex/cpoint). `[[:space:]]` and NOT `\t`, for the ugrep/GNU-grep disagreement documented in CLAUDE.md.

bound-is-load-bearing

Kind: instance-pin
Status: checked

Supports: The `i < n` hypothesis is necessary and the unbounded form of this statement is FALSE, demonstrated by computation rather than asserted in prose. `rat_mat_mul_id_left_needs_its_bound` takes A = [[1,2],[3,4]] (as A i j = (i+i+j+1)/1, defined at every index) and n = 2, checks matId * A agrees with A at all four in-range cells AND on the right, then evaluates at the OUT-of-range row i = 2: matId 2 0 * A 0 0 + matId 2 1 * A 1 0 = 0*1 + 0*3 = 0, while A 2 0 = 5. Both values are pinned and the test asserts they differ.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib rat_prelude::rat_prelude_tests::rat_mat_mul_id_left_needs_its_bound -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

This is the evidence a footprint check cannot carry and a statement pin can only half carry. An axiom-free theorem with a superfluous hypothesis has the same footprint as one whose hypothesis is necessary; only the out-of-range evaluation separates them. The command is anchored on the exact `1 passed; 0 failed` count so an unmatched filter -- which prints `running 0 tests ... ok` and exits 0 -- cannot read as success. `Rat.matId` is a Definition, so it is invisible to prelude_theorem_inventory (which lists Theorems only) and its correctness rests on this evaluation, not on any inventory row.

footprint-Rat.matMul_id_left

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Rat prelude's trusted surface is empty, so no theorem in it can rest on anything asserted.

Checker command

cargo run -q -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free rat

Evidence notes

Re-measured on this tree: `rat: axiom=0 opaque=0 quotient=0 total_trusted=0`, exit 0. Covers Axiom, Opaque AND Quotient, since Opaque has no proof body and Quotient admits Quot.sound.

Provenance

{
  "date": "2026-08-30",
  "established_by": "lane rat-matrix-layer, Rat.matMul_id_left in crates/axeyum-lean-kernel/src/rat_prelude/matrix_n.rs",
  "source": "classical"
}