git:20260914.9a89592 to git:20261028.714cea2
20 added, 88 removed. Audit A to A.
- # fep_lean (docs/other archive entry)
-
- ## Overview
-
- **Status**: active documentation program (draft) | **Version**: 0.2 | **Last
- Updated**: 2026-09-04
-
- ## Purpose
-
- Document, for GNN-side readers and agents, the formal collaboration program
- with the sibling Lean 4 repository `fep_lean`: how generative models that
- have Lean expressions can be rendered and executed by the GNN pipeline, and
- how GNN's steps and methods are being formalized in Lean. This folder is the
- GNN-side mirror of the fep_lean design program at
- `../fep_lean/docs/design/gnn-bridge/` (cross-repo references are inline code
- paths, never markdown links).
-
- On the fep_lean side, W2 source custody and Q5–Q7 concrete artifact proofs
- have current schema-2 native receipts. H2.7 acceptance opens only read-only
- H3.G0 eligibility. Current evidence and exact boundaries live in
- `../fep_lean/specs/gnn-bridge-w2-source-custody/WAVE2-REPORT.md`.
- The mirrored bridge contract is version 0.6.
-
- ## Contents
-
- | File | Role |
- | --- | --- |
- | [README.md](README.md) | Reader-facing entry point and navigation |
- | [fep_lean.md](fep_lean.md) | Catalogue overview: formalized content, evidence planes, commands |
- | [fep_lean_gnn.md](fep_lean_gnn.md) | The collaboration program: pipeline integration and the Lean formalization program |
- | [bridge-contract.md](bridge-contract.md) | Mirror of the canonical cross-repo contract |
- | [SPEC.md](SPEC.md) | Scope specification |
-
- ## Quick navigation
-
- - [Main documentation](../../README.md)
- - [docs/other archive](../README.md) and its [AGENTS.md](../AGENTS.md)
- - [GNN syntax](../../gnn/gnn_syntax.md)
- - [Active Inference theory folder](../../active_inference/README.md)
-
- ## Key concepts
-
- - **Model-kind alignment.** GNN's discrete POMDP family (`A/B/C/D[/E]`, `F[1]`
- readout) corresponds to fep_lean's finite carrier family
- (`active_inference.lean` `GenerativeModel`, `FiniteLaw`/`FiniteKernel`,
- `FiniteHMM`); GNN's continuous linear-Gaussian family (`F/H/Q/R`) corresponds
- to fep_lean's Gaussian/OU semigroup family.
- - **Evidence planes stay distinct.** A pipeline run establishes that a
- document parses, renders, and executes; a Lean compilation establishes that
- a named body compiles. Neither substitutes for the other.
- - **Provenance rule.** Bridge-emitted documents carry source repo, commit
- digest, Lean definition, and generator identity in their provenance section.
- - **`unsupported` vs `failed`.** Continuous models on categorical-only render
- backends report `unsupported` (excluded from execution) — a distinct status
- from `failed`; see `src/gnn/README.md`.
-
- ## Integration with pipeline
-
- A fep_lean-emitted document flows through the standard pipeline: step 3
- (parse), step 5 (type check), step 10 (ontology validation against
- `src/gnn/ontology/act_inf_ontology_terms.json`), step 11 (render, nine targets),
- step 12 (execute, eight targets). Naming convention for emitted documents:
- `GNNSection` identifier prefixed `FepLean`, with the `continuous` keyword for
- the continuous family so kind detection stays mechanical. Details:
- [fep_lean_gnn.md](fep_lean_gnn.md).
+ # FEP_Formal collaboration documentation
- ## Editing rules
+ This folder retains its historical `fep_lean` path and linked filenames.
+ Current public imports use `fep_formal`, commands use `fep-formal`, and public
+ settings use `FEP_FORMAL_`. Legacy names are deprecated aliases through 2.x.
- - The bridge contract in this folder is a **mirror**. Edit the canonical copy
- first (`../fep_lean/docs/design/gnn-bridge/bridge-contract.md`), then update
- this mirror in the same working session, keeping the bodies identical.
- - Keep all links relative and verify targets exist; the repository-wide
- documentation audit (`uv run --extra dev python
- docs/development/docs_audit.py --strict --check-anchors --no-write`) checks
- them for every markdown file.
- - Follow [style_guide.md](../../style_guide.md): `uv run python` command
- spellings, H1 title, metadata block, honest claims without embedded
- ungenerated counts.
- - Do not add pipeline behavior claims for fep_lean integration that the
- pipeline does not yet have; this folder describes a scoped research
- program, and its phases are tracked in [fep_lean_gnn.md](fep_lean_gnn.md).
+ ## Ownership
- ## Related resources
+ The canonical bridge contract lives at
+ `../fep_formal/docs/design/gnn-bridge/bridge-contract.md`. Edit it there first,
+ then synchronize this folder's [mirror](bridge-contract.md) in the same session.
+ Normalized bodies must match; only the canonical/mirror location rows differ.
+ Keep cross-repository paths in code, and local documentation links relative.
- - [fep_lean.md](fep_lean.md) and [fep_lean_gnn.md](fep_lean_gnn.md)
- - [Expected free energy](../../active_inference/expected_free_energy.md) and
- [generative models](../../active_inference/generative_models.md)
- - [Framework integration guide](../../gnn/integration/framework_integration_guide.md)
- - [Development guide](../../development/README.md)
+ ## Evidence and maintenance
- ---
+ Historical Q5/Q6/Q7 receipts describe their original source pairs. Current
+ qualification needs an explicitly named pair and fresh artifact-specific source
+ and native checks. Syntax, numerical agreement, native proof and generated-runner
+ execution remain separate evidence planes. Do not promote old receipts.
- **Status**: active | **Maintenance**: update together with the canonical
- bridge program on the fep_lean side | **Last Updated**: 2026-09-04
+ The [reader entry](README.md), [overview](fep_lean.md), [program](fep_lean_gnn.md)
+ and [scope](SPEC.md) retain dated program history. The current integration
+ workflow is owned by the [paired-revision procedure](../../development/fep_lean_paired_revision.md).
+ After edits, run the strict documentation audit with anchors and no writes:
+ `uv run --frozen --no-sync python docs/development/docs_audit.py --strict --check-anchors --no-write`.