Rat.unskip_matSkip: unskip p is a left inverse of the injection matSkip p, unconditionally

Identifier: F:rat-unskip-mat-skip
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Rat.matSkip p is the order-preserving injection [0,n) -> [0,n+1) whose image misses p. Rat.unskip p is declared here as its left inverse: unskip p q is q's position in [0,n+1) minus {p}. This fact records that unskip p (matSkip p k) = k for every p and k, with NO hypothesis -- unlike every other lemma in this cluster, which carries a Nat.ble premise. It is unconditional because matSkip p never produces p, so its whole image lies where unskip p inverts it, and the two branches of the guard are covered by the two branches of the recursion rather than by a case split. This is the index lemma that lets a Laplace double-expansion summand be defined as a function of the two COLUMNS: the inner cofactor column is k, but the summand has to be a function of (p, q), and k = unskip p q is how it is recovered.

Formal statement

theorem Rat.unskip_matSkip : ((x0 : AxNat) -> ((x1 : AxNat) -> Eq.{1} AxNat (Rat.unskip x0 (Rat.matSkip x0 x1)) x1))

Dependencies

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

0 direct dependencies 0 direct dependents

Evidence

kernel-Rat.unskip_matSkip

Kind: kernel-term
Status: checked

Supports: Rat.unskip_matSkip is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

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

Evidence notes

Two independent failure modes: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. Anchored with [[:space:]], never \t. ONE name per invocation. --release is MANDATORY.

footprint-Rat.unskip_matSkip

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the rat prelude's trusted surface is empty, which bounds Rat.unskip_matSkip.

Checker command

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

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built.

control-unskip-computes-both-branches

Kind: kernel-term
Status: checked

Supports: Rat.unskip is a DEFINITION, so the trusted gate says only that it is well-formed: Nat -> Nat -> Nat is that type whatever the function returns. It is reduced at concrete arguments hitting BOTH branches -- unskip 2 1 = 1 (identity) and unskip 2 3 = 2 (shift down) -- and unskip 2 3 is separately asserted NOT to be 3.

Checker command

cargo test -p axeyum-lean-kernel --lib the_laplace_summand_layer_computes 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

The count is tested, not just the exit status. The two arguments are one pair on purpose: a definition that took the identity branch everywhere passes the first and fails the second, and one that took the shift branch everywhere does the reverse -- NEITHER ALONE separates them. What it does NOT check: any behaviour at symbolic arguments, which this fact's own statement covers, or Rat.matSkip's guard order, which Rat.det_eq_det2 separates.

control-adr-1185-unskip-sweep

Kind: exhaustive-enumeration
Status: checked

Supports: The declared double-Nat.rec form agrees with the ble/pred closed form at all 64 pairs below 8; the left-inverse identity holds at all 81 pairs below 9; and under the Rat.matSkip branch-swap mutation it is FALSE at 72 of 81, so it carries real index content.

Checker command

python3 docs/research/09-decisions/adr-1185-laplace-summand-checks.py 2>&1 | grep -cE '^  unskip_matSkip +FALSE'

Evidence notes

grep -c on a tested count, consuming the whole pipe: the line only appears when the mutation actually falsifies the statement, so a mutation that changed nothing would report 0 and fail. The script separately carries a NEGATIVE control on the recursion itself -- a succ row that forgets its own succ must differ, and does at 49 of 64 pairs -- and exits 1 on any failure.

Provenance

{
  "date": "2026-08-31",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/matrix_det.rs)",
  "source": "Lane laplace-summand, closing ADR-1155's named remainder. Design note: ADR-1185."
}