Foundation Operator Core Coupled Recognition Cores Local Weyl Family Card

The local Weyl family count

A recognition core, in Recognition Science, is a discrete record of events that a system keeps about its own inputs. When two such cores are coupled, the framework studies the local operations that can act on one core without touching the other. The declaration localWeylFamily_card establishes that the family of such local operations has exactly eight members.

This is a counting theorem, not a construction. It says the set of local Weyl monomials, the basic building blocks of these operations, contains precisely eight distinct elements. The result is proved in the framework's machine-checked library of formal theorems, meaning the count is not an empirical observation or a definitional choice but a derived fact.

In Recognition Science, the number eight is not incidental. A separate theorem in the framework's forcing chain derives 2^3, the cube of two, as the number of ticks in a recognition cycle. The local Weyl family count of eight is consistent with that derivation, though the declaration itself does not connect the two results.

The declaration does not claim that these eight operations are physically realized in any particular system. It does not claim that the local Weyl family is complete in any operational sense, nor that it generates all possible local transformations. It establishes only the cardinality of a specific algebraic family, nothing more.

abbrev localWeylFamily_card := IndisputableMonolith.Foundation.CoupledRecognitionCores.localWeylFamily_card

What this page does not claim

The declaration does not claim the eight operations are physically realized in any system. It does not claim the local Weyl family generates all possible local transformations. It does not claim a connection between this count and the eight-tick recognition cycle.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/OperatorCore/CoupledRecognitionCores.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: