[sam-xif]

Summary

Closes #22. The boot metaclass ids and the one concrete control-heap size are now
derived rather than pinned, so adding a bootstrap class no longer requires hand-editing
them.

Authored by Nori, an agent — both this code and this description.

What changed

Denote/Sem/Core/State.lean — intMetaId/strMetaId. These are the metaclasses
Integer === x and String === x dispatch through. They were literals (76/85)
that PR #21 had to move to 87/96 by hand when the VFS step-1 classes shifted every
later id. They are now opaque definitions read off Semantics.bootedMachine:

opaque intMetaId : ObjId :=
  match Semantics.bootedMachine with
  | .ok m => classOf m.heap (.ref Boot.integerId)
  | .error _ => 0

opaque is the load-bearing choice: proofs that mention the ids treat them as
constants, so none unfolds the prelude, which the kernel cannot reduce (checked —
by decide gets stuck on Semantics.bootedMachine, while #eval evaluates it through
the compiled boot). The value is fixed once at definition time and stays 76/85, so
the corpus and the gate are unchanged.

The derivation is still checked, not merely computed: coreDataB's
classOf h intId == intMetaId is evaluated at the booted heap by #guard bootOkB, and a
new #eval reports the offending id and value if the derivation lands on 0 or a
non-class object — closing acceptance criterion 2 with a message instead of a bare
did not evaluate to true:

error: intMetaId derived as 0: the boot heap has no eigenclass for it

Denote/Controls/ConstantReachControls.lean — control-heap size. The literal
Array.replicate 47 (the same fragility: #21 bumped 47 → 48) is now
Boot.mainId + 3, expressed in terms of the id it sits just past.

notes/ratchet/implementation-notes.md — a short entry recording the change.

Verification

cd ruby-lean && ./scripts/run_typed_ratchet.sh — RATCHET GREEN:

• active clinks 125/125; 0 gated
• corpus agreement 256 agree, 0 disagree
• corpus rungs 131/263 accepted; negative controls 46/46 rejected
• ./scripts/run_clink_rebuild.sh also PASS on its own, same standard-axiom audit

The derived ids were confirmed to equal the literals they replace (76, 85), so no
observable behavior changes.

New issue filed

#46 — make gen-check is not run by any CI job, and make gate silently regenerates a
stale Prelude.lean, so generated-source drift can reach main green.

[jiro-by-nori]

Superseded by #84: the same change rebased onto current main, plus the constant-reach control's expected fresh object id derived from Boot.mainId instead of pinned to 48. This branch conflicts with main now, so #84 is the version to review.

[jiro-by-nori]

Superseded by #84, which makes the same change to the same two files against current main and is green and mergeable; #84's own description says it supersedes this one. Closing the stale copy so #22 has a single pull request to review. The branch remains if anything here is worth lifting.

_{Closed by Jiro, an autonomous coding agent.}