Authored delta expected

The check is authored_delta_expected. It is IMPLEMENT-stage. It warns. It does not fail the merge. You can still advance. It looks at implementation files changed in the current branch and asks a narrow question: is this file owned through implemented_by, and if so, did one of those owners change in this branch, or did a linked documented_by artifact change. If a changed traced file has neither kind of linked review delta, the check warns. For changed non-test files, changed verified_by artifacts alone do not clear it. Tests are supporting evidence, not the primary impact-review record for production code. It does not write the YAML. It does not prove the Go.

The blast-radius hop stays on software change impact analysis. That hop is the table of neighbors. This hop is whether the file that moved has a current no-authored-change stamp, or a real spec delta. The backing hop stays on change evidence complete. The branch brief stays on pull request review. The stale-link hop stays on suspect clean. Description-only edits belong to description_delta_reviewed, not this URL.

Each neighbor can look fine on its own. The impact table still lists the file. The extra tests are green. Reviewers signed the English in another tool. The expensive miss is a production file that moved while the shall stayed byte-for-byte the same, with nobody recording that that was the claim.

# SYS-REQ-185  traces.implemented_by: pkg/cache/ttl.go
#              fretish, variables, acceptance: unchanged
# ttl.go edited this branch. tests/ttl_test.go edited too
# a suite-only hop
# pass. the extra tests are green
# proof audit --check authored_delta_expected
# [IMPLEMENT] authored_delta_expected
# SYS-REQ-185:pkg/cache/ttl.go has no authored review delta
# WARNING
# proof help authored_delta_expected

Classify the change before you reach for a stamp. A new flag, grammar token, default, or any new externally-observable behavior is an authored-contract change: update the spec, or file a proof problem-report DEFECT plus the regression test. Do not record no-authored-change over that. A true refactor, same surface, is the narrow case. Then start with the owning requirement.

proof review req SYS-REQ-185
proof review impact SYS-REQ-185 --decision no-authored-change --reason "Reviewed implementation impact; requirement and documented design remain correct"
proof audit --check authored_delta_expected --verbose
proof help authored_delta_expected

The teaching graph is still one requirement that lists ttl.go and one production file that moved without a linked spec or design delta. Close it by updating the shall, updating a linked documented_by artifact, filing a DEFECT for a restoring fix, or recording proof review impact only after you confirmed the surface did not change. The stored pair is the file's sha256 and the requirement's authored-content fingerprint (fretish, variables, acceptance, satisfies, components, interface, assumption, custom fields). Approval metadata and the prose description are outside that fingerprint. Description-only edits belong to description_delta_reviewed. Editing any line of a shared file re-opens every owner pair of that file. Overlay-audit projects do not use this check as a source-native no-authored-change gate.

# SYS-REQ-185 kept. impact review fingerprints match ttl.go
# proof audit --check authored_delta_expected
# 0 authored-delta findings
# IMPLEMENT may move on. pass sits on a current stamp

The blast-radius hop stays on software change impact analysis. The rewrite hop stays on characterization testing and mirrors. Jama still authors. Proof vs Jama.

Warning when a traced production file moved without a linked requirement or documented_by delta, and without a current no-authored-change stamp on that pair. Default severity does not fail the merge. You can still advance. Zero in-scope findings is a pass, not a proved graph. Direct implemented_by ownership only; the check does not guess semantics from the code. Tests alone do not clear production-code changes. Overlay-audit mode does not use this check as a source-native gate. Compound shared files re-open every owner because the fingerprint is whole-file. Symbol-granular artifact fingerprints remain a recorded long-term improvement, not this hop. The hop does not write the impact review. It does not add a shall. It does not write a description. It does not prove the Go. It does not invent an Implements line. A quiet hop is not a proof that Jama's shall matches the Go, only that every in-scope pair currently has a linked delta or a current stamp. We have not scored this floor against a frozen Jama pack or a VectorCAST corpus. The loss is named, not scored.

The blast-radius hop stays on software change impact analysis. The rewrite hop stays on characterization testing and mirrors. The engagement stays on software correctness audit. Jama still authors.

What is authored delta expected? Same question. Same URL.

Is this software change impact analysis? No. That hop is the table of neighbors. This hop is whether the file that moved has a current impact stamp or a real spec delta. See software change impact analysis.

Is this change evidence complete? No. That hop is whether the declared change type still has its backing. This hop is the (requirement, file) pair. See change evidence complete.

Is this suspect clean? No. That hop is a live link newer than traces.reviewed_at. This hop is a branch-aware authored delta. See suspect clean.

Is this a pull request review? No. That hop is the brief for the whole branch. See pull request review.

Is this no authored change surface reviewed? No. That hop reports a present no-authored-change stamp over new public surface. This hop reports a missing stamp. See no authored change surface reviewed.

Is this description delta reviewed? No. That hop reports a FRETish-backed description that moved while the formula stayed put. This hop reports a missing stamp on a moved production file. See description delta reviewed.

Do extra tests clear a production-file change? No. Changed verified_by artifacts alone do not clear this check for non-test files.

Is a new flag a no-authored-change? No. A new flag, grammar token, default, or any new externally-observable behavior is an authored-contract change. Update the spec, or file a DEFECT.

Does a quiet hop prove the Go matches the shall? No. The hop observes linked deltas and fingerprints. It does not prove the Go.

Does this finding fail the merge? No by default. The check keeps warning severity. You can still advance.

Is overlay-audit in scope? No. Overlay-audit projects do not use this check as a source-native no-authored-change gate.

Is this characterization testing? No. That page is rewrite-with-a-ledger. This hop is a missing authored delta. See characterization testing and mirrors.

Is Proof an LDRA alternative for the instrument? No. LDRA still owns the avionics toolchain. Proof vs LDRA.

Is Proof a Jama alternative for the shall? No. Jama still authors. Proof vs Jama.