P3: assets' posted and scheduled depreciation, their bases, and the K-1 on the tax basis (defect 13, D-41)

Book value is cost less what the books posted; the schedule's figure is
apart. An asset's acquired date comes from its entry. Contributed
property keeps its section 723 carryover basis apart from its depreciable
basis (the lower of value and adjusted basis), with its 704(c) built-in
gain and method. The K-1 worksheet reports tax-basis capital (Form 1065
Item L) beside the book figures, leaving open what only the CPA knows.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01T3gXMVt7XJPi6ens1or9Dj

docs/verification.md

@@ -419,6 +419,22 @@ months); an exhaustive test walks the kernel itself over every
 1-to-3-month span of two calendar years, and the bridge and the exact
 unit tests check the rest.
 
+### An asset's basis figures (P3, defect 13)
+
+The register's tax figures beside book value (rules.md B-25) come from
+one kernel function, `kernel::basis_figures`, for every rule:
+
+27. **Each figure follows from the rule and the facts, and none
+    overflows**: a purchase depreciates from its cost and has no §723 basis
+    or built-in gain; a contribution's §723 basis is the member's adjusted
+    basis and its built-in gain the value less it (a loss exactly when the
+    basis exceeds the value); carryover property depreciates from the
+    basis, personal-use property from the lesser of value and basis (at
+    most each, equal to one). · Kani `basis_figures_laws` (every rule,
+    costs, bases and values within the bounds) · bridge `basis_figures_agree`
+    (the `Decimal` instantiation agrees, rule by rule) · property
+    `prop_basis_figures_laws`
+
 ## What the proofs found
 
 The engine already had 190+ tests, property tests, mutation testing,