[Property tracking] improved design: replace prose marker with typechecked statement-proof pair

## Context

PR #1226 (issue #1225) introduced the property catalog (`build-tools/scripts/property-tracking/properties.yaml`), the scanner (`build-tools/scripts/property-tracking/scan_properties.py`), and the generated dashboard.

**Status** of each property is derived, never declared:

+ no module → `idea`;
+ module named but module file absent → `planned`;
+ module file exists and contains the phrase "coming soon" → `stated`;
+ otherwise → `proved`.

The Agda `--safe` typecheck in the main CI guarantees that whatever Agda exists has no holes or postulates; the scanner guarantees the bookkeeping matches the files.

## Problem

The `stated`/`proved` distinction rests entirely on a prose marker. A module could formally state a property as an uninhabited type definition (e.g. `pp-wellFormed-invariant : Type` in `src/Ledger/Conway/Specification/Chain/Properties/PParamsWellFormed.lagda.md`), which typechecks cleanly. If the `*Proof*. (coming soon)` line is dropped or forgotten, the dashboard reports the property as ✅ proved with every CI job green: a false positive in the dangerous direction, caught by nothing automated. Some of the currently-stated Conway properties have this shape.

## Proposed re-design

Make the statement and the proof separately named artifacts, record both names in the catalog, and let the typechecker, not prose, certify the relationship between them.

### Catalog

In the `properties.yaml` catalog,

+ each record represents a single property;
+ rename `defs` to `def`; this field will contain a single value instead of a list; it is the name of the **type** that defines the property.
+ add a field called `proof`; it contains a single value: the name of the inhabitant of the type named in `def`.

Each entry continues to describe exactly one property. Replace `defs` (a list, currently decorative) with two scalar fields, as in the following example:

```yaml
- id: conway-ledger-pov
title: "LEDGER preserves value"
era: conway
sts: LEDGER
module: Ledger.Conway.Specification.Ledger.Properties.PoV
anchor: thm:LEDGER-PoV
def: LEDGER-pov # the property, stated as a type
proof: LEDGER-pov-proof # the inhabitant of that type
issues: [1238]
notes: ""
```

`def` names the property definition **as a type**; supporting lemmas stay out of the catalog; where a module proves several, the entry names the headline theorem only (though we should be able to have multiple yaml records for a single module).

### New rules for determining status

+ `module` field empty → `idea`;
+ `module` field nonempty but module file absent → `planned`;
+ module file exists but `def` field is empty → `planned`;
+ module file exists, `def` field nonempty →
+ `proof` field empty → `stated`
+ `proof` field non-empty it names an inhabitant of the type named in `def` → `proved`

### Module convention

Each property module states the property as a type definition and proves it with a literal one-line ascription; for example, instead of what we have now:

```agda
LEDGER-pov : {Γ : LEnv} {s s' : LState}
→ txId ∉ mapˢ proj₁ (dom (UTxOOf s))
→ Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'

LEDGER-pov
{s = s}
{s' = s'}
h (LEDGER-V {utxoSt' = utxoSt''} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , _ )) =
-- abridged --
```

we would change the Ledger PoV type/proof to the following format:

```agda
LEDGER-pov : Type
LEDGER-pov = {Γ : LEnv} {s s' : LState}
→ txId ∉ mapˢ proj₁ (dom (UTxOOf s))
→ Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → getCoin s ≡ getCoin s'

LEDGER-pov-proof : LEDGER-pov
LEDGER-pov-proof
{s = s}
{s' = s'}
h (LEDGER-V {utxoSt' = utxoSt''} ( valid , UTXOW⇒UTXO st@(UTXO-induction r) , h' , _ )) =
-- abridged ---
```

That way, the `scan_properties` script really only has to check that the line `LEDGER-pov-proof : LEDGER-pov` appears to confirm that the property is proved.

More generally, if a yaml record has

```yaml
- id: conway-ledger-property
def: PropertyType
proof: PropertyProof
```

Then the scanner must find a line containing the string `PropertyProof : PropertyType`.

Read build-tools/scripts/property-tracking/properties.yaml and build-tools/scripts/property-tracking/scan_properties.py, then inspect the example module src/Ledger/Conway/Specification/Chain/Properties/PParamsWellFormed.lagda.md. Update catalog records and property modules to use scalar def/proof names, and make the scanner recognize a proof line such as `PropertyProof : PropertyType`; done means statuses are derived from these typechecked statement-proof pairs rather than prose markers.

Written by the indexing model from the issue text.