Mathematical audit | Version 1.0 | 31 October 2026

This is an author-side logical audit, not an independent referee report.

1. Universal simulation
   Input: acceptable numbering, partial universal evaluator, total s-m-n map.
   Conclusion: equality of partial functions, including divergence.
   Excluded: equality of time, syntax, provenance; completed infinite towers.

2. Lambda presentation
   Input: fixed deterministic weak CBV and numeric encoding/observation protocol.
   Mutual adequacy is taken from cited established simulations.
   Conclusion: inverse maps on behavioral quotient sets.
   Excluded: literal code identity, beta convertibility, arbitrary contextual
   equivalence, a new compiled lambda implementation in this package.

3. Concrete higher model
   Construction: Fun(Fin^op, Spaces), constant program and natural objects.
   All trace relations are interpreted objectwise; graph equality is preserved.
   B includes general partial graphs; A is only the image of chosen codes.
   The ambient category has noncomputable morphisms. It is not misidentified
   with a higher realizability topos or with Hyland's effective topos.

4. Predicate descent
   Input: effective epi q, saturation on its full homotopy kernel pair.
   Construction: propositional truncation of the dependent sum of witnesses.
   The reverse implication eliminates truncation only into a proposition.
   Uniqueness uses local surjectivity, never a global section or choice.
   Statements are internal over generalized elements, not global points only.

5. Higher observations
   Path transport preserves a family only after a semantic path is supplied.
   Univalence does not prove arbitrary computable types equivalent.
   General family descent needs coherent Cech data. The C2-action example
   distinguishes identical underlying fibers with different descent data.

6. Counterexamples
   The provenance tag is total computable and independent of the behavioral
   quotient. Subobject equality is distinguished from bare type equivalence.
   A separate one-versus-two finite-fiber example refutes the latter reading.
   Exact transition cost is distinct from polynomial complexity overhead.

7. Rice
   Classical metatheorem on total computable Boolean classifiers over all codes.
   Uses nowhere-defined function, a witness of nontriviality, s-m-n, halting.
   Does not imply undefinability, triviality of Omega, or decidability of all
   subobjects. Assembly argument uses standard Boolean realizers and the full
   index set as the union of realizer sets.

8. Claim scope
   No theorem proves equivalence of arbitrary Real and Simulated predicates.
   Equality between two descended predicates requires equality on the quotient.
   No theorem asserts that all algorithms compute the same function.
   No physical interpretation or proof of metaphysical simulation is supplied.

9. Reproducibility
   Native and interpreter transitions are implemented separately.
   Terminating outputs and costs are checked against closed-form expectations.
   Fuel exhaustion is explicitly bounded evidence, not nontermination proof.
   No Lean, Coq/Rocq, Agda, or other kernel check of this manuscript was run.
