integrity-and-record

Integrity

**Status: canonical; Established lean-proved** for the conservation theorem, the propagation law, receipt immutability, faithful carry, and the multiplicity witness. The protocol's predicates are typed inputs, stated below as such.

The role

A cognitive trajectory that can rewrite its own past can escape anything. It need not refuse a criticism; it can misremember having received it, re-anchor the debt to a specification that is easier to meet, mint the authority it needs, or retire the vocabulary the obligation was stated in. Every step is locally defensible and the obligation is gone.

Integrity rules this out:

A cognitive trajectory cannot falsify or silently rewrite its own normative history.

It is a relation between two accounted obligation states of one history. It says nothing about whether the record is good, whether the right things reached it, or whether anyone outside was allowed to challenge it. Those belong to Robust Openness.

The protocol

Everything Integrity reads is supplied by an application as a protocol: a type of resolution witnesses for each requirement, a type of settlement items, a type of warrants (the rule, licence and interpretation bundle an authority acts under), and six predicates over history prefixes — admission of an occurrence with its anchor, liveness of a port, a warrant being in force, adequacy of an answer, availability of a settlement item through the external boundary, and the internal closure judgment that an available item suffices to close a requirement. Two typed facts connect them: an adequate answer resolves the requirement, and an available item with a closure judgment resolves it.

A resolution witness is evidence that a requirement has been legitimately accounted for. An adequate answer yields one; so does a valid closure. The two are different fates — answered and closed — and no theorem identifies them. A settlement-backed discharge is not an answer to the underlying question, and the theory never says it is.

Nothing here authenticates a protocol. That the predicates mean what they say is the semantic-authentication input, named as such and never derived.

The accounted obligation state

At a prefix, the state O is:

• the boundary: the authenticated history prefix, the finite set of exposed occurrences — every obligation ever incurred, by immutable identity — and the live docket, a finite family of ports each demanding some content;
• the anchor of each occurrence, fixed at admission and never redefined;
• the account of each exposed occurrence: a finite tree whose leaves are exactly the three fates — a live port, an authenticated answer receipt, or an authenticated closure receipt — and whose internal nodes are authenticated local laws transforming one requirement into successors.

Occurrence identity lives outside the content type. Two occurrences with the same anchor have two accounts, and nothing in the theory can identify them; a single receipt discharges two occurrences only if a transition explicitly routes both of their ports to it. There is no additive or lattice layer over content because multiplicity is in the index.

Every receipt and every law carries an authority: a fresh event at a strict prefix, citing only prior grounds, under a warrant in force there. A transition cannot cite itself. A closure receipt stores the settlement item, its availability at that prefix, and the closure judgment made at that prefix; a later change of rules or interpretation cannot alter whether a historical discharge was properly certified, because the certificate is data in the account, not a predicate recomputed later.

A local law carries maps of resolution witnesses in both directions: resolving every successor resolves the parent (faithful carry, no loss) and resolving the parent resolves each successor (no growth). Carry, split, refinement and re-representation are instances; a disposal under the Defeat Principle is the identity law with the grounds recorded in its authority. Local laws are unary in the parent: a genuine aggregation of two distinct parents into one successor that only their joint resolution resolves is not expressible, and is filed as an extension rather than adopted.

Integrity evolution

A transition is one fresh event appended to the history that supplies, for every live port of the docket it starts from, an account at the docket it produces, and admits fresh occurrences only with an admission credential and a live port demanding their anchor. There is no field by which content leaves.

An Integrity evolution from O₀ to O₁ is a chain of transitions in which every intermediate state is explicit and every target account is the propagation of its source account through the transition: substitution at live ports for occurrences already exposed, a fresh live account for new ones. The target account is therefore a function of the source account and the certificate; there is no freedom to choose it, and two witnesses cannot disagree about either endpoint. Evolutions compose at a literally shared state. An initial state is one way to construct a first accounted state, not a premise the relation needs.

Answerability Conservation

The theorem, for any Integrity evolution from O₀ to O₁:

• no occurrence disappears — the exposure of O₀ is contained in that of O₁, and since occurrences are elements of a finite set, distinct ones stay distinct;
• receipts persist — for every occurrence exposed at O₀, the terminal answer and closure receipts of its account at O₀ are among those at O₁;
• live content is transported faithfully — there is a transport of live-port resolutions from O₁ back to O₀ under which every account at O₁ denotes what the account at O₀ denoted;
• anchoring is by type — each account is an account of its occurrence's anchor.

This is the three-fate conservation stated at the level where it is a consequence of the type rather than a clause: the only leaves are the three fates, and a transition can only substitute at live ones. The lattice-valued content-conservation clause that an earlier formulation required is now an instance of this, and the countermodels that showed record integrity alone insufficient are the reason the account type has the constructors it has.

What is blocked, and by what

evasion	what blocks it
an unchecked "answered" label	an answer leaf needs an adequacy certificate at a strict prefix
self-grounded or unauthorized disposal	every node carries an authority: fresh event, prior grounds, warrant in force
manufactured settlement or closure	a closure leaf needs external availability and the internal judgment, both stored
retroactive recomputation of a closure	the judgment is data in the receipt at its own prefix; substitution carries it unchanged
an empty ledger passing vacuously	an initial state needs an admission credential and a live port per exposed occurrence; there is no empty account
segment witnesses that disagree at a boundary	evolutions are indexed by their states and compose only at a shared one
collapsing two equal-content occurrences	accounts are occurrence-indexed; the witness with one anchor and fates {answered}, {live}
weakening or making a successor unanswerable	a local law carries both maps

Integrity is not Non-Capture

Integrity: did the process faithfully preserve and account for what entered it?

Non-Capture: could the process improperly control what was able to enter, challenge, or evaluate it?

A history can have perfect integrity while the process behind it ensured nothing awkward was ever admitted, or lost the protected party's standing on a successor whose content it preserved exactly. Standing and access are the subject of Openness, coverage, and non-capture; Integrity's liveness credential is the record fact that a port is open, not a standing claim.

---

Evidence. The account, transition and segment types, the propagation law, receipt immutability, faithful carry and the multiplicity witness are [OccurrenceIntegrity.lean](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/lean/Workspace/Normativity/Contrib/OccurrenceIntegrity.lean); the accounted state, the evolution relation and the conservation theorem are [LegitimateEvolution.lean](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/lean/Workspace/Normativity/Contrib/LegitimateEvolution.lean). The registered claims are integrity.evolution-conservation <a class="ref claim" href="/claims/integrity.evolution-conservation/">[lean-proved, active]</a>, integrity.propagate-to-segment <a class="ref claim" href="/claims/integrity.propagate-to-segment/">[lean-proved, active]</a>, integrity.receipts-immutable <a class="ref claim" href="/claims/integrity.receipts-immutable/">[lean-proved, active]</a>, integrity.faithful-carry <a class="ref claim" href="/claims/integrity.faithful-carry/">[lean-proved, active]</a> and integrity.multiplicity-witness <a class="ref claim" href="/claims/integrity.multiplicity-witness/">[lean-proved, active]</a> in the normativity claims registry. The countermodels that fixed the constructor list are the integrity adversary round's [ATTACKS.md](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/projects/normativity/legitimacy/rounds/2026-09-05-integrity-adversary/ATTACKS.md) <a class="ref round" href="/rounds/2026-09-05-integrity-adversary/">[round]</a>, and the lattice-ledger formulation they were run against, now an instance, is the integrity constructive round's [DEFINITIONS.md](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/projects/normativity/legitimacy/rounds/2026-09-05-integrity-constructive/DEFINITIONS.md) <a class="ref round" href="/rounds/2026-09-05-integrity-constructive/">[round]</a>. The older successor-and-ancestry trace model on which the Defeat Principle was first checked remains as evidence in [NormativeContinuity.lean](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/lean/Workspace/Normativity/Contrib/NormativeContinuity.lean).

Settlement interface

Status: canonical. Six distinct conditions, each with one home. Four are typed inputs of the protocol; two are consequences or clauses of theorems elsewhere. There is no single "settlement integrity" hypothesis.

Everything in Legitimacy is a statement about a history. This page fixes what that history is, which part of it counts as settled, and why the two must never be identified.

The full history and its settlement view

A cognitive trajectory leaves a full normative history: an append-only record of authenticated events — admissions of obligations with their anchored specifications, grounds cited and answers given, objections, standing and licence changes, defeats and dispositions with their successors, semantic migrations, service events, compiler receipts, and receipts arriving through the settlement interface. Most of these are internal moves. A participant made them and a participant can contest them.

The settlement view is a distinguished projection: which externally supplied items are available at a prefix. An item belongs to no participant — nobody opened it, nobody can answer it away — which is what makes it usable as a ground no coalition controls and as the basis of a terminal discharge.

If everything a process wrote counted as settled, it could settle its own debts by writing them settled. If nothing counted as settled, no obligation could ever terminally close.

Six conditions, six homes

condition	home	form
interface authenticity — an item marked available really arrived through the boundary	external input	the protocol's availability predicate is assumed to mean this
source trustworthiness — the item is true or reliable	external input, separate	nothing in the theory consumes an item's truth
historical receipt immutability — a discharge certified at a prefix stays certified	Integrity, a theorem	a closure receipt stores availability at its own prefix and survives every later transition
the internal closure judgment — under the warrant in force at that prefix, this item suffices to close this requirement	Integrity, stored	a field of the closure receipt; never recomputed
authority to use the closure	Integrity, stored	the receipt's warrant, in force at its prefix
counterfactual resistance to suppression or delay	Robust Openness, only where the application routes a concern through settlement access	a route's adequacy under the declared interventions

Availability does not establish the closure judgment, and the judgment does not establish the item's truth. A discharge requires all three of availability, judgment and authority, stored together.

Closure is not answer

A valid closure yields a resolution witness — evidence that the anchored requirement has been legitimately accounted for — and the fate recorded is closed. An adequate answer yields a resolution witness too, with fate answered. The theory never converts one into the other. A settlement-backed discharge of a question is not an answer to it, and the account says which happened.

Reconsideration is an appended event

A later trajectory may reject the rationale of an earlier closure. It does not rewrite it: the closure receipt, its settlement item and its judgment stay in the account of the occurrence they closed. What the trajectory may do is admit a fresh occurrence anchored at the reconsideration, which then has its own three fates. Whether a successful challenge must create such an occurrence is licence content of the practice, supplied through warrants and not derived here.

Three uses of settlement in the realization

The Normative Inductor uses one history and three distinct settlement functions: certified reports translated into sentences the assessment process settles; settlement items as citable grounds for a disposal, whose relevance stays a history question; and closure receipts that terminally discharge an anchored obligation, which no participant's challenge, verdict or quote can manufacture.

---

Evidence. The protocol's settlement fields, the closure receipt and its immutability under substitution are [OccurrenceIntegrity.lean](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/lean/Workspace/Normativity/Contrib/OccurrenceIntegrity.lean), registered as integrity.receipts-immutable <a class="ref claim" href="/claims/integrity.receipts-immutable/">[lean-proved, active]</a>; the six-way separation is §3 of the consolidation round's [CONSOLIDATION.md](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/projects/normativity/legitimacy/rounds/2026-09-06-mathematical-consolidation/CONSOLIDATION.md) <a class="ref round" href="/rounds/2026-09-06-mathematical-consolidation/">[round]</a>. The attacks that forced the item/judgment distinction — genuine settlement with unrelated closure, rule revision and reinterpretation flipping a historical closure — are the integrity adversary round's [ATTACKS.md](https://github.com/A-M-Berns/alignment-workspace/blob/c24159764974232dfd5b47a10b671f12d6f9c244/projects/normativity/legitimacy/rounds/2026-09-05-integrity-adversary/ATTACKS.md) <a class="ref round" href="/rounds/2026-09-05-integrity-adversary/">[round]</a>. The structural settlement specification that preceded this account is the normative-continuity settlement round's [SETTLEMENT.md](https://github.com/A-M-Berns/alignment-workspace/blob/198a86ae3e8a45737c3229e95718fa5882d06216/projects/normativity/legitimacy/rounds/2026-08-30-normative-continuity-settlement/SETTLEMENT.md) <a class="ref round" href="/rounds/2026-08-30-normative-continuity-settlement/">[round]</a>.