audit docs: bring all four to 2026-05-04 post-CLM-prep state

Update VERIFICATION_STATUS, AXIOM_AUDIT, PARITY_REPORT, and
RESEARCH_ROADMAP to reflect the five-commit CLM-packaging-prep chain
(2026-05-04, commits `0e87907` … `0e5e4b9`).

Header dates → 2026-05-04; master ref → `0e5e4b9`.

New section in each doc enumerating the chain content:
  - 0e87907: eLpNorm → real-Lp.norm contractivity bridge
  - 49ff3ba: pointwise additivity + homogeneity (T_b f+g, T_b c•f)
  - aef881c: Lp-lifted linearity via MemLp.toLp_congr
  - 712ee4e: input-Lp-norm contractivity (LinearMap.mkContinuous form)
  - 0e5e4b9: direct Lp → Lp form + contractivity bound

What's-remaining narrowed and rephrased: the analytic content of
T_b : Lp → Lp with operator norm ≤ 1 is now COMPLETE in source. The
only outstanding piece for `LinearMap.mkContinuous` packaging is the
ae-equality propagation lemma — proving T_b respects ae-equality of
input under μ_log↾(0,1), which reduces to y_k preserving μ_log-null
sets. This follows from `inverseBranch_measurePreserving`
(volume-level, already in source) plus absolute continuity of μ_log
wrt volume on (0,1). Effort estimate: ~1-3 days.

No code change. Audit-only.

8 axioms (canonical PF/, unchanged), 0 sorries, 5488 jobs clean.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: your-name123

AXIOM_AUDIT.md

@@ -1,6 +1,18 @@
 # Lean 4 Axiom Audit — PF_Lean4_Code/PF/
 
-*As of 2026-05-03, post-rev-3 follow-on chain extended through Mayer 1991 contractivity in `eLpNorm` form + MemLp preservation (commits through `2e026aa`). **8 axioms** remain (canonical PF/), 0 sorries, 5488 jobs clean.*
+*As of 2026-05-04, post-rev-3 follow-on chain extended through CLM-packaging analytic prerequisites (commits through `0e5e4b9`). **8 axioms** remain (canonical PF/), 0 sorries, 5488 jobs clean.*
+
+## CLM-packaging analytic prerequisites (2026-05-04)
+
+A five-commit extension (`0e87907` through `0e5e4b9`) brings the transfer operator T_b's analytic content into the form mathlib's `LinearMap.mkContinuous` and `ContinuousLinearMap` API expect. Headline numbers unchanged; the formalization now exposes T_b at the `Lp → Lp` level with its operator-norm bound stated in real-valued `Lp.norm`.
+
+- `transferOperatorAction_fn_toLp_norm_le` — eLpNorm bound bridged to real-valued `Lp.norm` form via `Lp.norm_def` + `ENNReal.toReal_mono` (commit `0e87907`).
+- `transferOperatorAction_fn_add` + `transferOperatorAction_fn_smul` — pointwise additivity / homogeneity of $T_b^{fn}$ at the function level: $T_b(f+g) = T_b f + T_b g$, $T_b(c \cdot f) = c \cdot T_b f$ (commit `49ff3ba`).
+- `transferOperatorAction_fn_toLp_add` + `transferOperatorAction_fn_toLp_smul` — Lp-lifted linearity via `MemLp.toLp_congr` chain (mathlib `LpSpace/Basic.lean:109`) bridging to `MemLp.toLp_add` / `_const_smul` (each `rfl`) (commit `aef881c`).
+- `transferOperatorAction_fn_toLp_norm_le_input_toLp` — contractivity stated entirely in `Lp.norm`: $\|T_b^{fn,Lp}\, f\| \le \|\mathrm{MemLp.toLp}\, f\, h\|$, the form `LinearMap.mkContinuous` consumes as the operator-norm bound with $M = 1$ (commit `712ee4e`).
+- `transferOperator_lp` + `transferOperator_lp_norm_le` — direct `Lp → Lp` form via `(Lp.aestronglyMeasurable g).mk g` (canonical strongly-measurable representative), plus operator-norm bound $\|\mathrm{transferOperator}_{lp}\, g\| \le \|g\|$ (commit `0e5e4b9`).
+
+**What remains for $\|T_b\| \le 1$ as a `ContinuousLinearMap`**: lift the linearity (`_add`, `_smul` from `aef881c`) to `transferOperator_lp`. This requires showing $T_b$ respects ae-equality of input under $\mu_{\log}\!\restriction(0,1)$, which reduces to: $y_k$ preserves $\mu_{\log}$-null sets. The latter follows from `inverseBranch_measurePreserving` (volume level) plus absolute continuity of $\mu_{\log}$ wrt volume on $(0,1)$. Effort: ~1-3 days for the ae-equality propagation lemma, then `LinearMap.mkContinuous` is a one-shot.
 
 ## Phase A integration ladder + Mayer 1991 capstone + L² structural-swap analytic prerequisites (2026-05-01 → 2026-05-03)
 

PARITY_REPORT.md

@@ -1,6 +1,21 @@
 # Lean 4 ↔ Coq Axiom Parity Report
 
-*Last updated: 2026-05-03, post-rev-3 follow-on chain extended through Mayer 1991 contractivity in `eLpNorm` form + MemLp preservation (commits through `2e026aa`)*
+*Last updated: 2026-05-04, post-rev-3 follow-on chain extended through CLM-packaging analytic prerequisites (commits through `0e5e4b9`)*
+
+## CLM-packaging analytic prerequisites (2026-05-04)
+
+A five-commit extension (`0e87907` through `0e5e4b9`) brings $T_b$ to the `Lp → Lp` level with operator-norm bound stated in real-valued `Lp.norm`. Headline numbers unchanged on the Lean side; Coq side untouched.
+
+- **Lean 4 canonical**: 8 axioms (unchanged), **5488 jobs clean**, 0 sorries.
+- **Real-Lp.norm bridge of contractivity** (commit `0e87907`): `transferOperatorAction_fn_toLp_norm_le` — the eLpNorm bound (commit `de54564`) lifted via `Lp.norm_def` + `ENNReal.toReal_mono`.
+- **Pointwise linearity at the function level** (commit `49ff3ba`): `transferOperatorAction_fn_add` and `_smul` — $T_b(f+g) = T_b f + T_b g$, $T_b(c \cdot f) = c \cdot T_b f$ pointwise. No measurability hypothesis.
+- **Lp-lifted linearity** (commit `aef881c`): `transferOperatorAction_fn_toLp_add` and `_smul` — `Eq.trans` chain via `MemLp.toLp_congr` (mathlib `LpSpace/Basic.lean:109`) bridging to `MemLp.toLp_add` / `MemLp.toLp_const_smul` (each `rfl` in mathlib).
+- **Input-Lp.norm form of contractivity** (commit `712ee4e`): `transferOperatorAction_fn_toLp_norm_le_input_toLp` — $\|T_b^{fn,Lp}\, f\| \le \|\mathrm{MemLp.toLp}\, f\, h\|$. The form `LinearMap.mkContinuous` consumes as op-norm bound with $M = 1$.
+- **Direct `Lp → Lp` form** (commit `0e5e4b9`): `transferOperator_lp` (extracts canonical strongly-measurable representative via `(Lp.aestronglyMeasurable g).mk g`) + `transferOperator_lp_norm_le` ($\|\mathrm{transferOperator}_{lp}\, g\| \le \|g\|$). $T_b$ is now `Lp → Lp` with op norm $\le 1$.
+
+**Coq parity**: unchanged. The Coq formalization has its own independent axiomatization (253 axioms, separate scope from the canonical Lean's 8) and is not touched by this CLM-packaging work.
+
+**Effort to complete CLM packaging on the Lean side**: ~1-3 days remaining — lift `aef881c`'s linearity to `transferOperator_lp`, which requires showing $T_b$ respects ae-equality of input under $\mu_{\log}\!\restriction(0,1)$ (reduces to $y_k$ preserving $\mu_{\log}$-null sets, which follows from `inverseBranch_measurePreserving` + absolute continuity of $\mu_{\log}$ wrt volume on $(0,1)$). After that, `LinearMap.mkContinuous` is a one-shot.
 
 ## Phase A integration ladder + Mayer 1991 capstone + L² structural-swap analytic prerequisites (2026-05-01 → 2026-05-03)
 

RESEARCH_ROADMAP.md

@@ -86,8 +86,18 @@ The 8 axioms listed in `AXIOM_AUDIT.md` are the genuine mathematical boundary of
     * `enorm_rpow_two_eq_ofReal_norm_sq` — pointwise bridge `‖x‖ₑ^(2:ℝ) = ENNReal.ofReal(‖x‖^2)` (commit `63daa64`).
     * `transferOperatorAction_fn_eLpNorm_le_logWeightedMeasure` — **Mayer 1991 contractivity in `eLpNorm` form**: $\|T_b f\|_{L^2(\mu_{\log}\!\restriction(0,1))} \le \|f\|_{L^2(\mu_{\log}\!\restriction(0,1))}$ (commit `de54564`).
     * `transferOperatorAction_fn_memLp` — **MemLp preservation** corollary: the transfer operator preserves $L^2$ membership (commit `2e026aa`).
-
-**What remains for $\|T_b\| \le 1$ as a `ContinuousLinearMap` on `Lp ℂ 2`:** the structural rename / cascade — replacing the placeholder `structure LogWeightedL2` with `LogWeightedL2_concrete := MeasureTheory.Lp ℂ 2 logWeightedMeasure`, and updating `transferOperatorAction`'s `f.toFun` callsites to use the function-level `transferOperatorAction_fn` lifted via `MemLp.toLp`. The `MemLp` corollary (commit `2e026aa`) makes this lift mechanical.
+  - **CLM-packaging analytic prerequisites (commits `0e87907` … `0e5e4b9`, five commits 2026-05-04)**: brings $T_b$ to the `Lp → Lp` level with operator-norm bound stated in real-valued `Lp.norm` — the form mathlib's `LinearMap.mkContinuous` and `ContinuousLinearMap` API consume.
+    * `transferOperatorAction_fn_toLp_norm_le` — eLpNorm bound bridged to real-valued `Lp.norm` form via `Lp.norm_def` + `ENNReal.toReal_mono` (commit `0e87907`).
+    * `transferOperatorAction_fn_add` + `transferOperatorAction_fn_smul` — pointwise additivity / homogeneity of $T_b^{fn}$ at the function level: $T_b(f+g) = T_b f + T_b g$, $T_b(c \cdot f) = c \cdot T_b f$ (commit `49ff3ba`).
+    * `transferOperatorAction_fn_toLp_add` + `transferOperatorAction_fn_toLp_smul` — Lp-lifted linearity via `MemLp.toLp_congr` chain (mathlib `LpSpace/Basic.lean:109`) bridging to `MemLp.toLp_add` / `_const_smul` (each `rfl`) (commit `aef881c`).
+    * `transferOperatorAction_fn_toLp_norm_le_input_toLp` — contractivity stated entirely in `Lp.norm`: $\|T_b^{fn,Lp}\, f\| \le \|\mathrm{MemLp.toLp}\, f\, h\|$, the form `LinearMap.mkContinuous` consumes (commit `712ee4e`).
+    * `transferOperator_lp` + `transferOperator_lp_norm_le` — direct `Lp → Lp` form via `(Lp.aestronglyMeasurable g).mk g` (canonical strongly-measurable representative), plus operator-norm bound `‖transferOperator_lp g‖ ≤ ‖g‖` (commit `0e5e4b9`).
+
+**What remains for $\|T_b\| \le 1$ as a `ContinuousLinearMap` on `Lp ℂ 2`** (revised 2026-05-04, post `0e5e4b9`):
+- The function `transferOperator_lp : Lp → Lp` is in source with operator-norm bound `≤ 1` (commit `0e5e4b9`); both ingredients `LinearMap.mkContinuous` consumes are present at the right type level.
+- The remaining piece is **lifting linearity** (`_add`, `_smul` from commit `aef881c`) **to `transferOperator_lp`**. The challenge: `transferOperator_lp` uses the canonical `(Lp.aestronglyMeasurable g).mk g` representative, which differs (pointwise but not ae) between `g+h` and the sum of representatives of `g`, `h` separately. To prove `transferOperator_lp (g + h) = transferOperator_lp g + transferOperator_lp h`, one must show $T_b$ respects ae-equality of input under $\mu_{\log}\!\restriction(0,1)$ — equivalently, that $y_k$ preserves $\mu_{\log}$-null sets. This follows from `inverseBranch_measurePreserving` (volume level, already in source) plus absolute continuity of $\mu_{\log}$ wrt volume on $(0,1)$.
+- After the ae-equality propagation lemma, `LinearMap.mkContinuous` is a one-shot.
+- Once the CLM lands, `LogWeightedL2.inner` becomes mathlib's `@inner ℂ _ _` instance via the structural rename to `LogWeightedL2_concrete` (commit `88d5f37` already infrastructure-prepared).
 
 **Attack in Lean 4 (revised 2026-05-03 with eLpNorm contractivity in source):**
 - The analytic content is **complete**: function-level operator, measurability, eLpNorm contractivity, MemLp preservation are all in source.

VERIFICATION_STATUS.md

@@ -1,7 +1,7 @@
 # Principia Fractalis: Formal Verification Status
 
-**Last Updated:** 2026-05-03 (post-rev-3 follow-on chain extended through Mayer 1991 contractivity in eLpNorm form + MemLp preservation; master at `2e026aa`)
-**Status:** ✅ Rev-3 cycle complete + 58-commit follow-on chain extending the framework with conditional RH theorem, Millennium capstone, complete Phase A analytic foundations, the Mayer 1991 operator-norm bound in lintegral form, the function-level transfer operator with measurability, Mayer 1991 contractivity in mathlib's `eLpNorm` form ($\|T_b\| \le 1$ on $L^2(\mu_{\log}\!\restriction(0,1))$), and the `MemLp` preservation corollary
+**Last Updated:** 2026-05-04 (post-rev-3 follow-on chain extended through CLM-packaging analytic prerequisites: pointwise + Lp-lifted linearity, real-`Lp.norm` contractivity, direct `Lp → Lp` form; master at `0e5e4b9`)
+**Status:** ✅ Rev-3 cycle complete + 63-commit follow-on chain extending the framework with conditional RH theorem, Millennium capstone, complete Phase A analytic foundations, the Mayer 1991 operator-norm bound in lintegral form, the function-level transfer operator with measurability, Mayer 1991 contractivity in mathlib's `eLpNorm` form ($\|T_b\| \le 1$ on $L^2(\mu_{\log}\!\restriction(0,1))$), the `MemLp` preservation corollary, pointwise + Lp-lifted linearity of $T_b^{fn}$ ($T_b(f+g) = T_b f + T_b g$, $T_b(c\cdot f) = c\cdot T_b f$), and the direct `Lp → Lp` operator `transferOperator_lp` with `Lp.norm`-form contractivity bound
 **Audited By:** Pablo Cohen
 
 ---
@@ -27,6 +27,12 @@ The post-rev-3 follow-on chain (2026-04-29 → 2026-05-03, 49 commits) extended
     * `enorm_rpow_two_eq_ofReal_norm_sq` — pointwise bridge `‖x‖ₑ^(2:ℝ) = ENNReal.ofReal(‖x‖^2)` (commit `63daa64`).
     * `transferOperatorAction_fn_eLpNorm_le_logWeightedMeasure` — **Mayer 1991 contractivity in eLpNorm form** $\|T_b\| \le 1$ on $L^2(\mu_{\log}\!\restriction(0,1))$ (commit `de54564`).
     * `transferOperatorAction_fn_memLp` — **MemLp preservation corollary** (commit `2e026aa`).
+  - **CLM-packaging analytic prerequisites (commits `0e87907` … `0e5e4b9`, five commits 2026-05-04)**:
+    * `transferOperatorAction_fn_toLp_norm_le` — eLpNorm bound bridged to real-valued `Lp.norm` form via `Lp.norm_def` + `ENNReal.toReal_mono` (commit `0e87907`).
+    * `transferOperatorAction_fn_add` + `transferOperatorAction_fn_smul` — pointwise additivity / homogeneity of $T_b^{fn}$ at the function level: $T_b(f+g) = T_b f + T_b g$, $T_b(c \cdot f) = c \cdot T_b f$ (commit `49ff3ba`).
+    * `transferOperatorAction_fn_toLp_add` + `transferOperatorAction_fn_toLp_smul` — Lp-lifted linearity via `MemLp.toLp_congr` chain (mathlib `LpSpace/Basic.lean:109`) bridging to `MemLp.toLp_add` / `_const_smul` (each `rfl`) (commit `aef881c`).
+    * `transferOperatorAction_fn_toLp_norm_le_input_toLp` — contractivity stated entirely in `Lp.norm`: $\|T_b^{fn,Lp} f\| \le \|\mathrm{MemLp.toLp}\,f\,h\|$, the form `LinearMap.mkContinuous` consumes (commit `712ee4e`).
+    * `transferOperator_lp` + `transferOperator_lp_norm_le` — direct `Lp → Lp` form of the transfer operator via `(Lp.aestronglyMeasurable g).mk g` (extracts the canonical strongly-measurable representative), plus its operator-norm bound `‖transferOperator_lp g‖ ≤ ‖g‖` (commit `0e5e4b9`).
 
 **Current state: 8 axioms (canonical Lean 4 PF/), 0 sorries, `lake build` clean (5488 jobs; +2 over rev-3 for the `PF.Millennium` capstone module).**