[afflom]

Native language-1.2 decimal formatters currently inherit parser axioms through the combined Decimal instance. This source change uses the matching ToString evidence for formatting in Portable, Fixed, RustLemmas and the production certificate constructor, while retaining the shared Decimal parsing evidence and all exact policy declarations.

SM-39 preserves all 151 original boundary/parsing checks and 27 formatter/caller/parser policy observations. It uses the existing native runtime and A/B/E preservation machinery, including explicit replay/audit, a typed false-output lowering control and the Int empty-policy refusal. Unbounded Int observations stay native. The earlier unmerged closed-decision proof method was revised explicitly after its 18 LLV7002 failures; no new proof interface was added.

Evidence already obtained:

• Before implementation, the revised named conformance_sm_39 ran once on landed Port Host to v0.5 and make closed byte and string proofs practical #396: 0 passed, 1 failed, 483 filtered, 7.15s, with the intended sole LLV7005 for formatUInt8's empty policy observing [Classical.choice, Quot.sound, propext]. Caller/later assertions were not reached.
• Official model projection and comparison (484 IDs/86 codes), spec links, formatting and focused conformance Clippy passed on that regression-preparation tree, with correct linked roots and 905 embedded compiler inputs.
• The subsequent four-file implementation has independent source/graph review and standalone Rust formatting. Shared parsing subgraphs, policy declarations and 169 older-language partition files remain byte-identical. No post-fix compilation or positive SM39 result is claimed.

This PR is deliberately draft. Runtime/compiler identities and generated products are still the preceding versions. The source commit uses native [skip ci] to avoid a known-incomplete draft run; no required check was changed, and this is not CI acceptance. Reconcile the existing #405/#362/#433 source with the landed #396 work before one coordinated v0.5 identity/artifact wave. Official writers, actual canonical/type validation, all 27 policy observations, 151 native observations, fixed-width A/B/E checks, false-output and Int refusals, frozen older-language compatibility, and complete final changed-head CI remain required before readiness or merge. Preserve actual baseline and historical failure records in VERIFICATION.md.

Closes #434 only upon accepted completion. Parent #381 remains open for parsing coupling and the remaining String/decoder work.

[afflom]

Source review recorded at exact head77f6dd2d/tree8e9e2dc7. The four-part implementation matches the independently reviewed patch75b21d14: only formatDecimal's Portable type/value roots change; nine Fixed formatting operands and nine RustLemmas formatting applications use the matching existing ToString instances; the constructor's FormatDecimal arm supplies that evidence. The shared Decimal parsing closures/operands, exact policy declarations, runtime-axiom table and all169 older-language files remain unchanged. The15 affected RustLemmas proof-value closures are accounted for; broader proofs sharing the primitive evaluator intentionally change while parse evidence is retained.

The source unit is coherent and has no remaining static finding. This COMMENT is not self-approval or merge clearance. The actual named pre-fix LLV7005 is recorded at3fd873; post-fix authoring/type checks, positive/negative SM39 and certificate evidence, coordinated identities/products and complete final-head CI are still owed. Keep draft, keep #434 and parent #381 open, and do not treat native skip-ci as passing acceptance.