INDEPENDENT AI MATHEMATICAL REVIEW — ITERATION 1
Reviewer: Codex child agent /root/review_continuity
Access/review date: 2026-11-04 (Asia/Bangkok)
Scope: proposed mathematical setup and theorem statements supplied by the parent;
not a review of an already completed report. This is AI review, not peer review.

VERDICT
The proposed claims are correct under the explicit deterministic, finite,
known-model contracts. No new general automata, zero-error coding, or personal
identity result should be claimed. The strongest useful outcome is a carefully
typed comparison and an eight-case independence theorem for lineage, memory
preservation, and task prediction. Coordinator steering assigns active diagnostic
trees, origin-current beliefs, and repair-cost distinctions to the separate
causal thread; automata and logging checks below are supporting antecedent checks,
not a proposed main identity contribution.

1. RELATIONS AND TYPES
The memory criterion ker(s) subset ker(r), for maps r and s on one fixed finite
counterfactual domain H, is equivalent to existence of d with r=d composed with
s. Proof: define d on each attained s value by the common r value of its fiber;
fiber constancy is necessary and sufficient. This is reflexive and transitive,
but generally asymmetric. Preserve the common H when composing comparisons;
redefining H or the target record between stages invalidates that simple proof.
A record on a singleton actual history makes the criterion vacuous, so the
counterfactual family must remain explicit. Information preservation permits
recoding and requires neither literal bit equality nor authenticity.

Lineage is an occurrence relation; predictive equivalence is a state relation;
memory preservation compares registers over H; recovery is an experimental
feasibility property. Call them operational continuity criteria/relations with
their domains stated, rather than presenting all four as competing equivalence
relations on exactly the same set. A process or physical survivor edge must be
supplied by an audit/event model. Behavioral data alone cannot identify that edge.
Copying is causal descent without uniquely selecting numerical persistence.

2. CENTRAL INDEPENDENCE THEOREM AND LINEAGE IMPOSSIBILITY
Let H={(v,m):v,m in {0,1}}, b(v,m)=v, and task tick(v,m)=(1-v,m).
Every future task-output word depends only on v, and the empty word distinguishes
v=0 from v=1. Hence predictive equivalence E is exactly equality of v.

The four supplied changes realize all memory/prediction combinations:
identity (v,m)->(v,m): memory yes, prediction yes;
erase (v,m)->(v,0): memory no, prediction yes;
flip (v,m)->(1-v,m): memory yes, prediction no;
reset (v,m)->(0,0): memory no, prediction no.
Memory compares the old m with the resulting m over all of H. A decoder from
constant zero cannot return both old memory values, which proves the two negative
memory entries. Predictive preservation is the uniform condition h E F(h), so the
two positive and two negative entries follow directly from the v coordinate.
Independently implementing each map on the audited surviving carrier or on a
fresh carrier realizes all eight (lineage,memory,prediction) triples. Thus no
nontrivial Boolean implication among these three predicates is valid over the
declared model class. This is a complete elementary independence proof, not a
claim that real implementations permit every combination under every resource
constraint. The supplied lineage designation is independent data by construction.

Clarification: prediction compares future outputs from the two checkpoints under
the same task-action suffix. It does not mean that the mechanism/update rule is
unchanged or that the state followed its normal trajectory. Even the normal tick
preserves the task rule but changes v and fails this checkpoint prediction test.
That distinction should be explicit in the reader-facing report.

The black-box lineage impossibility is valid: two admissible histories can have
different lineage labels but identical full interface response functions. At any
equal observed history, a deterministic tester selects the same next instruction,
and both worlds return the same next output. Induction yields identical terminal
transcripts and reports. Coupling a randomized tester's state-independent random
seed proves identical report laws too. It cannot be surely correct in both worlds;
for binary labels its two error probabilities sum to at least one. This assumes
that ALL permitted observation/diagnostic ports are included in the matching
interface. A trusted provenance channel can invalidate the premise and permit
identification. No impossibility follows from matching only ordinary task outputs.

The copying-axiom conflict needs three explicit axioms: I is an equivalence;
both copies satisfy I(parent,copy_i); and distinct simultaneous tokens cannot
satisfy I. Symmetry and transitivity give I(copy_1,copy_2), violating the last
axiom. Equivalence alone is not contradictory: it can consistently group copies
into one class. Call the third axiom contemporaneous uniqueness, or similar plain
language. Causal ancestry can branch because it is not a numerical-identity
equivalence. A copy may preserve all records and predictions without receiving
the original audited survivor edge.

3. ORIGIN-PAIR PLANNING (SUPPORTING CHECK; CAUSAL-THREAD SCOPE)
The origin-current relation B is sufficient for the specified objective if all
enabled instructions depend only on its current projection (plus any explicitly
retained phase/resource variables). A terminal B must have one original target
label across ALL its pairs; one label per current state is insufficient unless
that state is actually observed. Empty outcome branches impose no requirement.

The recurrence is valid by induction on the maximal remaining number of steps.
For finite H,X and a finite instruction library, iterate the monotone predecessor
operator from terminal beliefs to its least fixed point. This captures bounded
sure termination. A deterministic protocol terminating on every possible initial
state has a uniform finite bound because the initial domain is finite. The bound
on all conceivable nonempty pair relations is 2^(|H||X|)-1; reachable relations
can be much fewer. If finite budgets, phases, consumed tests, or cumulative order
changes matter, include them in the planner state. Do not use the recurrence for
arbitrary history-dependent legality without that augmentation.

Critical overlap: the actual B-Theory acquisition manuscript already gives the
origin-current relation and its query/action updates in Section 7, immediately
before Example 11. Its origin/current separation is therefore an established
antecedent, not a newly introduced device. The proposed origin-target winning
condition is a direct standard extension of its current-target planning.

4. FIVE-STATE WITNESS (SUPPORTING CHECK; CAUSAL-THREAD SCOPE)
The witness works. Initial candidates h0,h1,h2 share output zero. Action ai sends
hi to output-one absorbing state z1 and every other candidate to output-zero
absorbing state z0. Any pair hi,hj is distinguished by ai, so the three candidate
origins occupy distinct predictive classes. Yet any first action has an outcome
zero branch with two origins that have become the same state. No later adaptive
action can separate that pair. Initial observation and indefinite waiting add
nothing. Under a uniform prior, the optimal one-run success probability is 2/3:
the singleton branch contributes 1/3 and the merged branch at most 1/3.

Two pristine instances in the same unknown initial state suffice: apply a0 to
one and a1 to the other. Output pairs for h0,h1,h2 are respectively (1,0), (0,1),
(0,0). This means two total experimental instances (one additional copy when the
original is retained), not necessarily two additional copies. Exact copying must
occur before the destructive probe; copying the merged z0 cannot restore origin.
Reset-to-known-state is different from reset-to-the-unknown-original-state.

Priority is especially clear here: Moore (1956), Theorem 1, printed pp.138–139
(PDF pages 11–12 counting the cover as page 1), establishes the general pairwise
distinguishability versus single-experiment gap and discusses multiple copies.
Use the new witness as an elementary worked instance, never as a new theorem.

5. PROTECTED RECORD / SIDE INFORMATION (SUPPORTING OBSERVABILITY CHECK)
If the decoder actually receives a fixed readout c(h), and z(h) is preserved and
readable, exact origin reconstruction is equivalent to injectivity of (z,c).
For an unrestricted encoder observing h, maximum c-fiber cardinality is the exact
minimum alphabet size: each fiber needs distinct symbols; labels can be reused
between fibers. Fixed-length bit count is ceiling(log2 of that cardinality).

For the restricted encoder z=g(r(h)) and target label ell, the proposed graph
criterion is correct, including self-loops. Two old-register symbols require
different colors precisely when a common c value can accompany different target
labels. Same vertex with such a conflict makes success impossible. Otherwise a
proper coloring supplies g and guarantees a well-defined decoder of (color,c).
This is the one-shot zero-error side-information construction; it is not a new
general logging theorem. For full origin and noninjective r, self-loops can make
recovery impossible even with an unbounded record alphabet.

Essential caveat: c=[f(h)]_E is NOT automatically an available readout. Predictive
classes are computed offline from tables, and the single-run witness shows that
their pairwise separation need not imply a safe common readout experiment.
Call this a trusted readout assumption or an oracle lower bound. Do not derive a
sufficient operational recovery criterion from this choice of c without proving
that c is actually acquired under the permitted dynamics. If readout depends on
an adaptive destructive policy, the confusability graph also depends on policy.

6. RECOMMENDED IDENTITY-SCOPE NEXT THEOREM
Ask which assumptions couple criteria that were independent in the four-state
example. A precise elementary characterization is available:

For a fixed finite task machine with behavioral equivalence E and memory map
r:X->M, every map F:X->X satisfying F(x) E x preserves old memory in the decoder
sense r=d composed with r composed with F if and only if r is constant on every
E-class.

Sufficiency: E-preservation and class constancy give r(F(x))=r(x), so d is the
identity on attained memory symbols. Necessity: choose a representative in each
E-class and let F send the whole class to that representative. If r varies on an
E-class, two different old records have the same new record, so no decoder exists.
This says that memory is automatically protected by task prediction only when
it contains no within-behavior-class distinctions that the task contract ignores.
The hypothesis quantifies over arbitrary known replacement maps; restrictions
on realizable maps change the necessary condition. This is ordinary quotient
factorization and should not receive a novelty claim without further work.

The next substantive problem is to replace arbitrary F by a specified family
of realizable replacements and find the exact memory-preservation condition.
This keeps the focus on copying, replacement, and continuity, and can use the
independence theorem as a negative control. A restricted family may permit
within-E memory that arbitrary class collapse would destroy.

7. OPTIONAL LOGGING EXTENSION (DEFER TO CAUSAL-THREAD COORDINATION)
Jointly minimize the protected record alphabet and worst-case probe depth when
the encoder sees only r(h), and post-change diagnostics can merge states. For a
fixed diagnostic policy, join register symbols whose differently labelled origins
produce the same terminal transcript; a coloring is then necessary/sufficient.
But an operational decoder may use the recorded color to choose different probe
policies. Thus minimizing a graph over color-blind policies can overestimate the
true memory requirement. Study this interaction explicitly in a small finite
model before claiming that a single fixed confusability graph solves it.

This is a concrete extension of the most useful theorem: logging and legal
experimentation must be optimized together. A small separation between a
color-blind-policy restriction and color-dependent adaptive diagnosis would be a
good next exact result. Novelty remains subject to targeted prior-art research
on feedback/interactive zero-error coding and automata testing with memory.

PRIMARY SOURCES READ (2026-11-04)
1. Brian Theory, From Observable States to Acquirable Predictive Models,
   revised 7 October 2026, Section 7 and provenance/related-work sections:
   https://www.b-theory.com/manuscripts-html/acquirable-predictive-models/
2. Edward F. Moore, Gedanken-Experiments on Sequential Machines, 1956,
   experiment definitions and Theorem 1:
   https://www.cs.cmu.edu/~cdm/resources/Moore1956-gedanken-experiments.pdf
3. Prashant Koulgi, Ertem Tuncel, Shankar L. Regunathan, Kenneth Rose,
   On Zero-Error Source Coding With Decoder Side Information, IEEE TIT 49(1),
   99–111, January 2003, introduction and coding/graph framework:
   https://web.ece.ucsb.edu/publications/rose/pubs/pub40-T-IT1-03.pdf
   DOI: https://doi.org/10.1109/TIT.2002.806154
   This primary paper explicitly credits Witsenhausen's 1976 graph construction;
   the original 1976 article was not independently read by this reviewer.

No code execution, external writes, publication, or human peer review occurred.

ADDENDUM: UNIVERSAL COUPLING THEOREMS (2026-11-04)
The parent requested a second check of the following exact universal statements.
Let X be finite and nonempty, E an equivalence on X, and r:X->M a memory map.
All maps F:X->X are admissible in this theorem. Write
P(F) iff F(x) E x for every x;
S(F) iff r composed with F equals r (literal record preservation);
M(F) iff r=d composed with r composed with F for some decoder d
(decoder-based record preservation).

All three proposed characterizations are correct, with no exceptional finite
nonempty cases:

(A) [For every F, P(F) implies M(F)] iff E subset ker(r).
If E subset ker(r), P(F) gives rF=r and hence M(F) with the identity decoder.
Conversely, choose one representative from each E-class and collapse each class
onto its representative. This F satisfies P. If two points in one E-class had
different original records, their equal final records would defeat every decoder.
Thus the universal implication forces E subset ker(r). This proof also shows
that the same condition characterizes universal P(F) implies S(F).

(B) [For every F, S(F) implies P(F)] iff ker(r) subset E.
The forward direction follows by taking any x,y with r(x)=r(y), mapping x to y,
and fixing every other point. That F satisfies S, so P forces x E y. The converse
is immediate from r(F(x))=r(x). The one-point map is valid also when x=y, where
the conclusion is already reflexivity.

(C) [For every F, M(F) implies P(F)] iff E is the universal relation X times X.
Universal E trivially suffices. For necessity, fix arbitrary x,y in X and choose
a permutation sigma of the attained alphabet r(X) satisfying sigma(r(x))=r(y).
For each attained target symbol t choose a state q_t with r(q_t)=t, choosing
q_{r(y)}=y. Set F(u)=q_{sigma(r(u))}. Then rF=sigma r. The decoder sigma inverse
on r(X), extended arbitrarily to unattained symbols of M if needed, witnesses M;
and F(x)=y. Hence the assumed implication gives x E y for every ordered pair.
When r(x)=r(y), sigma can be the identity; the representative choice still gives
F(x)=y. Nonemptiness of X supplies an extension value if a total decoder on M is
required. The proof is valid even if M contains unused symbols.

Consequences:
1. P(F) and S(F) agree for every F iff E=ker(r).
2. P(F) and M(F) agree for every F iff E is universal AND r is constant. Necessity
   combines (A) and (C); sufficiency makes both predicates true for every F.
3. Thus decoder-based preservation has a real recoding distinction. On X={0,1},
   r(x)=x, E=equality, and F(x)=1-x, M is true with decoder d(x)=1-x, while S and P
   are false. Although E=ker(r), only S coincides with P, not M.

The unrestricted-map quantifier is decisive. If allowed replacements form only
a semigroup or a declared implementation family, the representative collapses,
one-point substitutions, and alphabet-permutation realizations may be absent.
No reverse implication can then be imported from these unrestricted results.
The next research question should characterize these coupling implications for
a specified replacement family, keeping lineage as an independent audited datum.
These are elementary finite factorization results with complete proofs; this
review makes no publication-priority claim.
