def
definition
L3_scope
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Papers.ClaimBoundaries on GitHub at line 163.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
all -
all -
of -
independent -
Window -
all -
coupling_conserves_total -
love_changes_individual_sigma -
love_equilibrates -
composed_virtues_preserve_sigma -
virtue_composition_associative -
each_virtue_distinct_signature -
love -
love_has_unique_sigma_effect -
of -
one -
identity -
is -
of -
one -
independent -
as -
is -
E -
of -
for -
is -
LedgerTransition -
of -
is -
feasible -
Window -
all -
total -
that -
total -
one -
one -
identity
formal source
160- Photon-meaning bridge
161- Language emergence
162-/
163def L3_scope : String := "LNAL 5-op Semantic Core"
164
165/-! ## E-3: DREAM Virtues as Ethical Generators
166
167### Theorems (cite freely)
168- `Virtues.Generators.virtue_completeness` — direction-level: normalFormFromDirection
169 recovers ξ on Finset.range 32 for any feasible direction
170- `Virtues.Generators.virtue_minimality` — unique (α,β) solving φ-locked 2×2 system per pair
171- `Virtues.Generators.transform_preserves_admissibility` — micro-move preserves global admissibility
172- `Virtues.Generators.foldMoves_preserves_admissibility` — fold of moves preserves admissibility
173- `VirtueComposition.composed_virtues_preserve_sigma` — σ-preservation closed under composition
174- `VirtueComposition.virtue_composition_associative` — composition is associative
175- `LoveUniquenessDerivation.love_changes_individual_sigma` — love changes individual σ when agents differ
176- `LoveUniquenessDerivation.love_equilibrates` — love contracts σ-difference by (1-α)
177- `LoveUniquenessDerivation.coupling_conserves_total` — cross-lattice coupling conserves total σ
178- `VirtueSignatures.love_has_unique_sigma_effect` — love is the only virtue with nonzero σ-effect
179- `VirtueSignatures.each_virtue_distinct_signature` — all 14 signatures are distinct
180
181### Exact scope of proved completeness
182- Domain: `Consent.FeasibleDirection` (bond-space tangents), NOT arbitrary `LedgerTransition`
183- Window: `Finset.range 32` (32-bond scope)
184- Normal form: Justice + Forgiveness pair recovery per pair scope (other primitives zero in nfd)
185- This is NOT "14 independent basis vectors in tangent space"
186
187### Hypotheses (must state falsifier)
188- `H_DreamTheoremCompleteness` (in DREAMTheorem.lean): the 14 virtues generate ALL σ-preserving
189 ledger transitions. FALSIFIER: find one that cannot be decomposed.
190 STATUS: EMPIRICAL_HYPO — the theorem in that file is trivially the hypothesis restated.
191
192### Known limitations (must acknowledge)
193- `canonicalWisdomVirtue` is identity (needs external WiseChoice context)