The report-identity core: what is proved, and what is not

This note is the technical companion to the programme. It states the formal objects, the load-bearing results, the negative control, and the scope conditions. It describes the report-identity core, which is a six-module subset of this repository under report-core/. The full 56-file / 467-theorem corpus is under lean/; the counts are separated in §5.

1. Objects

Let Ω be a state space. A closure operator on Ω is a map

\[ C:\mathcal P(\Omega)\to\mathcal P(\Omega) \]

that is extensive (S ⊆ C(S)), monotone (S ⊆ T ⇒ C(S) ⊆ C(T)), and idempotent (C(C(S)) = C(S)). The closed sets are Fix(C) = {S : C(S) = S}.

A report family is a set R ⊆ P(Ω). It is the family of state-sets the system is willing to report as closed, not a single runtime string. The runtime report is one element of R.

From any report family define

\[ c_R(S)=\bigcap{T\subseteq\Omega : S\subseteq T,\ T\in R}. \]

A family is Moore when

\[ \mathrm{Moore}(R):=\forall F\subseteq R,\ \bigcap F\in R. \]

The empty intersection is Ω, so a Moore family always contains Ω. This is the corrected v1.1 condition. The v1.0 condition UpClosed (∅ ∈ R, closed under supersets) is degenerate in Lean: it forces R = Set.univ, so the v1.0 mutual-determination theorem is a tautology. The audit is retained under audit/ and is not imported.

2. The results

2.1 c_R is always a closure operator

theorem isClosure_repClosed (R : Report Ω) : IsClosure (repClosed R)

No precondition on R. The proof uses only the definition of c_R as an intersection. This is the construction side: every report family generates a closure.

2.2 Moore families determine their closure

theorem rep_eq_iff_closureOperator_eq {R R' : Report Ω}
    (hR : Moore R) (hR' : Moore R') :
    repClosed R = repClosed R' ↔ R = R'

On Moore families, the report family and the closure operator are two presentations of one object. This is the weak form: co-generation. Neither can be varied independently while the other is held fixed.

2.3 Report family = closed-set family

theorem report_eq_fix_iff {I : Set (Ω → Ω)} {R : Report Ω} (hR : Moore R) :
    R = {T : Set Ω | Inv I T} ↔ repClosed R = clos I

For a closure generated by an intervention family I, the report family is exactly the family of I-invariant sets if and only if the report closure equals the intervention closure. This is the strong form: a joint fixed point, not merely a mutual function.

2.4 The representation theorem

theorem moore_iff_exists_closure (R : Report Ω) :
    Moore R ↔ ∃ c : Set Ω → Set Ω, IsClosure c ∧ R = Fix c

Every Moore family is the fixed-point family of some closure operator, and every closure operator has a Moore fixed-point family. The theorem is a representation result. It does not identify the closure with a pre-existing operator such as the sharpness closure; that is a separate alignment problem (see §4).

2.5 The negative control

theorem nonMoore_not_canonical :
    ∃ R : Report (Fin 2), ¬ Moore R ∧ R ≠ Fix (repClosed R)

The witness is R = P(Fin 2) \ {∅}: all subsets of a two-element set except the empty set. It is not Moore, and it is not the fixed-point family of its own closure. This is the precise sense in which the Moore condition cannot be deleted. The counterexample does not say anything about the attribution presheaf or the potential; it is a report-family counterexample.

3. The gate

The formal results are conditional. The engineering question is whether the condition can be made a legal transition constraint rather than an after-the-fact check.

A candidate bundle carries:

C          closure operator
R          report family
report     runtime report (an element of R)
evidence   state/trace/certificate supporting the decision
version    monotone version
parent     hash of the previous committed bundle

The consistency gate checks R1–R7:

R2 is REVIEW rather than REJECT because a non-Moore family does not make the system "broken"; it means the system cannot claim the boundary–report identity until the family is repaired or the claim is withdrawn. R6 is a property of the candidate generator, not of a single candidate; the reference implementation wraps it in gate_candidates.

Atomic commit means there is no legal state in which C is committed without the matching R, report, evidence, and version. The action gate accepts only a committed bundle and denies actions that require a different version or leave the committed closure.

This is a reference implementation over finite state spaces. It is not a deployed agent and not a proof that a production system cannot bypass the gate. The tests are a protocol check, not an empirical validation.

4. What is not proved

The report-identity core is deliberately narrow. Four open items matter for reading it correctly.

4.1 The attribution-to-closure bridge

The programme's first layer uses an attribution presheaf A : Caus^op → Δ²; the core starts from a closure operator C. The current Lean development does not construct C from A. The attribution module and the closure module are separate. A route assessment (stable fibers, Moore families, point-vs-set closure levels) concludes that the missing step is not a single lemma: it requires an actual attribution section, a value predicate, and a path-compatibility condition. This is the next theoretical target, not a result of this repository.

Do not cite the Moore core as having derived the boundary from attribution.

4.2 The level parameter

The sharpness closure c(κ, μ, w) depends on w/κ. The potential V(κ) fixes κ* but does not fix w. The current gate must therefore take w as an input or adopt a separate selection principle. The claim "the level is uniquely determined" is not part of this core.

4.3 A7 and the potential

The form V(κ) = c₀κ + αC_F/κ is a model-class theorem under A7 (maintenance cost is a continuous additive functional). It is not a consequence of the free category's universal property. The A-module's 33 declarations are a separate scope; they are not this core's count.

4.4 Production behaviour

The gate's acceptance/rejection rates on a realistic task are unknown. A gate that always accepts is decoration; one that always rejects is unusable. The finite-state tests do not settle this.

5. Evidence and reproduction

The report-identity core has no sorry, no admit, and no custom axioms. The full corpus was verified separately (71 modules, 9/9 checks); its log is in this repository. Do not mix counts across scopes.

Build:

lake update
lake exe cache get
lake build

Offline:

MATHLIB_PACKAGES=/path/to/.lake/packages ./scripts/verify_offline.sh

Gate:

python3 architecture/gate_reference.py

The site is static; python3 site/build_site.py regenerates it from docs/.

6. Reading order

1. README.md — the claim and its refusals.
2. docs/PROGRAMME_EN.md — why the claim matters.
3. This note — what is actually machine-checked.
4. lean/ReportIdentityCore.lean — the main definitions and results.
5. lean/ReportCountermodelsCore.lean — the negative control.
6. architecture/PROTOCOL.md — how the condition becomes a gate.
7. docs/EVIDENCE.md — hashes, counts, and open items.