Bishop's natural sampling indices are closed under composition

Identifier: F:rat-nat-index-compose
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For naturals a, b, n, with D = (a+1)*b + a: (a+1)*((b+1)*n + b) + a = (D+1)*n + D -- every nested product of CReal.mul/CReal.add sampling indices has the same (c+1)*n + c shape as a single one.

Formal statement

theorem Rat.nat_index_compose : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (AxNat.add (AxNat.mul (AxNat.succ x0) (AxNat.add (AxNat.mul (AxNat.succ x1) x2) x1)) x0) (AxNat.add (AxNat.mul (AxNat.succ (AxNat.add (AxNat.mul (AxNat.succ x0) x1) x0)) x2) (AxNat.add (AxNat.mul (AxNat.succ x0) x1) x0)))))

Dependencies

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

5 direct dependencies 5 direct dependents

Evidence

kernel-Rat.nat_index_compose

Kind: kernel-term
Status: checked

Supports: Rat.nat_index_compose 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.nat_index_compose 2>/dev/null | grep -cE '^Rat\\.nat_index_compose[[:space:]]'

Evidence notes

`build_rat_prelude` admits Rat.nat_index_compose through the trusted `Kernel::add_declaration` gate, which re-checks the proof term against the stated type, so a line in this tool's output for the exact name is a machine-checked proof having been admitted. `theorem_dependency_inventory` exits non-zero for a named filter that matches nothing (a deleted theorem cannot read as a re-derived one), and `grep -c` (never `-q`) both avoids a SIGPIPE-under-pipefail false negative and independently asserts the exact tab-anchored line is present -- two ways the same absence would be caught. `--release` is MANDATORY: this tool also builds `creal`/`complex`/`cpoint`, which recurse deep enough in a debug build to overflow the default thread stack (measured: release exits 0, debug SIGABRTs at 134) -- the same resource-limit gotcha already documented for `prelude_theorem_inventory --include-constructed`.

footprint-Rat.nat_index_compose

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the Rat prelude's trusted surface is empty

Checker command

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

Evidence notes

`nat_axiom_inventory` builds the Rat environment as its own group and reports `rat: axiom=0 opaque=0 quotient=0 total_trusted=0` (re-measured on this tree). That bounds every individual Rat theorem's footprint by [], since a theorem cannot depend on a trusted declaration the environment does not contain -- and the enumeration covers Axiom, Opaque AND Quotient, not just Declaration::Axiom, because Opaque has no proof body and Quotient admits Quot.sound. `--require-axiom-free <name>` is an error (not a silent pass/zero) for a prelude this run never built, which is what makes `rat` here a claim rather than an absence.

Provenance

{
  "date": "2026-08-25",
  "established_by": "axeyum-lean-kernel build_rat_prelude",
  "source": "theorem name and dependency edges from theorem_dependency_inventory; canonical type read via a standalone probe binary depending on axeyum-lean-kernel by path and calling only its public Kernel API (environment(), display_name(), render_lean(), axiom_footprint()) -- the same calls nat_theorem_inventory itself makes -- because no in-tree example currently prints Rat theorem types (crates/ source was left untouched per this task's constraint). Probe deleted after use."
}