diff --git a/docs/pbs/pull-requests/PR-13.1-flow-body-analyzer-context-and-entrypoint-foundation.md b/docs/pbs/pull-requests/PR-13.1-flow-body-analyzer-context-and-entrypoint-foundation.md
new file mode 100644
index 00000000..cddab51c
--- /dev/null
+++ b/docs/pbs/pull-requests/PR-13.1-flow-body-analyzer-context-and-entrypoint-foundation.md
@@ -0,0 +1,67 @@
+# PR-13.1 - Flow Body Analyzer Context and Entrypoint Foundation
+
+## Briefing
+
+`PbsFlowBodyAnalyzer` concentra montagem de contexto, iteracao de callables e delegacao recursiva de block/statement analysis em uma unica classe.
+
+Esta PR introduz a base estrutural para decomposicao sem alterar funcionalidade: contexto compartilhado, encapsulamento dos argumentos recorrentes e uma fachada mais clara para a classe.
+
+## Motivation
+
+### Dor atual que esta PR resolve
+
+1. A classe repassa muitos parametros repetidos entre `validate`, `validateCallableBody`, `analyzeBlock` e `analyzeStatement`.
+2. Extracoes futuras ficam arriscadas sem um contexto comum explicito.
+3. A fundacao estrutural reduz risco antes de mover regras de completion, statements e assignment resolution.
+
+## Target
+
+Estabelecer uma base segura para o refactor:
+
+1. contexto compartilhado de body analysis,
+2. encapsulamento de `returnType`, `resultErrorName`, `receiverType`, `model` e `diagnostics`,
+3. fachada pequena para `validate(...)`.
+
+## Dependencies
+
+Nenhuma.
+
+## Scope
+
+1. Introduzir um contexto/request object para analise de corpo.
+2. Reorganizar `validate` e `validateCallableBody` sem mover ainda regras complexas.
+3. Preservar a relacao atual com `PbsFlowExpressionAnalyzer`.
+
+## Non-Goals
+
+1. Nao alterar inferencia de tipos ou diagnosticos.
+2. Nao alterar `Model.from(...)`.
+3. Nao mover ainda completion analysis ou assignment target resolution para classes separadas.
+
+## Method
+
+### O que deve ser feito explicitamente
+
+1. Criar um contexto pequeno e explicito para analise recursiva de blocos/callables.
+2. Manter `PbsFlowBodyAnalyzer` como entrypoint package-private.
+3. Preservar a ordem atual de validacao e emissao de erros.
+
+## Acceptance Criteria
+
+1. `PbsFlowBodyAnalyzer` continua com o mesmo contrato observavel.
+2. A quantidade de parametros repetidos nas chamadas internas e reduzida.
+3. Nao ha mudanca funcional em flow analysis, completion ou diagnosticos.
+
+## Tests
+
+1. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsControlFlowTest*`
+2. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsDeclarationsTest*`
+3. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test`
+
+## Affected Documents
+
+1. Nenhum documento normativo.
+
+## Open Questions
+
+1. O contexto deve ser derivado imutavelmente por bloco ou mutado localmente. A recomendacao e derivacao leve para reduzir risco de vazamento entre branches.
diff --git a/docs/pbs/pull-requests/PR-13.2-flow-body-analyzer-callable-body-and-completion-decomposition.md b/docs/pbs/pull-requests/PR-13.2-flow-body-analyzer-callable-body-and-completion-decomposition.md
new file mode 100644
index 00000000..3ea4d1a1
--- /dev/null
+++ b/docs/pbs/pull-requests/PR-13.2-flow-body-analyzer-callable-body-and-completion-decomposition.md
@@ -0,0 +1,71 @@
+# PR-13.2 - Flow Body Analyzer Callable Body and Completion Decomposition
+
+## Briefing
+
+As regras de entrada de callable e de completion/fallthrough em `PbsFlowBodyAnalyzer` formam um cluster coeso, mas hoje ficam misturadas com statement analysis e assignment resolution.
+
+Esta PR extrai essa superficie para colaboradores dedicados, sem alterar funcionalidade.
+
+## Motivation
+
+### Dor atual que esta PR resolve
+
+1. `validateCallableBody`, `validateCallableCompletion`, `blockAlwaysReturns`, `statementAlwaysReturns`, `expressionAlwaysReturns`, `switchAlwaysReturns` e `handleAlwaysReturns` concentram regras de completion com alto branching.
+2. Completion analysis e statement analysis sao preocupacoes diferentes e hoje dividem a mesma classe.
+3. Essa parte e muito sensivel e merece uma fronteira estrutural propria.
+
+## Target
+
+Separar a camada de body entry/completion:
+
+1. bootstrap de callable body,
+2. validacao de fallthrough/completion,
+3. regras de `always returns`,
+4. exaustividade relevante para completion.
+
+## Dependencies
+
+Prerequisito direto:
+
+1. `PR-13.1`
+
+## Scope
+
+1. Extrair `validateCallableBody`.
+2. Extrair `validateCallableCompletion`, `blockAlwaysReturns`, `statementAlwaysReturns`, `expressionAlwaysReturns`.
+3. Extrair `switchAlwaysReturns`, `switchIsExhaustive`, `handleAlwaysReturns`, `handleArmAlwaysReturns`, `isKnownErrorPath`.
+
+## Non-Goals
+
+1. Nao alterar as regras atuais de fallthrough para result/plain non-unit.
+2. Nao alterar a semantica de exaustividade usada apenas para completion.
+3. Nao alterar statement analysis ou assignment checks.
+
+## Method
+
+### O que deve ser feito explicitamente
+
+1. Introduzir um analisador de completion ou divisao equivalente.
+2. Manter `PbsFlowBodyAnalyzer` como orquestrador do processo.
+3. Preservar rigorosamente a ordem atual de checks e codigos de diagnostico.
+
+## Acceptance Criteria
+
+1. A logica de completion/fallthrough deixa de ficar centralizada em `PbsFlowBodyAnalyzer`.
+2. As regras de `always returns` permanecem equivalentes.
+3. Nenhum teste de fallthrough, control flow ou result flow muda comportamento esperado.
+
+## Tests
+
+1. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsFallthroughTest*`
+2. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsControlFlowTest*`
+3. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsResultFlowRulesTest*`
+4. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test`
+
+## Affected Documents
+
+1. Nenhum documento normativo.
+
+## Open Questions
+
+1. `switch`/`handle` completion deve ficar junto do completion analyzer ou reaproveitar colaboradores do expression analyzer. A recomendacao e manter local ao completion analyzer para evitar acoplamento indevido entre analise de tipo e analise de terminacao.
diff --git a/docs/pbs/pull-requests/PR-13.3-flow-body-analyzer-statement-analysis-splitting.md b/docs/pbs/pull-requests/PR-13.3-flow-body-analyzer-statement-analysis-splitting.md
new file mode 100644
index 00000000..f217bf03
--- /dev/null
+++ b/docs/pbs/pull-requests/PR-13.3-flow-body-analyzer-statement-analysis-splitting.md
@@ -0,0 +1,72 @@
+# PR-13.3 - Flow Body Analyzer Statement Analysis Splitting
+
+## Briefing
+
+Depois de separar entry/completion, o maior hotspot restante em `PbsFlowBodyAnalyzer` passa a ser `analyzeBlock` e `analyzeStatement`, com tratamento de `let`, `return`, `if`, `for`, `while`, expression statement e delegacao para `PbsFlowExpressionAnalyzer`.
+
+Esta PR extrai essa superficie para colaboradores menores, sem alterar funcionalidade.
+
+## Motivation
+
+### Dor atual que esta PR resolve
+
+1. `analyzeStatement` concentra varias formas de statement com regras semanticas distintas.
+2. Loops, `if` e `return` usam os mesmos parametros e diagnosticos, mas pertencem a clusters semanticos diferentes.
+3. A manutencao dessa logica em um unico metodo torna a classe dificil de evoluir.
+
+## Target
+
+Separar a analise de statements:
+
+1. blocos e escopos,
+2. `let` e expression statements,
+3. `return` flow,
+4. `if/for/while`.
+
+## Dependencies
+
+Prerequisitos diretos:
+
+1. `PR-13.1`
+2. `PR-13.2`
+
+## Scope
+
+1. Extrair `analyzeBlock` e o dispatch de `analyzeStatement`.
+2. Extrair regras de `let`, `if`, `for`, `while` e expression statement para helpers/colaboradores dedicados.
+3. Deixar `return` bootstrap pronto para corte proprio, sem ainda mexer em assignment target resolution.
+
+## Non-Goals
+
+1. Nao alterar mutabilidade de escopo local.
+2. Nao alterar validacao de tipos de condicao ou bounds de loop.
+3. Nao alterar assignment resolution.
+
+## Method
+
+### O que deve ser feito explicitamente
+
+1. Introduzir um statement analyzer ou divisao equivalente por familias.
+2. Reusar o contexto compartilhado da `PR-13.1`.
+3. Preservar a ordem atual de chamadas ao `expressionAnalyzer`.
+
+## Acceptance Criteria
+
+1. `analyzeStatement` deixa de concentrar todas as formas de statement.
+2. Scoping, condition checks e loop bound checks permanecem equivalentes.
+3. Suite semantica continua verde sem mudanca funcional.
+
+## Tests
+
+1. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsControlFlowTest*`
+2. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsAssignmentTest*`
+3. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsDeclarationsTest*`
+4. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test`
+
+## Affected Documents
+
+1. Nenhum documento normativo.
+
+## Open Questions
+
+1. `return` deve ficar no statement analyzer ou em um colaborador proprio de result flow. A recomendacao e deixar o corte final para a PR seguinte se isso simplificar mais a classe.
diff --git a/docs/pbs/pull-requests/PR-13.4-flow-body-analyzer-assignment-target-resolution-decomposition.md b/docs/pbs/pull-requests/PR-13.4-flow-body-analyzer-assignment-target-resolution-decomposition.md
new file mode 100644
index 00000000..672ba64c
--- /dev/null
+++ b/docs/pbs/pull-requests/PR-13.4-flow-body-analyzer-assignment-target-resolution-decomposition.md
@@ -0,0 +1,72 @@
+# PR-13.4 - Flow Body Analyzer Assignment Target Resolution Decomposition
+
+## Briefing
+
+`resolveAssignmentTarget` e a logica correlata de assignment compatibility concentram um dos trechos mais densos e sensiveis de `PbsFlowBodyAnalyzer`.
+
+Esta PR extrai a resolucao de assignment target e as regras de acesso/leitura/escrita de campo para colaboradores dedicados, sem alterar funcionalidade.
+
+## Motivation
+
+### Dor atual que esta PR resolve
+
+1. Assignment resolution mistura lookup de locals, `this`, singleton services, consts e navegação em campos de struct.
+2. Regras de leitura e escrita de campo estao acopladas ao fluxo do statement analyzer.
+3. A superficie e densa e merece um resolver proprio com foco em diagnósticos de assignability.
+
+## Target
+
+Separar a camada de assignment semantics:
+
+1. resolucao de assignment target,
+2. assignability de roots conhecidos,
+3. leitura/escrita de campos,
+4. type compatibility por operador de atribuicao.
+
+## Dependencies
+
+Prerequisitos diretos:
+
+1. `PR-13.1`
+2. `PR-13.2`
+3. `PR-13.3`
+
+## Scope
+
+1. Extrair `analyzeAssignmentStatement`.
+2. Extrair `resolveAssignmentTarget`, `assignmentCompatible`, `canReadStructField`, `canWriteStructField`, `isKnownNonAssignableRoot`.
+3. Manter `AssignmentTargetResolution` ou mover para um modelo focado de assignment.
+
+## Non-Goals
+
+1. Nao alterar regras de mutabilidade/local const.
+2. Nao alterar regras de acesso a campos privados/publicos.
+3. Nao alterar o mapeamento de operadores compostos para inferencia binaria.
+
+## Method
+
+### O que deve ser feito explicitamente
+
+1. Criar um resolver dedicado para assignment targets.
+2. Preservar exatamente os mesmos erros emitidos para target nao resolvido, nao assignable ou field access denied.
+3. Reusar `PbsFlowTypeOps` sem alterar sua logica.
+
+## Acceptance Criteria
+
+1. Assignment target resolution deixa de ficar centralizada em `PbsFlowBodyAnalyzer`.
+2. Regras de assignability e field access permanecem equivalentes.
+3. Nenhum teste de assignment ou control flow muda comportamento esperado.
+
+## Tests
+
+1. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsAssignmentTest*`
+2. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsDeclarationsTest*`
+3. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test`
+
+## Affected Documents
+
+1. Nenhum documento normativo.
+
+## Open Questions
+
+1. `AssignmentTargetResolution` deve permanecer como record local ou migrar para um modelo package-private dedicado. A recomendacao e mover para o resolver de assignment para reduzir acoplamento.
diff --git a/docs/pbs/pull-requests/PR-13.5-flow-body-analyzer-regression-hardening-and-final-cleanup.md b/docs/pbs/pull-requests/PR-13.5-flow-body-analyzer-regression-hardening-and-final-cleanup.md
new file mode 100644
index 00000000..d39656f5
--- /dev/null
+++ b/docs/pbs/pull-requests/PR-13.5-flow-body-analyzer-regression-hardening-and-final-cleanup.md
@@ -0,0 +1,77 @@
+# PR-13.5 - Flow Body Analyzer Regression Hardening and Final Cleanup
+
+## Briefing
+
+As PRs anteriores reduzem a complexidade estrutural de `PbsFlowBodyAnalyzer`. Esta PR fecha a trilha com consolidacao final, limpeza de duplicacao residual e endurecimento de regressao, sem alterar funcionalidade.
+
+## Motivation
+
+### Dor atual que esta PR resolve
+
+1. Refactors estruturais em flow/body analysis podem preservar casos principais e ainda mudar detalhes finos de diagnostico ou scoping.
+2. Ao final da decomposicao, tendem a restar helpers redundantes ou caminhos duplicados.
+3. O fechamento da trilha precisa garantir equivalencia observavel e uma fachada final pequena.
+
+## Target
+
+Concluir a trilha de refactor:
+
+1. limpeza estrutural final,
+2. consolidacao dos helpers remanescentes,
+3. cobertura de regressao para completion, statements e assignment semantics.
+
+## Dependencies
+
+Prerequisitos diretos:
+
+1. `PR-13.1`
+2. `PR-13.2`
+3. `PR-13.3`
+4. `PR-13.4`
+
+## Scope
+
+1. Remover duplicacao residual apos as extracoes.
+2. Garantir que `PbsFlowBodyAnalyzer` fique reduzido a composicao/orquestracao.
+3. Reforcar testes de regressao para fallthrough, return flow, loops e assignments.
+
+## Non-Goals
+
+1. Nao alterar taxonomia de `PbsSemanticsErrors`.
+2. Nao alterar `PbsFlowTypeOps` ou `PbsFlowExpressionAnalyzer`.
+3. Nao introduzir novas regras semanticas.
+
+## Method
+
+### O que deve ser feito explicitamente
+
+1. Fazer uma passada final de consolidacao.
+2. Verificar equivalencia com foco em:
+   - completion/fallthrough,
+   - scoping local,
+   - return result flow,
+   - assignment target resolution,
+   - field access diagnostics.
+3. Encerrar a trilha com uma fachada pequena e clara.
+
+## Acceptance Criteria
+
+1. `PbsFlowBodyAnalyzer` termina como orquestrador, nao como concentrador da logica completa.
+2. Nao ha mudanca funcional observavel em flow analysis ou diagnosticos.
+3. Suite do frontend PBS passa integralmente.
+
+## Tests
+
+1. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsFallthroughTest*`
+2. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsAssignmentTest*`
+3. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsControlFlowTest*`
+4. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test --tests *PbsSemanticsResultFlowRulesTest*`
+5. `:prometeu-compiler:frontends:prometeu-frontend-pbs:test`
+
+## Affected Documents
+
+1. Nenhum documento normativo.
+
+## Open Questions
+
+1. Nenhuma. A partir desta PR, qualquer mudanca adicional deve ser tratada como evolucao funcional separada.