Phase 12: links-defined Peano natural numbers (advances #97)

[konard]

Summary

Advances #97 by adding the inductive data layer the issue's
Software Foundations reference (Logic.v, Basics.v, Induction.v)
starts from: Nat, zero, succ, addition, and induction
expressed entirely as links-level proof-substrate rules.

Successor stays a literal constructor; there is no succ → +1 host
shortcut. The host's decimal numeric domain is unaffected — this PR
adds an inductive substrate, not a replacement numeric backend. The
default foundation default-rml continues to be active on every fresh
Env, so every .lino file that ran before this PR runs identically
afterwards.

Builds on the merged foundation + trust-report scaffolding from PR
#175 and the semantic-status / proof-checking-relation layer from PR
#176. Follows the acceptance criteria from
issue #97 follow-up comment.

What's in this PR

• examples/nat-links.lino — declares the five
  proof-substrate rules nat-zero-formation, nat-succ-formation,
  nat-add-zero, nat-add-succ, nat-induction; builds zero,
  (succ zero), (succ (succ zero)) as inhabitants of Nat;
  computes 0+0, 1+0, 0+1, 1+1 step by step; and discharges a
  universal claim via induction. All 8 (check-proof …) calls return
  1 with no diagnostics.
• lib/self/foundations.lino — adds 9 (root-construct …)
  entries (Nat, zero, succ, add, nat-zero-formation,
  nat-succ-formation, nat-add-zero, nat-add-succ,
  nat-induction) with status: links-defined and
  semantic-status: links-checked, plus the
  (foundation nat-links …) declaration that bundles the five rules.
• JS + Rust host seeds —
  _registerDefaultFoundation (js/src/rml-links.mjs) and
  register_default_foundation (rust/src/lib.rs) pre-seed the
  nat-links foundation with extends default-rml so a fresh Env
  lists it in foundation-report without changing legacy semantics.
• examples/expected.lino — (nat-links.lino: 1 1 1 1 1 1 1 1)
  pins the byte-identical replay between engines.
• Tests — js/tests/nat-links.test.mjs and
  rust/tests/nat_links_tests.rs each add 10 tests covering
  foundation pre-registration, foundations.lino documentation,
  every individual rule, two negative cases that raise E064, and
  the end-to-end example replay.
• Docs — docs/FOUNDATIONS.md lists nat-links as a bundled
  foundation in §5 and adds Phase 12 to §10; the issue-97 case study
  (docs/case-studies/issue-97/README.md) gains a timeline row, a
  phase-table row, and a new §9.9 explaining the construction.

Acceptance-criteria coverage (issue #97 comment §7)

1. Adds a nat-links foundation — ✅ (foundation nat-links …)
   pre-registered in both engines.
2. Nat, zero, succ as explicit root constructs — ✅
   lib/self/foundations.lino.
3. Proves zero : Nat, succ zero : Nat, succ (succ zero) : Nat —
   ✅ proof-objects zero-is-nat, one-is-nat, two-is-nat.
4. Addition rules add zero n = n and add (succ m) n = succ (add m n)
   — ✅ rules nat-add-zero, nat-add-succ.
5. Replays at least two addition proof objects — ✅ four:
   zero-plus-zero, one-plus-zero, zero-plus-one, one-plus-one.
6. Separates nat-equality from host numeric equality — ✅ equals
   is a literal identifier consumed by the proof substrate's
   structural matcher; the host numeric = operator is never invoked
   for Nat reasoning.
7. Keeps all host boundaries visible in foundation-report — ✅ the
   rules are links-defined with links-checked semantics;
   pattern-matching/structural substitution remain explicit
   host-trusted boundaries unchanged.
8. JS and Rust parity tests — ✅ 10 + 10 mirrored tests; full
   npm test (1237 pass) and cargo test (all targets pass) green.
9. Examples + expected outputs — ✅ nat-links.lino +
   expected.lino entry.
10. Docs + case study updated — ✅ docs/FOUNDATIONS.md and
    docs/case-studies/issue-97/README.md.
11. No Fixes #97 — ✅ uses "Advances Use similar idea, but everything should be built from links and references #97".

Stretch goal — symbolic Nat induction rule + one proof object using it
— ✅ nat-induction rule + every-nat-is-nat proof object.

Test plan

• cd js && npm test — 1237 / 1237 pass (including 10 new
  nat-links tests).
• cd rust && cargo test — all binaries pass (including 10 new
  nat_links_tests).
• examples/expected.lino entry (nat-links.lino: 1 1 1 1 1 1 1 1)
  pins the shared-examples replay between engines.
• Negative cases verify E064 fires when a derivation violates a
  rule (mistyped successor, contradictory add-succ).
• (foundation-report) lists nat-links with sorted uses
[nat-add-succ, nat-add-zero, nat-induction, nat-succ-formation, nat-zero-formation] and extends default-rml in both engines.

Backward compatibility

Additive only. default-rml is still active on every fresh Env; no
existing operator, query result, or diagnostic shape changes.

[konard]

Working session summary

Phase 12 is complete and the PR is ready for review.

PR #177: #177

What landed:

• examples/nat-links.lino — 5 proof-substrate rules (nat-zero-formation, nat-succ-formation, nat-add-zero, nat-add-succ, nat-induction) + 8 (check-proof …) calls, all returning 1.
• lib/self/foundations.lino — 9 new (root-construct …) entries with links-defined/links-checked status, plus (foundation nat-links …) declaration.
• JS + Rust host seeds (_registerDefaultFoundation / register_default_foundation) pre-register nat-links extending default-rml.
• 10 JS tests (js/tests/nat-links.test.mjs) + 10 mirrored Rust tests (rust/tests/nat_links_tests.rs), including negative cases that raise E064.
• examples/expected.lino entry (nat-links.lino: 1 1 1 1 1 1 1 1) pins shared-examples replay between engines.
• Docs: docs/FOUNDATIONS.md §5 + §10; case study §1 timeline, §9 phase table, new §9.9.

Verification:

• npm test — 1237/1237 pass.
• cargo test --all-targets — all binaries pass.
• All 6 CI workflows green (tests, lint-english, bootstrap, parity, api-docs, docker).

Title uses "advances #97" (not "Fixes") per the acceptance criteria; default-RML semantics are unchanged.

---

This summary was automatically extracted from the AI working session output.

[konard]

🤖 Solution Draft Log

This log file contains the complete execution trace of the AI solution draft process.

💰 Cost: $8.667383

📊 Context and tokens usage:

Claude Opus 4.7: (3 sub-sessions)

1. 114.4K / 1M (11%) input tokens, 6.3K / 128K (5%) output tokens
2. 116.1K / 1M (12%) input tokens, 30.5K / 128K (24%) output tokens
3. 100.1K / 1M (10%) input tokens, 24.6K / 128K (19%) output tokens

Total: (11.7K new + 326.9K cache writes + 9.5M cache reads) input tokens, 73.3K output tokens, $8.667383 cost

🤖 Models used:

• Tool: Anthropic Claude Code
• Requested: opus
• Model: Claude Opus 4.7 (claude-opus-4-7)

📎 Log file uploaded as Gist (4943KB)

• View complete solution draft log

---

Now working session is ended, feel free to review and add any feedback on the solution draft.

[konard]

✅ Ready to merge

This pull request is now ready to be merged:

• All CI checks have passed
• No merge conflicts
• No pending changes

---

Monitored by hive-mind with --auto-restart-until-mergeable flag