LEAN MACRO KERNEL REPLAY RECEIPT
================================

The release theorem is:

  theorem exact_p4_two_cube_macro_patch_verified :
      p4TwoCubeMacroPatchCertificate.verify = true := by
    decide +kernel

A hostile auxiliary replay first used plain `decide`; that tactic did not reduce
the closed Array computation and the failed theorem was reported with `sorryAx`.
That failed auxiliary theorem is not a release theorem and its `sorryAx` was the
elaborator's placeholder after tactic failure.

Correct replay command (Lean 4.30.0):

  lake env lean /tmp/AuditKernelReplayFixed.lean

where the temporary theorem also uses `decide +kernel`.

Observed output:

  'macroKernelReplayFixed' depends on axioms: [propext]
  'Freudenthal.exact_p4_two_cube_macro_patch_verified' depends on axioms: [propext]

Exit status: 0
No `sorryAx`, `Lean.ofReduceBool`, or native-decision axiom appears.
