Derive actual FA initial operator moment

1 files changed, 33 insertions, 5 deletions

diff --git a/notes/28_contribution_status_proof_vs_fit.md b/notes/28_contribution_status_proof_vs_fit.md
index 40c1118..5507de7 100644
--- a/notes/28_contribution_status_proof_vs_fit.md
+++ b/notes/28_contribution_status_proof_vs_fit.md
@@ -17,7 +17,7 @@ Our current project should avoid calling every component a theorem.
 | contribution | current status | fitted? | safe main-paper phrasing |
 |---|---|---:|---|
 | 1. capacity formalization | definition + exact random-geometry theorem | no | exact under isotropic feedback assumptions |
-| 2. scaling and soft erosion | exact scaling + exact random-subspace null model; real FA extension not yet proved | no, but partly only a null model | capacity cost scales exactly; random-subspace erosion gives a baseline, while real FA needs `k_eff` |
+| 2. scaling and soft erosion | exact scaling + exact random-subspace null model + actual-FA initial moment theorem | no, but finite-time FA still needs dynamics | capacity cost scales exactly; actual FA has a no-fit `e_0` theorem, while `t>0` needs operator dynamics |
 | 3. prior-free minimax bound | exact theorem | no | minimax optimality for prior-free angular alignment |
 | 4. tangent-operator estimator | first-order tangent derivation + conditional predictor | no scalar fit, but uses early observed operators | estimator for finite-time gap, not architecture-only theorem |
 | 5. empirical distribution validation | experiment | no | validates which theoretical distributions and estimators match trajectories |
@@ -132,6 +132,31 @@ hard-k random-subspace formula exactly predicts real FA/BP gap
 
 This is false in our current experiments.
 
+We now have a stronger actual-FA initialization theorem:
+
+```text
+speed_BP = sum_l ||g_l^BP||^2
+speed_FA = sum_l <g_l^BP, g_l^FA>
+e_0 = 1 - speed_FA / speed_BP
+```
+
+For fixed forward weights and residuals, with independent zero-mean feedback:
+
+```text
+E_B[speed_FA | W,r] = ||g_output^BP||^2
+```
+
+Therefore:
+
+```text
+E_B[e_0 | W,r]
+  = 1 - ||g_output^BP||^2 / sum_l ||g_l^BP||^2
+```
+
+This is actual FA, not a random-subspace proxy. It says the initial effective
+burden is the hidden-layer BP speed share. It does not yet solve the full
+finite-time problem because training makes `W_t` depend on `B`.
+
 ## 3. Prior-Free Minimax Initialization Bound
 
 This is proof-level.
@@ -305,9 +330,12 @@ The paper can honestly claim:
 The current unresolved theoretical gap:
 
 ```text
-derive k_eff or e_t distribution for actual FA directly from architecture and
-feedback initialization, rather than measuring early tangent operators.
+derive the t>0 distribution of k_eff(t) or e_t for actual FA directly from
+architecture and feedback initialization, rather than measuring early tangent
+operators.
 ```
 
-Until that is solved, contribution 2 should not overpromise exact FA gap
-prediction, and contribution 4 should be the quantitative gap tool.
+The t=0 conditional mean is now solved by the actual-FA initial moment theorem.
+Until the t>0 dynamics are solved, contribution 2 should not overpromise exact
+finite-time FA gap prediction, and contribution 4 should remain the
+quantitative finite-time gap tool.