CORE32_PROOF_GUIDE.md
Machine Native Reasoning
CORE32_PROOF_GUIDE.md
1 # Exact memory for partition evidence
2
3 The current state is a candidate set V of possible worlds. Evidence filters this
4 set by intersection. The target map t supplies the values that remain possible.
5 A correction signature records these possible values after every admitted event.
6
7 For a cell map c, admitted events are exactly preimages of sets of cell labels.
8 The actual EvidenceAlgebra proves the total-event and intersection laws. Its
9 event collection includes each single cell and excludes events splitting a cell.
10
11 An attainable pair is (c(w),t(w)) for some world w. The pair type is the range of
12 this map, not the entire product of cell labels and target values. In particular,
13 unused target values do not add bits. The ambient target type need not be finite
14 or fully attained. Finite worlds make the attained pair type finite.
15
16 ## Classification
17
18 Occupancy records which attained pairs meet V. A single-cell query and one target
19 value recover membership of each pair from the signature. Conversely, for a union
20 of cells, the occupied pairs with cell label in the union determine exactly the
21 remaining target values. Thus signature equality is equivalent to occupancy
22 equality, including empty candidates and contradictory results.
23
24 Every occupancy S is realized by taking the full preimage of S under the map from
25 worlds to attained pairs. This differs from the written proof's choice of one
26 representative per pair, but realizes the same records. Surjectivity onto the
27 attained range gives every included pair, and the fibre definition excludes all
28 others. `memoryEquiv` is an actual equivalence between attained signatures and
29 subsets of the pair type. It gives the exact count 2^r.
30
31 ## Fixed binary memory
32
33 Choose a finite enumeration of the r attained pairs. Its occupancy indicator is
34 an r-bit vector. The readout takes target values of occupied pairs. A cell-union
35 filter removes pairs outside its cells. The Lean definitions prove exact readout
36 and update, including every finite event sequence.
37
38 For a competing exact memory using b bits, the inherited correction contract
39 forces different signatures to initialize different retained states. Equivalently,
40 compose occupancy realization with its encoder to obtain an injection from the
41 2^r occupancy records into the 2^b bit strings. Binary cardinality monotonicity
42 gives r <= b. This is a worst-case fixed-width state bound on all candidate
43 subsets. It is not a variable-length, average-bit or runtime bound.
44
45 The formal construction uses classical finite enumeration. Its proof of finite
46 encoding does not certify a compiled memory implementation or its performance.
47
48 ## Source and boundaries
49
50 The source endpoint retains the raw world, cell and target maps and the
51 nonempty-cell hypothesis as surjectivity. The internal classification is valid
52 even with unused cell labels because it counts attained pairs only.
53
54 The source sensor has eight worlds, four cells and four attained pairs, giving
55 sixteen signatures and four necessary and sufficient bits. Its current target
56 set can coincide for two candidates that later calibration separates. Additional
57 examples test mixed-target cells, repeated targets across cells, unused targets,
58 one-cell constant targets and empty worlds. Negative controls test removal of
59 single-cell evidence, evidence splitting a cell, and a too-short fixed-bit claim.
60
61 Source: `source/core_v0.2.tex`, `r:occupancy`, with the immediately preceding
62 partition-evidence setup. Formal entry points are in `THEOREM_MAP.json`.