October 2026 main drop: mirror from GitHub

.gitattributes

@@ -33,3 +33,4 @@ saved_model/**/* filter=lfs diff=lfs merge=lfs -text
 *.zip filter=lfs diff=lfs merge=lfs -text
 *.zst filter=lfs diff=lfs merge=lfs -text
 *tfevents* filter=lfs diff=lfs merge=lfs -text
+docs/images/foundry-j-verify.png filter=lfs diff=lfs merge=lfs -text

LICENSE

@@ -0,0 +1,661 @@
+                    GNU AFFERO GENERAL PUBLIC LICENSE
+                       Version 3, 19 November 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The GNU Affero General Public License is a free, copyleft license for
+software and other kinds of works, specifically designed to ensure
+cooperation with the community in the case of network server software.
+
+  The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works.  By contrast,
+our General Public Licenses are intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+  Developers that use our General Public Licenses protect your rights
+with two steps: (1) assert copyright on the software, and (2) offer
+you this License which gives you legal permission to copy, distribute
+and/or modify the software.
+
+  A secondary benefit of defending all users' freedom is that
+improvements made in alternate versions of the program, if they
+receive widespread use, become available for other developers to
+incorporate.  Many developers of free software are heartened and
+encouraged by the resulting cooperation.  However, in the case of
+software used on network servers, this result may fail to come about.
+The GNU General Public License permits making a modified version and
+letting the public access it on a server without ever releasing its
+source code to the public.
+
+  The GNU Affero General Public License is designed specifically to
+ensure that, in such cases, the modified source code becomes available
+to the community.  It requires the operator of a network server to
+provide the source code of the modified version running there to the
+users of that server.  Therefore, public use of a modified version, on
+a publicly accessible server, gives the public access to the source
+code of the modified version.
+
+  An older license, called the Affero General Public License and
+published by Affero, was designed to accomplish similar goals.  This is
+a different license, not a version of the Affero GPL, but Affero has
+released a new version of the Affero GPL which permits relicensing under
+this license.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                       TERMS AND CONDITIONS
+
+  0. Definitions.
+
+  "This License" refers to version 3 of the GNU Affero General Public License.
+
+  "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+  "The Program" refers to any copyrightable work licensed under this
+License.  Each licensee is addressed as "you".  "Licensees" and
+"recipients" may be individuals or organizations.
+
+  To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy.  The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+  A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+  To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy.  Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+  To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies.  Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+  An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License.  If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+  1. Source Code.
+
+  The "source code" for a work means the preferred form of the work
+for making modifications to it.  "Object code" means any non-source
+form of a work.
+
+  A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+  The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form.  A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+  The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities.  However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work.  For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+  The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+  The Corresponding Source for a work in source code form is that
+same work.
+
+  2. Basic Permissions.
+
+  All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met.  This License explicitly affirms your unlimited
+permission to run the unmodified Program.  The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work.  This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+  You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force.  You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright.  Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+  Conveying under any other circumstances is permitted solely under
+the conditions stated below.  Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+  3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+  No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+  When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+  4. Conveying Verbatim Copies.
+
+  You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+  You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+  5. Conveying Modified Source Versions.
+
+  You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+    a) The work must carry prominent notices stating that you modified
+    it, and giving a relevant date.
+
+    b) The work must carry prominent notices stating that it is
+    released under this License and any conditions added under section
+    7.  This requirement modifies the requirement in section 4 to
+    "keep intact all notices".
+
+    c) You must license the entire work, as a whole, under this
+    License to anyone who comes into possession of a copy.  This
+    License will therefore apply, along with any applicable section 7
+    additional terms, to the whole of the work, and all its parts,
+    regardless of how they are packaged.  This License gives no
+    permission to license the work in any other way, but it does not
+    invalidate such permission if you have separately received it.
+
+    d) If the work has interactive user interfaces, each must display
+    Appropriate Legal Notices; however, if the Program has interactive
+    interfaces that do not display Appropriate Legal Notices, your
+    work need not make them do so.
+
+  A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit.  Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+  6. Conveying Non-Source Forms.
+
+  You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+    a) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by the
+    Corresponding Source fixed on a durable physical medium
+    customarily used for software interchange.
+
+    b) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by a
+    written offer, valid for at least three years and valid for as
+    long as you offer spare parts or customer support for that product
+    model, to give anyone who possesses the object code either (1) a
+    copy of the Corresponding Source for all the software in the
+    product that is covered by this License, on a durable physical
+    medium customarily used for software interchange, for a price no
+    more than your reasonable cost of physically performing this
+    conveying of source, or (2) access to copy the
+    Corresponding Source from a network server at no charge.
+
+    c) Convey individual copies of the object code with a copy of the
+    written offer to provide the Corresponding Source.  This
+    alternative is allowed only occasionally and noncommercially, and
+    only if you received the object code with such an offer, in accord
+    with subsection 6b.
+
+    d) Convey the object code by offering access from a designated
+    place (gratis or for a charge), and offer equivalent access to the
+    Corresponding Source in the same way through the same place at no
+    further charge.  You need not require recipients to copy the
+    Corresponding Source along with the object code.  If the place to
+    copy the object code is a network server, the Corresponding Source
+    may be on a different server (operated by you or a third party)
+    that supports equivalent copying facilities, provided you maintain
+    clear directions next to the object code saying where to find the
+    Corresponding Source.  Regardless of what server hosts the
+    Corresponding Source, you remain obligated to ensure that it is
+    available for as long as needed to satisfy these requirements.
+
+    e) Convey the object code using peer-to-peer transmission, provided
+    you inform other peers where the object code and Corresponding
+    Source of the work are being offered to the general public at no
+    charge under subsection 6d.
+
+  A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+  A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling.  In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage.  For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product.  A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+  "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source.  The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+  If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information.  But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+  The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed.  Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+  Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+  7. Additional Terms.
+
+  "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law.  If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+  When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it.  (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.)  You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+  Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+    a) Disclaiming warranty or limiting liability differently from the
+    terms of sections 15 and 16 of this License; or
+
+    b) Requiring preservation of specified reasonable legal notices or
+    author attributions in that material or in the Appropriate Legal
+    Notices displayed by works containing it; or
+
+    c) Prohibiting misrepresentation of the origin of that material, or
+    requiring that modified versions of such material be marked in
+    reasonable ways as different from the original version; or
+
+    d) Limiting the use for publicity purposes of names of licensors or
+    authors of the material; or
+
+    e) Declining to grant rights under trademark law for use of some
+    trade names, trademarks, or service marks; or
+
+    f) Requiring indemnification of licensors and authors of that
+    material by anyone who conveys the material (or modified versions of
+    it) with contractual assumptions of liability to the recipient, for
+    any liability that these contractual assumptions directly impose on
+    those licensors and authors.
+
+  All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10.  If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term.  If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+  If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+  Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+  8. Termination.
+
+  You may not propagate or modify a covered work except as expressly
+provided under this License.  Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+  However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+  Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+  Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License.  If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+  9. Acceptance Not Required for Having Copies.
+
+  You are not required to accept this License in order to receive or
+run a copy of the Program.  Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance.  However,
+nothing other than this License grants you permission to propagate or
+modify any covered work.  These actions infringe copyright if you do
+not accept this License.  Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+  10. Automatic Licensing of Downstream Recipients.
+
+  Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License.  You are not responsible
+for enforcing compliance by third parties with this License.
+
+  An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations.  If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+  You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License.  For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+  11. Patents.
+
+  A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based.  The
+work thus licensed is called the contributor's "contributor version".
+
+  A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version.  For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+  Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+  In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement).  To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+  If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients.  "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+
+  If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+  A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License.  You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+  Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+  12. No Surrender of Others' Freedom.
+
+  If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all.  For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+  13. Remote Network Interaction; Use with the GNU General Public License.
+
+  Notwithstanding any other provision of this License, if you modify the
+Program, your modified version must prominently offer all users
+interacting with it remotely through a computer network (if your version
+supports such interaction) an opportunity to receive the Corresponding
+Source of your version by providing access to the Corresponding Source
+from a network server at no charge, through some standard or customary
+means of facilitating copying of software.  This Corresponding Source
+shall include the Corresponding Source for any work covered by version 3
+of the GNU General Public License that is incorporated pursuant to the
+following paragraph.
+
+  Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU General Public License into a single
+combined work, and to convey the resulting work.  The terms of this
+License will continue to apply to the part which is the covered work,
+but the work with which it is combined will remain governed by version
+3 of the GNU General Public License.
+
+  14. Revised Versions of this License.
+
+  The Free Software Foundation may publish revised and/or new versions of
+the GNU Affero General Public License from time to time.  Such new versions
+will be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+  Each version is given a distinguishing version number.  If the
+Program specifies that a certain numbered version of the GNU Affero General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation.  If the Program does not specify a version number of the
+GNU Affero General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+  If the Program specifies that a proxy can decide which future
+versions of the GNU Affero General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+  Later license versions may give you additional or different
+permissions.  However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+  15. Disclaimer of Warranty.
+
+  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. Limitation of Liability.
+
+  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+  17. Interpretation of Sections 15 and 16.
+
+  If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+                     END OF TERMS AND CONDITIONS
+
+            How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU Affero General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU Affero General Public License for more details.
+
+    You should have received a copy of the GNU Affero General Public License
+    along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+Also add information on how to contact you by electronic and paper mail.
+
+  If your software can interact with users remotely through a computer
+network, you should also make sure that it provides a way for users to
+get its source.  For example, if your program is a web application, its
+interface could display a "Source" link that leads users to an archive
+of the code.  There are many ways you could offer source, and different
+solutions will be better for different programs; see section 13 for the
+specific requirements.
+
+  You should also get your employer (if you work as a programmer) or school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.
+For more information on this, and how to apply and follow the GNU AGPL, see
+<https://www.gnu.org/licenses/>.

README.md

@@ -0,0 +1,15 @@
+---
+license: agpl-3.0
+tags:
+- snapkitty
+- october-2026-drop
+- j
+- goldilocks-field
+- spectral
+- contraction
+- banach
+- research
+---
+
+> Mirrored from [https://github.com/SNAPKITTYWEST/foundry-j](https://github.com/SNAPKITTYWEST/foundry-j) at commit `cee36b3`. Part of the **SnapKitty October 2026 main drop**.
+

j/BOXING.md

@@ -0,0 +1,131 @@
+<!--
+  Copyright (C) 2026 Foundry / Prime Materia Commons
+  SPDX-License-Identifier: AGPL-3.0-or-later
+
+  This file is part of Foundry F1 Pure-J Core.
+  License: GNU Affero General Public License v3.0 or later.
+  See <https://www.gnu.org/licenses/>.
+-->
+
+# Foundry J Core — Record boxing contracts
+
+Field **order** is owned by `spec/J_API.md`. This file freezes the **boxing / nesting** used by Pure-J Core under `j/` so `;` (link) never flattens multi-field records into sibling boxes when paired with another value.
+
+## J link hazard (why wrap)
+
+In J9, `x ; y` with **unboxed** `x` and **list-of-boxes** `y` yields `(<x) , y` — the fields of `y` become siblings of `x`. Multi-field records must therefore be wrapped in **one outer box** whenever they are:
+
+- returned alone as a record value, or
+- linked with another value (`value ; <record>`).
+
+Atoms and plain numeric arrays are not list-of-boxes; `xi ; lam` with two numeric arrays is already length-stable.
+
+## StepInfo (length 7)
+
+Open field list (J_API order):
+
+```text
+step ; q ; epsilon ; n_xi ; n_lam ; projected ; residual
+```
+
+| Producer | Return shape |
+|----------|----------------|
+| `rec_step` | `x_next ; <StepInfo>` — always length 2 |
+| `rec_run` | list of `<StepInfo>` (one box per step) |
+| `REC_STATE` | `x_current ; converged ; <history>` — length 3; `history` is the same list `rec_run` returns |
+
+Unpack:
+
+```j
+'x info' =. x rec_step ...          NB. info is still boxed
+info =. > info                      NB. open length-7 StepInfo
+NB. or: info =. 1 {:: pair
+
+hist =. x0 rec_run ...
+step =. > k { hist                  NB. open StepInfo
+resid =. 6 {:: step                 NB. or > 6 { step
+```
+
+## SpectralResult (length 5)
+
+Open field list (J_API order):
+
+```text
+spectral_radius ; contractive ; gershgorin_bound ; power_iter_bound ; used_power_iteration
+```
+
+| Producer | Return shape |
+|----------|----------------|
+| `gershgorin_check` | `<SpectralResult>` |
+| `power_iteration_check` | `<SpectralResult>` |
+| `spectral_analyze` | `<SpectralResult>` |
+
+Unpack: `sr_open res` then index, or `1 {:: > res`, or `sr_contractive res`.
+`sr_open` is `>` (Core). Parenthesize: `sr_open (J spectral_analyze eps)`.
+
+Accessors `sr_radius` … `sr_used_pi` accept wrapped or open form.
+
+## AceCert (length 4)
+
+Open field list (J_API order):
+
+```text
+lipschitz_upper ; safety_margin ; tail_bound ; certified
+```
+
+| Producer | Return shape |
+|----------|----------------|
+| `ace_certify` | `<AceCert>` |
+
+`ace_certify` consumes a list of `<StepInfo>` (same packing as `rec_run` history).
+
+Unpack: `> ace` then field index, e.g. `3 {:: > ace` for `certified`.
+
+## PMat
+
+Open field list (shape used by Core today):
+
+```text
+rows ; cols ; entries
+```
+
+- `rows`, `cols` — integer atoms  
+- `entries` — numeric table `n×5`: `sign , delta_source , delta_target , row , col` (empty: `0 5 $ 0`)
+
+| Producer | Return shape |
+|----------|----------------|
+| `pmat_new` | open `rows ; cols ; entries` |
+| `pmat_compose` | open `rows ; cols ; entries` |
+| `pmat_insert` | **`new_PMat ; <ok>`** — length 2; `new_PMat` is the open 3-field PMat; `ok` is boolean 0/1 wrapped so the pair stays length-2 under link |
+
+Unpack insert:
+
+```j
+pair =. m pmat_insert row ; col ; sign ; sig
+m  =. 0 {:: pair          NB. open PMat
+ok =. 1 {:: pair          NB. boolean (opens <ok>)
+NB. 'm ok' =. pair  then  ok =. > ok
+```
+
+Accessors `pmat_rows` / `pmat_cols` / `pmat_entries` take the **open** PMat.
+
+`pmat_validate_grading` remains the C++ stub: always `1` (no invented checks).
+
+## Other multi-part returns
+
+| Producer | Return shape |
+|----------|----------------|
+| `synth_weights` | `xi_schedule ; lambda_schedule` — length 2; each a numeric table |
+| `soft_project` | `xi ; lam` — length 2; each a numeric list |
+
+Both sides are unboxed numerics, so bare `;` is length-stable. Do not link an unboxed value onto these pairs without wrapping the pair: `value ; <(xi;lam)>`.
+
+## Summary preference
+
+| Situation | Shape |
+|-----------|--------|
+| Record alone | `<record>` (StepInfo items in history; SpectralResult; AceCert) |
+| Value + record | `value ; <record>` (`rec_step`; conceptually same nesting for insert) |
+| PMat alone | open `rows ; cols ; entries` |
+| PMat + ok | `PMat ; <ok>` |
+| Numeric pair | `a ; b` (schedules / soft_project) |

j/certify.ijs

@@ -0,0 +1,57 @@
+NB. =============================================================================
+NB. Foundry F1 — AceCertificate math (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md § ace_*; PROPERTIES §H (53–54); j/BOXING.md.
+NB. AceCert open fields: lipschitz_upper ; safety_margin ; tail_bound ; certified
+NB. ace_certify returns <AceCert>.
+NB. Verbs: ace_safety_margin ace_tail_bound ace_certify
+
+cocurrent 'foundry'
+
+NB. max_q ace_safety_margin epsilon → (1-ε) - max_q  (PROPERTIES 53)
+ace_safety_margin =: 4 : '(1 - y) - x'
+
+NB. tail_norm ace_tail_bound max_q → tail/(1-max_q) or _ if max_q>=1 (PROPERTIES 54)
+ace_tail_bound =: 4 : 0
+  if. y >: 1 do. _ else. x % 1 - y end.
+)
+
+NB. steps ace_certify delta
+NB. steps = list of <StepInfo> (same packing as rec_run history)
+NB. Returns <AceCert>
+ace_certify =: 4 : 0
+  steps =. boxxopen x
+  delta =. y
+  if. 0 = # steps do. < 0 ; 0 ; 0 ; 0 return. end.
+  qs =. 0 $ 0.
+  rs =. 0 $ 0.
+  for_s. steps do.
+    info =. > s
+    qs =. qs , 1 {:: info
+    rs =. rs , 6 {:: info
+  end.
+  max_q =. >./ qs
+  max_resid =. >./ rs
+  eps =. 2 {:: > 0 { steps
+  margin =. max_q ace_safety_margin eps
+  tail =. max_resid ace_tail_bound max_q
+  certified =. margin >: delta
+  < max_q ; margin ; tail ; certified
+)
+
+cocurrent 'base'

j/foundry.ijs

@@ -0,0 +1,57 @@
+NB. =============================================================================
+NB. Foundry F1 — Pure-J Core package loader
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Load order matches dependency: types → goldilocks → pmat → spectral →
+NB. recurrence → gate → certify.
+NB. Record boxing contracts: j/BOXING.md (StepInfo, SpectralResult, AceCert, PMat).
+NB.
+NB. Usage (from any cwd):
+NB.   load '/workspace/foundry-j/j/foundry.ijs'
+NB. Then verbs live in locale 'foundry'; bring into base with:
+NB.   cocurrent 'foundry'   NB. or call as foundry_fp_add_ etc.
+
+(3 : 0) ''
+here =. ({.~ i:&'/') > {: 4!:3 ''
+if. 0 = # here do. here =. 1!:43 '' end.
+sep =. '/'
+mods =. 'types';'goldilocks';'pmat';'spectral';'recurrence';'gate';'certify'
+for_m. mods do.
+  load here , sep , (> m) , '.ijs'
+end.
+i. 0 0
+)
+
+NB. Optional: export key verbs into base for Verify convenience
+NB. Uncomment if desired:
+NB. (3 : 0) ''
+NB. names =. ;: 'fp_add fp_sub fp_mul fp_inv fp_mulmod fp_pow fp_reduce fp_add_batch fp_mul_batch pmat_new pmat_insert pmat_conservation pmat_compose pmat_frobenius pmat_validate_grading gershgorin_bound gershgorin_check power_iteration power_iteration_check spectral_analyze synth_weights soft_project q_estimate residual_l2 rec_step rec_run tier_eps emit_apply csl_neutrality csl_beneficence csl_commutation ace_safety_margin ace_tail_bound ace_certify GOLDILOCKS_PRIME p EPSILON_FOLD P64'
+NB. for_n. names do.
+NB.   (n) =: (n) f.   NB. not valid across locales this way
+NB. end.
+NB. i.0 0
+NB. )
+
+NB. Instead expose a verb that copies selected names into base:
+foundry_export =: 3 : 0
+  ns =. ;: 'fp_reduce fp_add fp_sub fp_mul fp_mulmod fp_pow fp_inv fp_add_batch fp_mul_batch pmat_new pmat_insert pmat_validate_grading pmat_conservation pmat_compose pmat_frobenius pmat_entries pmat_shape gershgorin_bound gershgorin_check power_iteration power_iteration_check spectral_analyze sr_open sr_fields sr_radius sr_contractive synth_weights soft_project q_estimate residual_l2 rec_step rec_run tier_eps tier_epsilon emit_apply csl_neutrality csl_beneficence csl_commutation ace_safety_margin ace_tail_bound ace_certify GOLDILOCKS_PRIME p EPSILON_FOLD P64 P_64 K_MAX MAX_DRIFT PHI PIRTM_MAGIC T1 T2 T3 T4 WP_UNIFORM WP_HARMONIC WP_LOGDECAY GP_PASSTHROUGH GP_SUPPRESS GP_HOLD GP_ATTENUATE CSL_PASS CSL_FAIL_NEUTRALITY CSL_FAIL_BENEFICENCE CSL_FAIL_COMMUTATION'
+  cocurrent 'base'
+  for_n. ns do.
+    ". (>n) , ' =: ' , (>n) , '_foundry_'
+  end.
+  i. 0 0
+)

j/gate.ijs

@@ -0,0 +1,110 @@
+NB. =============================================================================
+NB. Foundry F1 — Emission Gate + CSL checks (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md § Emission/CSL; PROPERTIES §H (48–52).
+NB. Verbs: emit_apply csl_neutrality csl_beneficence csl_commutation
+NB. Verdicts: CSL_PASS CSL_FAIL_NEUTRALITY CSL_FAIL_BENEFICENCE CSL_FAIL_COMMUTATION
+NB. Policies: GP_PASSTHROUGH GP_SUPPRESS GP_HOLD GP_ATTENUATE  (types.ijs)
+
+cocurrent 'foundry'
+
+NB. ── emit_apply ──────────────────────────────────────────────────────────────
+NB. out emit_apply (prev ; q ; policy ; epsilon)
+NB. PassThrough: out
+NB. Suppress: zeros if q >= 1-ε else out          (PROPERTIES 48)
+NB. Hold: prev if q >= 1-ε else out
+NB. Attenuate: out * max(0, (1-ε)-q)  NB. parens: J is RTL (PROPERTIES 49)
+emit_apply =: 4 : 0
+  out =. , x
+  y =. boxxopen y
+  prev =. , > 0 { y
+  q    =. 0 ". ": > 1 { y
+  pol  =. 0 ". ": > 2 { y
+  eps  =. 0 ". ": > 3 { y , <0.1
+  select. pol
+  case. GP_PASSTHROUGH do. out
+  case. GP_SUPPRESS do.
+    if. q >: 1 - eps do. (# out) $ 0. else. out end.
+  case. GP_HOLD do.
+    if. q >: 1 - eps do. prev else. out end.
+  case. GP_ATTENUATE do.
+    scale =. 0 >. (1 - eps) - q
+    out * scale
+  case. do. out
+  end.
+)
+
+NB. ── csl_neutrality ──────────────────────────────────────────────────────────
+NB. x csl_neutrality (Tx ; epsilon)
+NB. Fail if |xi-xj|>1e_15 and |Ti-Tj|/|xi-xj| > 1+ε  (PROPERTIES 50)
+csl_neutrality =: 4 : 0
+  xv =. , x
+  y =. boxxopen y
+  Tx =. , > 0 { y
+  eps =. 0 ". ": > 1 { y , <0.1
+  n =. # xv
+  verdict =. CSL_PASS
+  for_i. i. n do.
+    for_j. (i + 1) + i. 0 >. (n - i) - 1 do.
+      dx =. | (i { xv) - j { xv
+      dT =. | (i { Tx) - j { Tx
+      if. (dx > 1e_15) *. ((dT % dx) > 1 + eps) do.
+        verdict =. CSL_FAIL_NEUTRALITY
+      end.
+    end.
+  end.
+  verdict
+)
+
+NB. ── csl_beneficence ─────────────────────────────────────────────────────────
+NB. x csl_beneficence (Tx ; residual ; epsilon)
+NB. ‖T(x)‖_2 ≤ (1+ε)‖x‖_2 and residual ≤ (1+ε)‖x‖_2  (PROPERTIES 51)
+csl_beneficence =: 4 : 0
+  xv =. , x
+  y =. boxxopen y
+  Tx =. , > 0 { y
+  resid =. 0 ". ": > 1 { y
+  eps =. 0 ". ": > 2 { y , <0.1
+  norm_x =. %: xv +/ . * xv
+  norm_Tx =. %: Tx +/ . * Tx
+  if. (norm_x > 1e_15) *. (norm_Tx > (1 + eps) * norm_x) do.
+    CSL_FAIL_BENEFICENCE return.
+  end.
+  if. resid > (1 + eps) * norm_x do.
+    CSL_FAIL_BENEFICENCE return.
+  end.
+  CSL_PASS
+)
+
+NB. ── csl_commutation ─────────────────────────────────────────────────────────
+NB. x csl_commutation (T_hook ; filter_hook ; epsilon)
+NB. ‖filter(T(x)) - T(filter(x))‖_∞ ≤ ε  (PROPERTIES 52)
+csl_commutation =: 4 : 0
+  xv =. , x
+  y =. boxxopen y
+  Th =. 0 { y
+  Fh =. 1 { y
+  eps =. 0 ". ": > 2 { y , <0.1
+  Tx  =. xv apply_hook Th
+  fTx =. Tx apply_hook Fh
+  fx  =. xv apply_hook Fh
+  Tfx =. fx apply_hook Th
+  if. +./ eps < | fTx - Tfx do. CSL_FAIL_COMMUTATION else. CSL_PASS end.
+)
+
+cocurrent 'base'

j/goldilocks.ijs

@@ -0,0 +1,95 @@
+NB. =============================================================================
+NB. Foundry F1 — Goldilocks F_p arithmetic (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md § Goldilocks; PROPERTIES §A–C (1–18).
+NB. Carrier Fp: extended int with 0 ≤ v < p.
+NB.
+NB. Verbs: fp_reduce fp_add fp_sub fp_mul fp_mulmod fp_pow fp_inv
+NB.        fp_add_batch fp_mul_batch
+
+cocurrent 'foundry'
+
+NB. fp_reduce y — single-limb: (y >= p) ? y-p : y   (PROPERTIES 12)
+fp_reduce =: 3 : 0"0
+  y =. x: y
+  if. y >: p do. y - p else. y end.
+)
+
+NB. fp_mulmod x y — Goldilocks fold (PROPERTIES 5–11)
+NB. 2^64 ≡ 2^32-1 (mod p); x ≡ lo + hi_lo*EPSILON_FOLD - hi_hi (mod p)
+fp_mulmod =: 4 : 0"0
+  a =. x: x
+  b =. x: y
+  product =. a * b
+  lo    =. TWO64 | product
+  hi    =. product <.@% TWO64
+  hi_lo =. TWO32 | hi  NB. C++: hi & 0xFFFFFFFFull (= mod 2^32), not mod EPSILON_FOLD
+  hi_hi =. hi <.@% TWO32
+  folded =. lo + hi_lo * EPSILON_FOLD
+  if. folded >: hi_hi do.
+    reduced =. folded - hi_hi
+  else.
+    reduced =. folded + p - hi_hi
+  end.
+  if. reduced >: p do. reduced =. reduced - p end.
+  reduced
+)
+
+NB. fp_add x y — (a+b) mod p (PROPERTIES 13)
+fp_add =: 4 : 0"0
+  r =. (x: x) + (x: y)
+  if. r >: p do. r =. r - p end.
+  r
+)
+
+NB. fp_sub x y — (a-b) mod p with underflow +p (PROPERTIES 14)
+fp_sub =: 4 : 0"0
+  r =. (x: x) - (x: y)
+  if. r < 0x do. r =. r + p end.
+  r
+)
+
+NB. fp_mul x y — mulmod (PROPERTIES 15)
+fp_mul =: 4 : 0"0
+  x fp_mulmod y
+)
+
+NB. fp_pow x y — square-and-multiply x^y mod p (PROPERTIES 17)
+fp_pow =: 4 : 0
+  a =. x: x
+  e =. x: y
+  result =. 1x
+  base =. a
+  while. e > 0x do.
+    if. 1x = 2x | e do. result =. result fp_mul base end.
+    base =. base fp_mul base
+    e =. e <.@% 2x
+  end.
+  result
+)
+
+NB. fp_inv y — Fermat a^(p-2) (PROPERTIES 16)
+fp_inv =: 3 : 0
+  y fp_pow (p - 2x)
+)
+
+NB. Batch elementwise (PROPERTIES 18) — same verbs, list rank
+fp_add_batch =: fp_add"0
+fp_mul_batch =: fp_mul"0
+
+cocurrent 'base'

j/pmat.ijs

@@ -0,0 +1,122 @@
+NB. =============================================================================
+NB. Foundry F1 — Prime Monomial Matrix / PMAT (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md § PMAT; PROPERTIES §E (26–32); GAP_DECISIONS §3–4; j/BOXING.md.
+NB. PMat open fields: rows ; cols ; entries
+NB. entries = n×5 table: sign, delta_source, delta_target, row, col
+NB. Signature = length-2 list (delta_source, delta_target)
+NB. pmat_insert returns new_PMat ; <ok>  (length 2; see BOXING.md)
+NB.
+NB. Verbs: pmat_new pmat_insert pmat_validate_grading pmat_conservation
+NB.        pmat_compose pmat_frobenius
+NB. Accessors: pmat_rows pmat_cols pmat_entries pmat_shape
+
+cocurrent 'foundry'
+
+NB. rows pmat_new cols  → empty PMat
+pmat_new =: 4 : 0
+  (x ; y ; (0 5 $ 0))
+)
+
+pmat_rows    =: 0 {:: ]
+pmat_cols    =: 1 {:: ]
+pmat_entries =: 2 {:: ]
+pmat_shape   =: 3 : '(pmat_rows y) , (pmat_cols y)'
+
+NB. m pmat_insert (row ; col ; sign ; Signature)
+NB. Signature may be length-2 list or two trailing atoms ds,dt
+NB. Returns new_PMat ; <ok>  (BOXING.md). ok=0 on bounds/sign failure only
+NB. (PROPERTIES 27 / GAP_DECISIONS §3 — no signature↔grade checks).
+pmat_insert =: 4 : 0
+  args =. y
+  if. 1 = L. args do.
+    'r c s sig' =. 4 {. args , 4 $ a:
+    if. 1 = L. sig do. sig =. > sig end.
+    'ds dt' =. 2 {. sig , 0 0
+  else.
+    'r c s ds dt' =. 5 {. args , 5 $ 0
+  end.
+  rows =. pmat_rows x
+  cols =. pmat_cols x
+  ents =. pmat_entries x
+  ok =. 1
+  if. (r >: rows) +. (r < 0) do. ok =. 0 end.
+  if. (c >: cols) +. (c < 0) do. ok =. 0 end.
+  if. -. s e. _1 1 do. ok =. 0 end.
+  if. ok do.
+    ents =. ents , s , ds , dt , r , c
+    (rows ; cols ; ents) ; <ok
+  else.
+    x ; <ok
+  end.
+)
+
+NB. Mirror C++ stub: always true (PROPERTIES 28 gap / GAP_DECISIONS §3)
+pmat_validate_grading =: 3 : '1'
+
+NB. Σ monomials → Signature (PROPERTIES 29)
+pmat_conservation =: 3 : 0
+  ents =. pmat_entries y
+  if. 0 = # ents do. 0 0 else. +/ 1 2 {"1 ents end.
+)
+
+NB. a pmat_compose b — sign *= ; ds += a.delta_source only ; dt += b.delta_target only
+NB. (PROPERTIES 31 as coded / GAP_DECISIONS §4 — not full both-signature sum)
+pmat_compose =: 4 : 0
+  a =. x
+  b =. y
+  rA =. pmat_rows a
+  cB =. pmat_cols b
+  eA =. pmat_entries a
+  eB =. pmat_entries b
+  if. (0 = # eA) +. (0 = # eB) do. rA pmat_new cB return. end.
+  acc =. 0 5 $ 0
+  for_i. i. rA do.
+    for_j. i. cB do.
+      sign_acc =. 1
+      mon_ds =. 0
+      mon_dt =. 0
+      any =. 0
+      arows =. eA #~ i = 3 {"1 eA
+      brows =. eB #~ j = 4 {"1 eB
+      for_ai. i. # arows do.
+        ea =. ai { arows
+        acol =. 4 { ea
+        for_bi. i. # brows do.
+          eb =. bi { brows
+          if. acol = 3 { eb do.
+            sign_acc =. sign_acc * (0 { ea) * (0 { eb)
+            mon_ds =. mon_ds + 1 { ea
+            mon_dt =. mon_dt + 2 { eb
+            any =. 1
+          end.
+        end.
+      end.
+      if. any do.
+        if. sign_acc >: 0 do. sign_acc =. 1 else. sign_acc =. _1 end.
+        acc =. acc , sign_acc , mon_ds , mon_dt , i , j
+      end.
+    end.
+  end.
+  rA ; cB ; acc
+)
+
+NB. Frobenius = sqrt(#entries) (PROPERTIES 32)
+pmat_frobenius =: 3 : '%: # pmat_entries y'
+
+cocurrent 'base'

j/recurrence.ijs

@@ -0,0 +1,194 @@
+NB. =============================================================================
+NB. Foundry F1 — Banach Contraction Recurrence (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md § Banach recurrence; PROPERTIES §G (39–46); j/BOXING.md.
+NB. Equation: x_{t+1} = Ξ_t · x_t + Λ_t · T(x_t) + g_t
+NB. Constraint: q_t = ‖Ξ‖ + ‖Λ‖·‖T‖ < 1 - ε
+NB.
+NB. Verbs: synth_weights soft_project q_estimate residual_l2 rec_step rec_run
+NB.        (tier_eps lives in types.ijs)
+NB.
+NB. StepInfo open fields (length 7):
+NB.   step ; q ; epsilon ; n_xi ; n_lam ; projected ; residual
+NB. rec_step → x_next ; <StepInfo>
+NB. rec_run  → list of <StepInfo>
+NB. REC_STATE → x_current ; converged ; <history>
+NB. T / p_op hooks: boxed verb-name strings (or gerunds) resolved by apply_hook.
+
+cocurrent 'foundry'
+
+NB. x apply_hook boxed_fn — invoke rank-1→1 transform
+apply_hook =: 4 : 0
+  f =. > y
+  if. 2 = 3!:0 f do. (f)~ x else. f `: 6 x end.
+)
+
+NB. ── synth_weights ───────────────────────────────────────────────────────────
+NB. synth_weights max_steps;tier;profile;[primes]
+NB. Returns xi_schedule ; lambda_schedule (length 2; numeric tables) — BOXING.md
+NB. q_star=1-tier_eps; xi=q_star*factor*0.7; lam=q_star*factor*0.3 (PROPERTIES 44)
+synth_weights =: 3 : 0
+  y =. boxxopen y
+  max_steps =. 0 ". ": > 0 { y , <200
+  tier      =. 0 ". ": > 1 { y , <T1
+  profile   =. 0 ". ": > 2 { y , <WP_UNIFORM
+  q_star =. 1 - tier_eps tier
+  xi_s =. 0 2 $ 0.
+  lam_s =. 0 2 $ 0.
+  for_t. i. max_steps do.
+    select. profile
+    case. WP_HARMONIC do. factor =. % t + 1.
+    case. WP_LOGDECAY do. factor =. % ^. t + 2.
+    case. do.             factor =. 1.
+    end.
+    xi_s  =. xi_s  , (q_star * factor * 0.7) , 0.
+    lam_s =. lam_s , 0. , (q_star * factor * 0.3)
+  end.
+  xi_s ; lam_s
+:
+  synth_weights x
+)
+
+NB. ── soft_project ────────────────────────────────────────────────────────────
+NB. (xi ; lam) soft_project (q ; eps)  — scale by (1-eps)/q if q>1-eps
+NB. Returns xi ; lam (length 2; numeric lists) — BOXING.md
+soft_project =: 4 : 0
+  'xi lam' =. x
+  xi =. , > xi
+  lam =. , > lam
+  'q eps' =. 2 {. (,y) , 0 0.1
+  target =. 1 - eps
+  if. q <: target do. xi ; lam
+  else. scale =. target % q
+        (xi * scale) ; (lam * scale)
+  end.
+)
+
+NB. ── q_estimate ──────────────────────────────────────────────────────────────
+NB. q_estimate xi;lam;x;Tx  (PROPERTIES 42)
+q_estimate =: 3 : 0
+  'xi lam xv Tx' =. y
+  xi =. , > xi
+  lam =. , > lam
+  xv =. , > xv
+  Tx =. , > Tx
+  n_xi =. >./ | xi
+  n_lam =. >./ | lam
+  n_T =. >./ | Tx
+  n_x =. >./ | xv
+  if. n_x > 1e_15 do. n_T =. n_T % n_x end.
+  n_xi + n_lam * n_T
+)
+
+NB. ── residual_l2 ─────────────────────────────────────────────────────────────
+NB. x_next residual_l2 x_t → ‖x'-x‖_2
+residual_l2 =: 4 : 0
+  d =. (,x) - ,y
+  %: d +/ . * d
+)
+
+NB. weight at component i (C++: xi[min(i,1)])
+wt_at =: 4 : '((y <. 1) { , x)'
+
+NB. ── rec_step ────────────────────────────────────────────────────────────────
+NB. x_t rec_step xi;lam;g;T_hook;p_hook;[step_idx];[tier]
+NB. Returns x_next ; <StepInfo>  (length 2 — BOXING.md)
+rec_step =: 4 : 0
+  xv =. , x
+  y =. boxxopen y
+  xi  =. , > 0 { y
+  lam =. , > 1 { y
+  g   =. , > 2 { y
+  Th  =. 3 { y
+  Ph  =. 4 { y
+  if. 0 = # g do. g =. (# xv) $ 0. end.
+  if. 5 < # y do. step_idx =. 0 ". ": > 5 { y else. step_idx =. 0 end.
+  if. 6 < # y do. tier =. 0 ". ": > 6 { y else. tier =. T1 end.
+  eps =. tier_eps tier
+  dim =. # xv
+
+  Tx =. xv apply_hook Th
+  q =. q_estimate xi ; lam ; xv ; Tx
+  projected =. 0
+  xi_use =. xi
+  lam_use =. lam
+  if. q > 1 - eps do.
+    sp =. (xi ; lam) soft_project q , eps
+    xi_use =. , > 0 { sp
+    lam_use =. , > 1 { sp
+    q =. q_estimate xi_use ; lam_use ; xv ; Tx
+    projected =. 1
+  end.
+  n_xi =. >./ | xi_use
+  n_lam =. >./ | lam_use
+
+  x_next =. dim $ 0.
+  for_i. i. dim do.
+    val =. ((xi_use wt_at i) * i { xv) + ((lam_use wt_at i) * i { Tx) + i { g
+    x_next =. val i} x_next
+  end.
+  x_next =. x_next apply_hook Ph
+  resid =. x_next residual_l2 xv
+  info =. step_idx ; q ; eps ; n_xi ; n_lam ; projected ; resid
+  x_next ; <info
+)
+
+NB. ── rec_run ─────────────────────────────────────────────────────────────────
+NB. x0 rec_run max_steps;tier;profile;tol;T_hook;p_hook
+NB. Returns list of <StepInfo> (Verify prop 46 via this history).
+NB. Sets REC_STATE =: x_current ; converged ; <history>  (length 3)
+rec_run =: 4 : 0
+  x0 =. , x
+  y =. boxxopen y
+  max_steps =. 0 ". ": > 0 { y , <200
+  tier      =. 0 ". ": > 1 { y , <T1
+  profile   =. 0 ". ": > 2 { y , <WP_UNIFORM
+  tol       =. 0 ". ": > 3 { y , <1e_6
+  Th =. 4 { y , <'['
+  Ph =. 5 { y , <'['
+  if. 0 = max_steps do. max_steps =. 200 end.
+  if. 0 = tol do. tol =. 1e_6 end.
+
+  sched =. synth_weights max_steps ; tier ; profile
+  xi_s =. > 0 { sched
+  lam_s =. > 1 { sched
+  g =. (# x0) $ 0.
+  xc =. x0
+  history =. 0 $ a:
+  converged =. 0
+
+  for_t. i. max_steps do.
+    xi =. t { xi_s
+    lam =. t { lam_s
+    pair =. xc rec_step xi ; lam ; g ; Th ; Ph ; t ; tier
+    xc =. , > 0 { pair
+    info =. > 1 { pair
+    history =. history , <info
+    resid =. 6 {:: info
+    if. resid < tol do. converged =. 1 break. end.
+  end.
+
+  REC_STATE =: xc ; converged ; <history
+  history
+)
+
+rec_state_x         =: 0 {:: ]
+rec_state_converged =: 1 {:: ]
+rec_state_history   =: 2 {:: ]
+
+cocurrent 'base'

j/spectral.ijs

@@ -0,0 +1,106 @@
+NB. =============================================================================
+NB. Foundry F1 — Spectral Governor (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md § Spectral; PROPERTIES §F (33–38); j/BOXING.md.
+NB. Jacobian = n×n real matrix.
+NB. SpectralResult open fields:
+NB.   spectral_radius ; contractive ; gershgorin_bound ;
+NB.   power_iter_bound ; used_power_iteration
+NB. Producers return <SpectralResult> (one outer box) — see BOXING.md.
+NB.
+NB. Verbs: gershgorin_bound gershgorin_check power_iteration
+NB.        power_iteration_check spectral_analyze
+
+cocurrent 'foundry'
+
+NB. gershgorin_bound J (PROPERTIES 33)
+gershgorin_bound =: 3 : 0
+  J =. y
+  n =. # J
+  if. 0 = n do. 0 return. end.
+  bounds =. 0 $ 0.
+  for_i. i. n do.
+    row =. i { J
+    diag =. | i { row
+    off  =. +/ | (i ~: i. n) # row
+    bounds =. bounds , diag + off
+  end.
+  >./ bounds
+)
+
+NB. J gershgorin_check epsilon — contractive iff bound < 1-ε (PROPERTIES 34)
+NB. Returns <SpectralResult>
+gershgorin_check =: 4 : 0
+  bound =. gershgorin_bound x
+  contractive =. bound < (1 - y)
+  < bound ; contractive ; bound ; bound ; 0
+)
+
+NB. J power_iteration (max_iters , tol)
+NB. Defaults: max_iters=100, tol=1e_12 (PROPERTIES 35)
+power_iteration =: 4 : 0
+  J =. x
+  'max_iters tol' =. 2 {. (,y) , 100 1e_12
+  n =. # J
+  if. 0 = n do. 0 return. end.
+  v =. n $ %: % n
+  eigenvalue =. 0.
+  for_iter. i. max_iters do.
+    Jv =. J +/ . * v
+    new_ev =. v +/ . * Jv
+    if. tol > | new_ev - eigenvalue do. | new_ev return. end.
+    eigenvalue =. new_ev
+    norm =. %: Jv +/ . * Jv
+    if. norm < 1e_15 do. break. end.
+    v =. Jv % norm
+  end.
+  | eigenvalue
+)
+
+NB. J power_iteration_check (epsilon , max_iters) (PROPERTIES 36)
+NB. Returns <SpectralResult>
+power_iteration_check =: 4 : 0
+  'eps max_iters' =. 2 {. (,y) , 0.1 100
+  bound =. x power_iteration max_iters , 1e_12
+  gersho =. gershgorin_bound x
+  contractive =. bound < (1 - eps)
+  < bound ; contractive ; gersho ; bound ; 1
+)
+
+NB. J spectral_analyze epsilon (PROPERTIES 37)
+NB. Gershgorin first; if contractive but bound > 0.95*(1-ε), power-iterate
+NB. Returns <SpectralResult>
+spectral_analyze =: 4 : 0
+  result =. > x gershgorin_check y
+  'sr c gersh pi used' =. result
+  if. c *. (gersh > 0.95 * 1 - y) do.
+    result =. > x power_iteration_check y , 100
+  end.
+  < result
+)
+
+NB. SpectralResult accessors — accept <SpectralResult> (L.>1) or open fields
+sr_open        =: >
+sr_fields      =: 3 : 'if. 1 < L. y do. > y else. y end.'
+sr_radius      =: 0 {:: sr_fields
+sr_contractive =: 1 {:: sr_fields
+sr_gersh       =: 2 {:: sr_fields
+sr_power       =: 3 {:: sr_fields
+sr_used_pi     =: 4 {:: sr_fields
+
+cocurrent 'base'

j/types.ijs

@@ -0,0 +1,85 @@
+NB. =============================================================================
+NB. Foundry F1 — Shared types and constants (PURE J)
+NB. Copyright (C) 2026 Foundry / Prime Materia Commons
+NB.
+NB. This program is free software: you can redistribute it and/or modify
+NB. it under the terms of the GNU Affero General Public License as published
+NB. by the Free Software Foundation, either version 3 of the License, or
+NB. (at your option) any later version.
+NB.
+NB. This program is distributed in the hope that it will be useful,
+NB. but WITHOUT ANY WARRANTY; without even the implied warranty of
+NB. MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+NB. GNU Affero General Public License for more details.
+NB.
+NB. You should have received a copy of the GNU Affero General Public License
+NB. along with this program.  If not, see <https://www.gnu.org/licenses/>.
+NB. =============================================================================
+NB.
+NB. Contract: spec/J_API.md nouns + PROPERTIES.md §A,D (constants).
+NB. GAP_DECISIONS: EPSILON_FOLD fold noun; BARRITT_MU omitted (no Barrett path);
+NB. PHI exposed, no math consumer. Boxing: see j/BOXING.md.
+NB. Locale: foundry
+
+cocurrent 'foundry'
+
+NB. ── Field / system constants (PROPERTIES 1–2, 6, 19–24) ─────────────────────
+NB. GOLDILOCKS_PRIME = 2^64 - 2^32 + 1 = 0xFFFFFFFF00000001
+GOLDILOCKS_PRIME =: 18446744069414584321x
+p                =: GOLDILOCKS_PRIME
+NB. Fold constant EPSILON (README) / EPSILON_FOLD (J_API): 2^32 - 1
+EPSILON_FOLD     =: 4294967295x
+TWO64            =: 18446744073709551616x
+TWO32            =: 4294967296x
+
+K_MAX            =: 133144
+MAX_DRIFT        =: 300000000000000000x
+PIRTM_MAGIC      =: 2135945554x          NB. 0x7F504952
+PHI              =: 1.618033988749895
+GENESIS_HASH_SIZE=: 32
+
+NB. First 64 primes — types.h P_64 / J_API noun P64
+P64 =: 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 71 73 79 83 89 97 101 103 107 109 113 127 131 137 139 149 151 157 163 167 173 179 181 191 193 197 199 211 223 227 229 233 239 241 251 257 263 269 271 277 281 283 293 307 311
+P_64 =: P64                              NB. C++ name alias
+
+NB. ── Tier (PROPERTIES 25) ────────────────────────────────────────────────────
+NB. Tier atoms: 1=T1 2=T2 3=T3 4=T4
+T1 =: 1
+T2 =: 2
+T3 =: 3
+T4 =: 4
+
+NB. tier_eps / tier_epsilon — T1:0.10 T2:0.05 T3:0.02 T4:0.01; default 0.10
+tier_eps =: 3 : 0
+  select. y
+  case. 1 do. 0.10
+  case. 2 do. 0.05
+  case. 3 do. 0.02
+  case. 4 do. 0.01
+  case. do. 0.10
+  end.
+)
+tier_epsilon =: tier_eps
+
+NB. Weight profile codes (WeightProfile)
+WP_UNIFORM  =: 0
+WP_HARMONIC =: 1
+WP_LOGDECAY =: 2
+
+NB. GatePolicy (J_API)
+GP_PASSTHROUGH =: 0
+GP_SUPPRESS    =: 1
+GP_HOLD        =: 2
+GP_ATTENUATE   =: 3
+
+NB. CSLVerdict
+CSL_PASS              =: 0
+CSL_FAIL_NEUTRALITY   =: 1
+CSL_FAIL_BENEFICENCE  =: 2
+CSL_FAIL_COMMUTATION  =: 3
+
+NB. Signature helpers: length-2 integer list (delta_source, delta_target)
+sig_sub =: -
+sig_eq  =: -:
+
+cocurrent 'base'

spec/COVERAGE_MATRIX.md

@@ -0,0 +1,107 @@
+<!--
+  Copyright (C) 2026 Foundry J contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Coverage Matrix — PROPERTIES.md ↔ harness
+
+**Target commit:** `194e588` (pure-J Foundry F1).  
+**Sources:** `spec/PROPERTIES.md` (56 numbered properties); `verify/PROPERTY_MAP.md` (harness Primary/Related + measured results); `verify/INVENTORY.md` (non-mathematical / ignored note).  
+**Measured log:** `logs/run-20261007-061701.log` — PROPERTY_MAP reports **8 PASS / 1 FAIL / 0 BLOCKED** (not 9/9).  
+**No invented numbers.** Status definitions exactly as Spec brief.
+
+| Status | Definition |
+|--------|------------|
+| **covered** | Listed in PROPERTY_MAP as Primary # or Related # **and** measured **PASS** |
+| **partial** | Listed as Primary/Related but measured **FAIL**; **or** harness works around Core (e.g. recurrence via `rec_step` not `rec_run`); **or** emission / CSL / AceCert / WORM props called out as non-mathematical / ignored by harness |
+| **untested** | Not mentioned in PROPERTY_MAP Primary or Related columns (and not in the ignored 47–56 band) |
+
+---
+
+| Prop | Short name | Status | Evidence | Notes |
+|------|------------|--------|----------|-------|
+| 1 | Goldilocks prime (decimal) | covered | `goldilocks_add` (Related) | PASS in PROPERTY_MAP |
+| 2 | Goldilocks prime (hex / named constant) | covered | `goldilocks_add` (Related) | PASS in PROPERTY_MAP |
+| 3 | Field elements are u64 reduced mod p | covered | `goldilocks_add` (Related) | PASS in PROPERTY_MAP |
+| 4 | Elem construction reduces | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 5 | Congruence \(2^{64} \equiv 2^{32}-1 \pmod{p}\) | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 6 | Fold constant EPSILON | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 7 | 128-bit product split | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 8 | hi split into 32-bit halves | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 9 | Reduction identity (fold) | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 10 | Underflow handling on fold | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 11 | Final conditional reduction after fold | covered | `goldilocks_mul` (Related 5–11) | PASS in PROPERTY_MAP |
+| 12 | Single-limb reduce | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 13 | Addition mod p | covered | `goldilocks_add` (Primary) | PASS in PROPERTY_MAP; `verify/tests/goldilocks.ijs` |
+| 14 | Subtraction mod p | covered | `goldilocks_sub` (Primary) | PASS in PROPERTY_MAP; `verify/tests/goldilocks.ijs` |
+| 15 | Multiplication via mulmod | covered | `goldilocks_mul` (Primary) | PASS in PROPERTY_MAP; `verify/tests/goldilocks.ijs` |
+| 16 | Fermat inverse | partial | `goldilocks_inv` (Primary) | **covered-but-FAIL** — PROPERTY_MAP: `42*fp_inv(42)` → `11152786313141180820` (not 1); log `run-20261007-061701` |
+| 17 | Binary exponentiation | partial | `goldilocks_inv` (Related) | Listed with prop 16; same measured **FAIL** |
+| 18 | Batch add/mul | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 19 | K_MAX | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 20 | MAX_DRIFT | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 21 | PIRTM_MAGIC | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 22 | PHI | untested | none | Not in PROPERTY_MAP Primary/Related; see Gaps |
+| 23 | P_64 — first 64 primes | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 24 | GENESIS_HASH_SIZE | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 25 | Tier epsilons (contraction margins) | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 26 | PMat entry shape | covered | `pmat_insert` (Related) | PASS in PROPERTY_MAP |
+| 27 | Insert domain checks | covered | `pmat_insert` (Primary) | PASS in PROPERTY_MAP; `verify/tests/pmat.ijs` |
+| 28 | Grading condition (stated) | untested | none | Gap: `validate_grading` stub; not in harness map |
+| 29 | Conservation theorem | covered | `pmat_conservation` (Primary) | PASS in PROPERTY_MAP; `verify/tests/pmat.ijs` |
+| 30 | Composition preserves grading (stated) | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 31 | Compose monomial accumulation rule (as coded) | untested | none | Not in PROPERTY_MAP Primary/Related; see Gaps |
+| 32 | Frobenius norm of PMat | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 33 | Gershgorin disk bound | covered | `spectral_contractive`, `spectral_expansive` (Related) | PASS in PROPERTY_MAP |
+| 34 | Contractive test (Gershgorin) | covered | `spectral_contractive`, `spectral_expansive` (Related) | PASS in PROPERTY_MAP |
+| 35 | Power iteration (Rayleigh) | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 36 | Contractive test (power iteration) | untested | none | Not in PROPERTY_MAP Primary/Related |
+| 37 | Analyze fallback policy | covered | `spectral_contractive`, `spectral_expansive` (Related) | PASS in PROPERTY_MAP |
+| 38 | Tested contractive / expansive examples | covered | `spectral_contractive`, `spectral_expansive` (Primary) | PASS in PROPERTY_MAP; `verify/tests/spectral.ijs` |
+| 39 | Recurrence equation | partial | `recurrence_converges` (Related 39–45) | PASS measured, but PROPERTY_MAP notes harness loop via `synth_weights`+`rec_step`; Core `rec_run` still flattens StepInfo |
+| 40 | Contraction condition | partial | `recurrence_converges` (Related 39–45) | Same workaround note as prop 39 |
+| 41 | Unique fixed-point guarantee (narrative) | partial | `recurrence_converges` (Related 39–45) | Same workaround note as prop 39 |
+| 42 | q estimate in step (as coded) | partial | `recurrence_converges` (Related 39–45) | Same workaround note as prop 39 |
+| 43 | Soft projection | partial | `recurrence_converges` (Related 39–45) | Same workaround note as prop 39 |
+| 44 | Weight budget split | partial | `recurrence_converges` (Related 39–45) | Same workaround note as prop 39 |
+| 45 | Projector | partial | `recurrence_converges` (Related 39–45) | Same workaround note as prop 39 |
+| 46 | Residual | partial | `recurrence_converges` (Primary) | PASS measured via `rec_step` loop; PROPERTY_MAP: Core `rec_run` packing still broken (`x_next ; info` flattens) |
+| 47 | WORM / seal chain invariant (system-level) | partial | none (ignored) | INVENTORY: props 47–56 adjacent / gate-WORM theater, not in harness |
+| 48 | Emission Suppress | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 49 | Emission Attenuate scale | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 50 | CSL neutrality | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 51 | CSL beneficence | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 52 | CSL commutation | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 53 | AceCertificate safety margin | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 54 | AceCertificate tail bound | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 55 | Guardian spectral legality | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+| 56 | Consensus / false-positive bound (narrative) | partial | none (ignored) | INVENTORY non-mathematical / ignored by harness |
+
+---
+
+## Summary counts
+
+| Status | Count |
+|--------|------:|
+| covered | **20** |
+| partial | **20** |
+| untested | **16** |
+| **Total** | **56** |
+
+### Partial breakdown (for handoff)
+
+| Reason | Props | Count |
+|--------|-------|------:|
+| Measured FAIL (`goldilocks_inv`) | 16, 17 | 2 |
+| Harness workaround (`rec_step` / `rec_run` packing) | 39–46 | 8 |
+| Ignored / non-mathematical (INVENTORY 47–56) | 47–56 | 10 |
+
+### Harness measured (PROPERTY_MAP / log `run-20261007-061701`)
+
+| Result | Count | Detail |
+|--------|------:|--------|
+| PASS | 8 | `goldilocks_add`, `goldilocks_mul`, `goldilocks_sub`, `pmat_insert`, `pmat_conservation`, `spectral_contractive`, `spectral_expansive`, `recurrence_converges` |
+| FAIL | 1 | `goldilocks_inv` / prop **16** |
+| BLOCKED | 0 | — |
+
+Cite: `verify/PROPERTY_MAP.md` Summary counts; `verify/INVENTORY.md` Math count line.

spec/GAP_DECISIONS.md

@@ -0,0 +1,124 @@
+<!--
+  Copyright (C) 2026 Foundry J contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Gap Decisions — DRAFT for Core handoff
+
+**Status:** DRAFT. Spec rulings for Core against gaps listed in `spec/PROPERTIES.md` § Gaps.  
+**Target commit:** `194e588`.  
+**Policy:** Prefer **Match C++ as coded** when README prose and implementation disagree, unless README is the only statement of a math identity (then say so). **No invented numeric constants.** Alapeno remains out of scope.
+
+Sources for gap list: `spec/PROPERTIES.md` lines 269–276 (Gaps section).
+
+---
+
+## 1. EPSILON naming (README name vs `0xFFFFFFFFULL` literal)
+
+**Sources**
+
+- PROPERTIES Gaps: “Named C++ identifier `EPSILON`: named only in README Key Constants; code uses literal `0xFFFFFFFFULL` in mulmod, not a `types.h` symbol.”
+- Prop 6 cites: README.md § “Key Constants” (line 320); `src/goldilocks.cpp:27,31`.
+- `J_API.md` already exposes fold constant as noun `EPSILON_FOLD` (= `0xFFFFFFFF` = \(2^{32}-1\)), noting README name `EPSILON`.
+
+**Ruling:** **Match C++ as coded** (literal fold mask in mulmod path).
+
+**Rationale:** README supplies the name; the implementation never defines an `EPSILON` symbol in `types.h` — Core must implement the fold arithmetic with the same literal value, not invent a C++ identifier.
+
+**Done for Core**
+
+- Provide a named J noun for the fold constant (e.g. `EPSILON_FOLD` per `J_API.md`) equal to `0xFFFFFFFF` (= \(2^{32}-1\)).
+- Use that value in `fp_mulmod` / fold exactly as `src/goldilocks.cpp` uses `eps` / `hi_lo` mask.
+- Do not require a `types.h`-style C++ symbol named `EPSILON`; README naming is documentation alias only.
+
+---
+
+## 2. BARRITT_MU unused
+
+**Sources**
+
+- PROPERTIES Gaps: “`BARRITT_MU`: defined equal to `P` and unused (`src/goldilocks.cpp:9–10`); no Barrett algorithm steps beyond the comment.”
+- No numbered property asserts Barrett reduction; Goldilocks reduction is props 5–12 (fold / mulmod as coded).
+
+**Ruling:** **Match C++ as coded** (define-equal-to-`P`, unused; no Barrett path).
+
+**Rationale:** Sources define the constant and leave it unused; there is no Barrett algorithm identity to implement beyond the comment. Inventing Barrett steps would invent math not present in the cited cpp.
+
+**Done for Core**
+
+- May omit `BARRITT_MU` entirely, or expose a synonym equal to `GOLDILOCKS_PRIME` / `P` with no call sites.
+- Do **not** implement Barrett reduction; keep reduction as fold/mulmod per props 5–12 and `src/goldilocks.cpp`.
+
+---
+
+## 3. PMat grading unchecked in `insert` / `validate_grading`
+
+**Sources**
+
+- PROPERTIES Gaps: “PMat per-entry grading vs indices: stated in `pmat.h:3` but not checked in `insert` / `validate_grading`.”
+- Prop 28: header/README narrative says grading `tgt_sig - src_sig = monomial` is enforced; **Gap note** — `insert` does not compare signatures to row/col grades; `validate_grading` always returns `true` (`src/pmat.cpp:19–22`). Cite: `include/pmat.h:3,21–25`.
+
+**Ruling:** **Match C++ as coded** (stub / always-true validate; insert domain checks only).
+
+**Rationale:** The stated grading condition is narrative in the header; the coded surface that tests and callers see is domain checks on `insert` (prop 27) plus a no-op `validate_grading`. Enforcing full grading now would change observable C++ behavior Core is recreating. README/header is not a separate coded math identity here — the stub is the behavior.
+
+**Done for Core**
+
+- `pmat_insert`: fail only on `row ≥ rows`, `col ≥ cols`, or `sign ∉ {1,-1}` (prop 27); do not compare signatures to row/col grades.
+- `validate_grading` (or J equivalent): return success / true unconditionally, matching `src/pmat.cpp:19–22`.
+- Document that prop 28 “stated” grading remains a future Spec upgrade, not Core F1 obligation.
+
+---
+
+## 4. Compose deltas (`a.delta_source + b.delta_target` only vs README/full both signatures)
+
+**Sources**
+
+- PROPERTIES Gaps: “Compose monomial rule vs ‘sum of both signatures’: coded as `a.delta_source` + `b.delta_target` only (`src/pmat.cpp:54–55`), not full addition of both signatures from both factors.”
+- Prop 31 (as coded): on matching `a.col == b.row`: `sign_acc *= a.sign * b.sign`; `monom_acc.delta_source += a.monomial.delta_source`; `monom_acc.delta_target += b.monomial.delta_target`. Cite: `src/pmat.cpp:51–55`.
+- Prop 30 states composition preserves grading (narrative); prop 29 conservation is separately tested on entry monomials.
+
+**Ruling:** **Match C++ as coded** (accumulate `a.delta_source` into result source and `b.delta_target` into result target only).
+
+**Rationale:** Prop 31 already records the coded rule with a precise cite. A “sum of both signatures from both factors” reading is the prose disagreement; Core must reproduce the cpp accumulation, not invent a fuller bilinear sum.
+
+**Done for Core**
+
+- On compose match `a.col == b.row`: multiply signs; add **only** `a.monomial.delta_source` to accumulated `delta_source`; add **only** `b.monomial.delta_target` to accumulated `delta_target`.
+- Do not add `a.delta_target` or `b.delta_source` into the composed monomial unless/until Spec revises prop 31 against a code change.
+
+---
+
+## 5. PHI unused in math cpp
+
+**Sources**
+
+- PROPERTIES Gaps: “PHI usage in UAC/recurrence math: constant present; no consuming identity in the cited math cpp files.”
+- Prop 22: `PHI = 1.618033988749895`. Cite: `include/types.h:21`. “(Sources do not state further mathematical use in the UAC/recurrence core.)”
+
+**Ruling:** **Match C++ as coded** (constant present; unused in field / PMat / spectral / recurrence math paths).
+
+**Rationale:** Value is sourced from `types.h`; no cited math cpp consumes it. README is not supplying a PHI identity to implement — absence of use is the coded fact.
+
+**Done for Core**
+
+- Expose noun `PHI` with the value from `include/types.h:21` / prop 22 (do not invent a different constant).
+- Do not wire PHI into Goldilocks, PMat, spectral governor, or Banach recurrence steps unless a later Spec cites a consuming identity.
+
+---
+
+## Summary table
+
+| # | Gap | Spec ruling | Done for Core (one line) |
+|---|-----|-------------|---------------------------|
+| 1 | EPSILON naming | Match C++ as coded | Named fold noun = `0xFFFFFFFF`; use in mulmod; no required C++ `EPSILON` symbol |
+| 2 | BARRITT_MU unused | Match C++ as coded | Omit or synonym-of-P; no Barrett algorithm |
+| 3 | PMat grading unchecked | Match C++ as coded | Insert domain checks only; validate always true |
+| 4 | Compose deltas | Match C++ as coded | `a.delta_source` + `b.delta_target` only (prop 31) |
+| 5 | PHI unused | Match C++ as coded | Expose constant; no math consumer in Core F1 |
+
+---
+
+## Handoff note
+
+This document is **DRAFT for Core**. It does not modify `PROPERTIES.md`, `j/`, `verify/`, `include/`, `src/`, or Alapeno. Core should treat the five “Done for Core” bullets as the F1 obligation for these gaps; reopen Spec only if a later commit changes the cited cpp behavior.

spec/HCALC_CROSSLINKS.md

@@ -0,0 +1,116 @@
+<!--
+  Copyright (C) 2026 Foundry J / HCALC contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Foundry J → HCALC cross-links (Spec input)
+
+**From:** Foundry J Spec  
+**For:** HCALC Spec / Alloy / Lean (via Hilbert)  
+**Sources:** `/workspace/foundry-j/spec/PROPERTIES.md`, `J_API.md`, `GAP_DECISIONS.md`; Foundry README Sedona Spine / PIRTM.  
+**HCALC abstract (as given):** \( X_{t+1}=\Xi(t,\Lambda_m\cdot C[T_p(X_t)]) \).  
+**Rule:** No invented \(\Lambda_m\) or \(\Xi\) definitions. Gaps flagged below.  
+**Note:** `/workspace/hcalc` had no prior tree when this note was written.
+
+---
+
+## 0. Shape gap (read first)
+
+| | Foundry F1 (cited) | HCALC abstract (given) |
+|--|--------------------|-------------------------|
+| Step | \( x_{t+1}=\Xi_t x_t+\Lambda_t T(x_t)+g_t \) (PROPERTIES **39**) | \( X_{t+1}=\Xi(t,\Lambda_m\cdot C[T_p(X_t)]) \) |
+| \(\Xi\) | Per-step **schedule weights** (length-2 vectors) | Operator/map \(\Xi(t,\cdot)\) — **undefined in Foundry** |
+| \(\Lambda\) / \(\Lambda_m\) | \(\Lambda_t\) schedule weights (same carrier as \(\Xi_t\)) | \(\Lambda_m\) — **no definition in Foundry sources** |
+| \(T\) / \(T_p\) | Nonlinear \(T(x)\) in recurrence; **no \(T_p\)** symbol | Prime-indexed \(T_p\) — **not named in Foundry math** |
+| \(C\) | Not a Foundry recurrence symbol | **Undefined** in Foundry inventory |
+
+**Spec stance:** Treat Foundry as a **candidate instantiation layer** for pieces of the HCALC pipeline (prime index set, contraction tests, Banach step), not as a definition of \(\Lambda_m\) or HCALC-\(\Xi\). Alloy/Lean must not silently equate the two step forms.
+
+---
+
+## 1. Map: what Foundry can instantiate
+
+### \(T_p\) candidates (prime-indexed structure)
+
+| Foundry prop / surface | Role vs \(T_p\) | Cite |
+|------------------------|----------------|------|
+| **23** `P_64` (first 64 primes, length-64 list) | Discrete **prime index set** for any prime-indexed tensor/mask; strongest Foundry hook for “prime-indexed” | `types.h:24–30`; PROPERTIES 23 |
+| `PrimeMask` / `ResonanceWord` (J_API nouns) | Bitmask / packed class∥payload over `P_64` indices — **representation**, not a recursive tensor law | J_API.md nouns |
+| **26–32** PMAT / prime monomials (`Signature`, conservation, compose-as-coded) | Sparse **prime-monomial** linear algebra; possible skeleton for layer ops, **not** a definition of recursive tensor reps | PROPERTIES E; GAP_DECISIONS: grading stub, compose = `a.delta_source+b.delta_target` only |
+| **1–17** Goldilocks \(\mathbb{F}_p\) | Finite-field **carrier** for discrete/algebraic lifts; does **not** by itself give real contraction of \(X_t\) | PROPERTIES A–C |
+| **21** `PIRTM_MAGIC` / linker PIRTM | Bytecode/linker theater (Sedona Spine tooling) — **not** a math definition of \(T_p\) | PROPERTIES 21; README linker |
+
+**Sedona Spine:** README names a 10-layer architecture and Triple-Lock; it does **not** define HCALC \(T_p\), \(\Lambda_m\), or \(C\). Use as architectural context only.
+
+### Contraction / spectral measures (layerwise contraction → converged \(X\))
+
+| Foundry prop | Measure | Cite |
+|--------------|---------|------|
+| **33–34** Gershgorin bound; `contractive ⟺ bound < 1-ε` | A priori row-sum spectral bound | PROPERTIES 33–34 |
+| **35–37** Power iteration + fallback policy | Dominant-modulus check; recheck when Gershgorin tight | PROPERTIES 35–37 |
+| **38** Contractive / expansive test matrices | Concrete witnesses (quoted in PROPERTIES; do not alter) | PROPERTIES 38 |
+| **25** Tier ε: T1→0.10, T2→0.05, T3→0.02, T4→0.01 | Contraction **margin** schedule | PROPERTIES 25 |
+| **39–46** Banach recurrence, \(q_t\), soft project, residual | Foundry **evolution** + projection when \(q>1-\varepsilon\) | PROPERTIES G |
+| **55** Guardian spectral legality | Reject if `spectral_radius >= 1` or non-finite next state | PROPERTIES 55 |
+
+---
+
+## 2. Invariants demanded before calling HCALC “coherent”
+
+Demand these as **explicit** Spec/Alloy/Lean obligations (Foundry-backed where cited; HCALC-native where flagged):
+
+1. **Step-form declared** — Either adopt Foundry **39** as an instance, or define HCALC \(\Xi(t,\cdot)\) / \(\Lambda_m\) / \(C\) / \(T_p\) separately. **Do not mix symbols without a bridge lemma.** (Gap: HCALC defs missing.)
+2. **Prime index honesty** — If “prime-indexed” means Foundry, \(T_p\) (or its mask) is valued on **`P_64` (prop 23)** or a stated extension; no silent infinite prime stream.
+3. **Contraction predicate** — Layer/Jacobian (or stated linearization) satisfies Foundry-style **34/36**: modulus bound \(< 1-\varepsilon\) for a declared \(\varepsilon\) (tier **25** or other cited constant).
+4. **q-budget / soft projection** — If Foundry schedules are used: **40/42/43** — \(q=\|\Xi\|+\|\Lambda\|\cdot\|T\|\); if \(q>1-\varepsilon\), scale as coded.
+5. **Convergence witness** — Residual **46** (or Lean equivalent) below a declared tolerance; unique fixed-point only where Banach hypotheses **41** are discharged (not assumed from narrative alone).
+6. **PMAT conservation (if PMAT used)** — **29** product/sum of entry monomials equals accumulated signature sums (test vector cited in PROPERTIES).
+7. **Gap rulings respected** — Match C++ as coded per `GAP_DECISIONS.md` (compose deltas, grading stub, EPSILON literal, unused BARRITT_MU/PHI) until HCALC Spec overrides **in writing**.
+8. **No invented \(\Lambda_m\)** — Alloy/Lean may leave \(\Lambda_m\), HCALC-\(\Xi\), \(C\), \(T_p\) as **opaque symbols** or axioms with `sorry`/uninterpreted ops until HCALC Spec defines them.
+
+---
+
+## 3. Shortlist for Alloy asserts + Lean axiom candidates
+
+### Alloy-oriented asserts (finite, checkable)
+
+| ID | Assert (informal) | Foundry anchor |
+|----|-------------------|----------------|
+| A1 | `#P_64 = 64` and elements are the listed first-64 primes | Prop **23** |
+| A2 | `contractive(J,ε) iff gershgorin(J) < 1-ε` (and optional power-iter branch **37**) | **33–37** |
+| A3 | Soft-project: if `q > 1-ε` then scaled weights used in the step | **43** |
+| A4 | Recurrence carrier: next state is affine Foundry form **only if** instance = Foundry | **39** |
+| A5 | PMAT conservation on insert-set | **29** |
+| A6 | Guardian: reject when spectral radius ≥ 1 or non-finite | **55** |
+| A7 | **Gap stub:** `Λm`, HCALC-`Ξ`, `C`, `T_p` are unconstrained until defined — assert **presence of a definition record**, not a formula | (no Foundry cite) |
+
+### Lean axiom / definition candidates (prefer defs where Foundry is concrete)
+
+| ID | Candidate | Kind | Note |
+|----|-----------|------|------|
+| L1 | `P64 : Fin 64 → ℕ` with the PROPERTIES **23** list | **definition** (data) | No axiom needed if listed |
+| L2 | `gershgorinBound`, `contractiveG` | **definition** + theorem | From **33–34** |
+| L3 | `FoundryStep Ξ Λ T g x` | **definition** | Exact **39**; ≠ HCALC abstract |
+| L4 | `qEstimate` / `softProject` | **definition** | **42–43** as coded |
+| L5 | Banach unique fixed point under `q < 1-ε` | **theorem** (or axiom until proof) | Narrative **41** — prove or mark unfinished |
+| L6 | `Λm`, `HCALC.Ξ`, `C`, `Tp` | **axioms / uninterpreted** | **Gaps — do not invent** |
+| L7 | Bridge `HCALCStep = FoundryStep` (or embedding) | **axiom or theorem** | Only after HCALC Spec defines left-hand side |
+
+### Explicit gaps (do not invent)
+
+- \(\Lambda_m\) — no Foundry definition (Foundry has \(\Lambda_t\) weights only).
+- HCALC \(\Xi(t,\cdot)\) — not Foundry \(\Xi_t\) vectors.
+- \(C[\cdot]\) — undefined in Foundry inventory.
+- \(T_p\) — no Foundry symbol; closest are `P_64` + PMAT + \(T(x)\).
+- Recursive tensor representation law — **absent** from Foundry PROPERTIES.
+- `/workspace/hcalc` content beyond this note — none at write time.
+
+---
+
+## 4. Suggested handoff order
+
+1. HCALC Spec: define or explicitly leave open \(\Lambda_m\), \(\Xi\), \(C\), \(T_p\).  
+2. Alloy: A1–A6 on Foundry instance; A7 gate on open symbols.  
+3. Lean: L1–L4 defs first; L6 axioms for gaps; L5/L7 only with proof or labeled unfinished.  
+4. Foundry Core/Verify: keep prop **16** FAIL and coverage matrix in view when claiming Goldilocks lifts into HCALC.
+

spec/HCALC_PRODUCTION_REVIEW.md

@@ -0,0 +1,66 @@
+<!--
+  Copyright (C) 2026 Foundry J contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Foundry J Spec — HCALC PRODUCTION.md review (pass 3 / InstanceBridge)
+
+**Reviewer:** Foundry J Spec  
+**Date:** 2026-10-07 (PT)  
+**Target:** `/workspace/hcalc/spec/PRODUCTION.md` @ `f5a08da`  
+**Focus:** §6 ShapeMap `InstanceBridge` vs REJECT identity; Core path `/workspace/hcalc/j/`
+
+---
+
+## Verdict (short)
+
+| Item | Verdict |
+|------|---------|
+| §6 `InstanceBridge` (NOT rfl / NOT Foundry39≡nested) | **ACCEPT** |
+| Explicit param table \(T:=C\circ T_p\), \(\Lambda:=\Lambda_m\mathbf{1}\), \(\Xi:=\xi_t\) without symbol identity | **ACCEPT** |
+| Option B: implement `hcalc_step` only; `toFoundryStep` diagnostic cite-only | **ACCEPT** |
+| soft_project remains Foundry-coded **42–43**; `C` is Spec wiring that *uses* the scale idea | **ACCEPT** (wording in §6) |
+| Core path `/workspace/hcalc/j/` + verb list matching `HCALC_API_DRAFT.md` | **ACCEPT** |
+| GAP_DECISIONS | **No conflict** |
+| Silent identity Foundry39 ≡ nested | Still **REJECT** — PRODUCTION agrees |
+
+**Overall:** **ACCEPT** PRODUCTION @ `f5a08da` for ShapeMap / implement path. Non-blocking nits below.
+
+---
+
+## §6 ShapeMap detail
+
+PRODUCTION now states clearly:
+
+- `toFoundryStep` = \(\xi_t\cdot x + \Lambda_m(C\circ T_p)(x)+g_t\) under InstanceBridge params.  
+- `hcalcStep` = \(\xi_t\cdot(\Lambda_m\cdot C(T_p(x)))+g_t\).  
+- These differ (\(\xi_t\cdot x\) only on Foundry side).  
+- L7 = structure + theorems about the table, **not** `FoundryStep = hcalcStep`.
+
+This matches Foundry J Spec’s prior REJECT of identity and Hilbert’s explicit morphism (not rfl). **ACCEPT.**
+
+---
+
+## `/workspace/hcalc/j/` implement path
+
+| Check | Result |
+|-------|--------|
+| Path authoritative under hcalc | **ACCEPT** |
+| Verbs: `tp_from_p64`, `c_wrap`, `lam_m_from_bound`, `hcalc_xi_apply`, `hcalc_step`, `hcalc_run` | **ACCEPT** (names match draft) |
+| Do not equate `hcalc_step` / `rec_step` | **ACCEPT** |
+| Implementation status | **Scaffold only** (`j/README.md`); bodies still Core’s job — not a Spec reject |
+
+---
+
+## Non-blocking nits (optional Spec polish)
+
+1. **§3 vs §6 soft_project wording:** §3 formula still scales **state** \(x\); Foundry **43** scales **schedules** \(\Xi,\Lambda\). §6 correctly calls that Spec wiring. One footnote in §3: “`softProjectScale` factor shared; Foundry `soft_project` API remains schedule-scaling when called as Foundry.”  
+2. **Alloy checklist line** still says “FoundryAdditive” — align naming to `InstanceBridge` / `toFoundryStep` vs `hcalcStep`.  
+3. **§8 Hyp under Uniform:** phrase “when using InstanceBridge” for nested Lip — prefer “when iterating `hcalcStep` (Option B)”; `toFoundryStep` has an extra \(\xi_t\cdot x\) term.  
+4. **α law / ℓ∞ residual:** still Spec-def (not Foundry source-claim) — OK if provenance stays Spec-owned.
+
+---
+
+## Summary for Hilbert / HCALC Spec
+
+**ACCEPT** InstanceBridge ShapeMap and `/workspace/hcalc/j/` Core path. Identity REJECT stands and is honored. Ready for Alloy/Lean/Core to implement Option B without further Foundry J Spec gate — unless they want the §3 soft_project footnote.

spec/J_API.md

@@ -0,0 +1,129 @@
+# Foundry F1 — Pure-J Core API Surface
+
+Mapping of the C++ mathematical surface to J Core verbs/nouns.
+**No implementation.** Names, ranks, and domains only.
+Preferred license for derivative pure-J work: **AGPL-3.0**.
+
+Convention: J ranks — `0` atom, `1` list/vector, `2` table/matrix, `3` rank-3. Domains name the mathematical carrier.
+
+---
+
+## Nouns (data carriers)
+
+| Noun | Rank | Domain | Maps from |
+|------|------|--------|-----------|
+| `Fp` | 0 | atom `u64` with \(0 \le v < p\) | `Goldilocks::Elem` |
+| `FpVec` | 1 | list of `Fp` | batch Elem arrays |
+| `Signature` | 1 | length-2 integer list `(delta_source; delta_target)` | `pmc::Signature` |
+| `PMatEntry` | 1 | boxed/record: `sign (±1)`, `Signature`, `row`, `col` | `pmc::PMatEntry` |
+| `PMat` | 1–2 | sparse list of `PMatEntry` plus shape `(rows; cols)` | `pmc::PMat` |
+| `Jacobian` | 2 | real matrix \( n\times n \) | `vector<vector<double>>` spectral input |
+| `State` | 1 | real vector \( x_t \) | recurrence state |
+| `Weights` | 1 | length-2 (or dim) real list for Ξ / Λ schedule row | `xi_schedule_[t]`, `lambda_schedule_[t]` |
+| `StepInfo` | 0–1 | record: `step`, `q`, `epsilon`, `n_xi`, `n_lam`, `projected`, `residual` | `pmc::StepInfo` |
+| `SpectralResult` | 0–1 | record: `spectral_radius`, `contractive`, `gershgorin_bound`, `power_iter_bound`, `used_power_iteration` | `SpectralGovernor::Result` |
+| `AceCert` | 0–1 | record: `lipschitz_upper`, `safety_margin`, `tail_bound`, `certified` | `pmc::AceCertificate` |
+| `Tier` | 0 | enum atom T1..T4 | `pmc::Tier` |
+| `GatePolicy` | 0 | enum: PassThrough / Suppress / Hold / Attenuate | `pmc::GatePolicy` |
+| `P64` | 1 | length-64 list of first primes | `pmc::P_64` |
+| `PrimeMask` | 0 | `u64` bitmask over `P64` indices | `pmc::PrimeMask` |
+| `ResonanceWord` | 0 | `u64` packed class∥payload | `pmc::ResonanceWord` |
+
+### Named constant nouns (must match PROPERTIES.md)
+
+| Noun | Rank | Value source |
+|------|------|--------------|
+| `GOLDILOCKS_PRIME` / `p` | 0 | `0xFFFFFFFF00000001` = 18446744069414584321 |
+| `EPSILON_FOLD` | 0 | `0xFFFFFFFF` = \(2^{32}-1\) (fold; README name `EPSILON`) |
+| `K_MAX` | 0 | 133144 |
+| `MAX_DRIFT` | 0 | 300000000000000000 |
+| `PIRTM_MAGIC` | 0 | `0x7F504952` |
+| `PHI` | 0 | 1.618033988749895 |
+| `tier_epsilon` | 0←0 | T1:0.10 T2:0.05 T3:0.02 T4:0.01 |
+
+---
+
+## Verbs — Goldilocks field
+
+| Verb | Rank | Domain → range | Meaning |
+|------|------|----------------|---------|
+| `fp_reduce` | 0→0 | `u64` → `Fp` | conditional \( x-p \) if \( x\ge p \) |
+| `fp_add` | 0 0→0 | `Fp×Fp` → `Fp` | \( (a+b)\bmod p \) |
+| `fp_sub` | 0 0→0 | `Fp×Fp` → `Fp` | \( (a-b)\bmod p \) |
+| `fp_mul` | 0 0→0 | `Fp×Fp` → `Fp` | mulmod via reduction identity |
+| `fp_mulmod` | 0 0→0 | `u64×u64` → `u64` | 128-bit product + fold \( \mathrm{lo}+\mathrm{hi\_lo}\cdot\varepsilon-\mathrm{hi\_hi} \) |
+| `fp_pow` | 0 0→0 | `Fp×u64` → `Fp` | square-and-multiply |
+| `fp_inv` | 0→0 | `Fp` → `Fp` | \( a^{p-2} \) (Fermat) |
+| `fp_add_batch` | 1 1→1 | `FpVec×FpVec` → `FpVec` | elementwise add |
+| `fp_mul_batch` | 1 1→1 | `FpVec×FpVec` → `FpVec` | elementwise mul |
+
+---
+
+## Verbs — PMAT
+
+| Verb | Rank | Domain → range | Meaning |
+|------|------|----------------|---------|
+| `pmat_new` | 0 0→1 | `(rows;cols)` → empty `PMat` | allocate shape |
+| `pmat_insert` | 1 0 0 0 1→1 | PMat,row,col,sign,Signature → PMat\|fail | domain checks ±1 and bounds |
+| `pmat_validate_grading` | 1→0 | `PMat` → boolean | global grading (stated identity) |
+| `pmat_conservation` | 1→1 | `PMat` → `Signature` | Σ monomials |
+| `pmat_compose` | 1 1→1 | `PMat×PMat` → `PMat` | sign multiply + monomial accumulate |
+| `pmat_frobenius` | 1→0 | `PMat` → real | \( \sqrt{\#entries} \) |
+
+---
+
+## Verbs — Spectral governor
+
+| Verb | Rank | Domain → range | Meaning |
+|------|------|----------------|---------|
+| `gershgorin_bound` | 2→0 | `Jacobian` → real | max disk \( |J_{ii}|+\sum_{j\neq i}|J_{ij}| \) |
+| `gershgorin_check` | 2 0→1 | Jacobian,ε → `SpectralResult` | contractive iff bound \( <1-\varepsilon \) |
+| `power_iteration` | 2 0 0→0 | Jacobian,max_iters,tol → real | dominant \|eigenvalue\| |
+| `power_iteration_check` | 2 0 0→1 | Jacobian,ε,max_iters → `SpectralResult` | same contractive predicate |
+| `spectral_analyze` | 2 0→1 | Jacobian,ε → `SpectralResult` | Gershgorin then optional power iter |
+
+---
+
+## Verbs — Banach recurrence
+
+| Verb | Rank | Domain → range | Meaning |
+|------|------|----------------|---------|
+| `tier_eps` | 0→0 | `Tier` → real | margin ε |
+| `synth_weights` | 0 0 1→2 | max_steps,Tier,profile,[primes] → (Ξ schedule; Λ schedule) | Uniform/Harmonic/LogDecay; 0.7/0.3 of \( q^\star \) |
+| `soft_project` | 1 1 0 0→1 1 | Ξ,Λ,q,ε → scaled Ξ,Λ | scale by \( (1-\varepsilon)/q \) if \( q>1-\varepsilon \) |
+| `rec_step` | 1 1 1 1→1 1 | x, Ξ, Λ, g ; T ; p_op → (x_next; StepInfo) | \( x'=\Xi x+\Lambda T(x)+g \) then project |
+| `rec_run` | 1 0→2 | x0, config, T, p_op → StepInfo history | until residual < tol or max_steps |
+| `residual_l2` | 1 1→0 | x_next, x_t → real | \( \|x'-x\|_2 \) |
+| `q_estimate` | 1 1 1 1→0 | Ξ,Λ,x,Tx → real | \( \|\Xi\|_\infty+\|\Lambda\|_\infty\cdot\|T\| \) (coded max-abs form) |
+
+Transform `T` and projector `p_op` are rank-1→1 function nouns (hooks), not fixed verbs.
+
+---
+
+## Verbs — Emission / CSL / certify (math-adjacent)
+
+| Verb | Rank | Domain → range | Meaning |
+|------|------|----------------|---------|
+| `emit_apply` | 1 1 0 0→1 | out,prev,q,policy×ε → out' | PassThrough/Suppress/Hold/Attenuate |
+| `csl_neutrality` | 1 1 0→0 | x,Tx,ε → verdict | pairwise Lip-style bound |
+| `csl_beneficence` | 1 1 0 0→0 | x,Tx,residual,ε → verdict | norm & residual growth |
+| `csl_commutation` | 1 0→0 | x; T; filter; ε → verdict | filter∘T ≈ T∘filter |
+| `ace_safety_margin` | 0 0→0 | max_q,ε → real | \( (1-\varepsilon)-\max_q \) |
+| `ace_tail_bound` | 0 0→0 | tail_norm,max_q → real | \( \mathrm{tail}/(1-\max_q) \) or ∞ |
+| `ace_certify` | 1 0→1 | StepInfo list, delta → `AceCert` | margin ≥ delta |
+
+---
+
+## Coverage map (C++ → J)
+
+| C++ module | J surface |
+|------------|-----------|
+| `goldilocks.h/cpp` | `fp_*` verbs + `Fp` / `FpVec` |
+| `pmat.h/cpp` | `pmat_*` + `Signature` / `PMat` |
+| `spectral.h/cpp` | `gershgorin_*` / `power_*` / `spectral_analyze` |
+| `recurrence.h/cpp` | `rec_*` / `synth_weights` / `soft_project` / `q_estimate` |
+| `types.h` constants | constant nouns + `tier_eps` |
+| `gate.h/cpp` (math) | `emit_apply` / `csl_*` |
+| `certify.h/cpp` | `ace_*` |
+
+Non-math orchestration (SHA-256 WORM bytes, linker PIRTM, audit JSON) is out of this pure-J math Core inventory except where PROPERTIES.md cites seal-chain / consensus narrative for completeness.

spec/LICENSE_NOTE.txt

@@ -0,0 +1,3 @@
+AGPL-3.0 preferred for pure-J recreation inventory under this directory.
+Sources under /workspace/foundry-j do not ship a LICENSE file; this note records inventory policy only.
+Alapeno (/workspace/alapeno) is out of scope.

spec/PROPERTIES.md

@@ -0,0 +1,282 @@
+# Foundry F1 — Pure-J Recreation Property Inventory
+
+Extracted from cpp-foundry sources under `/workspace/foundry-j/`.
+Every claim below is required to hold in a pure-J recreation of the mathematical surface.
+Citations are `file:line` or README section. **No invented numeric constants.**
+
+Preferred license for derivative pure-J work: **AGPL-3.0** (sources do not ship a LICENSE file; this preference is inventory policy only).
+
+---
+
+## A. Goldilocks prime and field carrier
+
+1. **Goldilocks prime (decimal).**  
+   \( p = 2^{64} - 2^{32} + 1 = 18446744069414584321 \).  
+   Cite: README.md § "Goldilocks Field F_p" (lines 209–210).
+
+2. **Goldilocks prime (hex / named constant).**  
+   `GOLDILOCKS_PRIME = 0xFFFFFFFF00000001ULL`, meaning \( 2^{64} - 2^{32} + 1 \).  
+   Cite: `include/types.h:17`; README.md § "Key Constants" (line 315); `include/goldilocks.h:2,12`.
+
+3. **Field elements are u64 reduced mod p.**  
+   Carrier is unsigned 64-bit values always reduced modulo \( p \).  
+   Cite: README.md § "Goldilocks Field F_p" (line 212); `include/goldilocks.h:14–18`.
+
+4. **Elem construction reduces.**  
+   `Elem(x)` stores `reduce(x)`.  
+   Cite: `include/goldilocks.h:18`.
+
+---
+
+## B. Reduction identity and mulmod
+
+5. **Congruence \( 2^{64} \equiv 2^{32} - 1 \pmod{p} \).**  
+   Cite: README.md § "Goldilocks Field F_p" (line 214); `src/goldilocks.cpp:23`.
+
+6. **Fold constant EPSILON.**  
+   README names `EPSILON = 0xFFFFFFFF` as \( 2^{32} - 1 \) (Goldilocks fold constant). Implementation uses the same literal as `eps` / `hi_lo` mask.  
+   Cite: README.md § "Key Constants" (line 320); `src/goldilocks.cpp:27,31`.
+
+7. **128-bit product split.**  
+   For \( a \cdot b \), form `__uint128_t product`, then `lo = product`, `hi = product >> 64`.  
+   Cite: README.md (line 213); `src/goldilocks.cpp:20–25`.
+
+8. **hi split into 32-bit halves.**  
+   `hi_lo = hi & 0xFFFFFFFF`, `hi_hi = hi >> 32`.  
+   Cite: `src/goldilocks.cpp:27–28`.
+
+9. **Reduction identity (fold).**  
+   \( x \equiv \mathrm{lo} + \mathrm{hi\_lo}\cdot(2^{32}-1) - \mathrm{hi\_hi} \pmod{p} \).  
+   Cite: README.md § "Goldilocks Field F_p" (line 216); implemented as `folded = lo + hi_lo * eps` then subtract `hi_hi` with underflow handling (`src/goldilocks.cpp:30–41`).
+
+10. **Underflow handling on fold.**  
+    If `folded >= hi_hi` then `reduced = folded - hi_hi`, else `reduced = folded + P - hi_hi`.  
+    Cite: `src/goldilocks.cpp:36–41`.
+
+11. **Final conditional reduction after fold.**  
+    If `reduced >= P` then `reduced -= P`; result is `uint64_t`.  
+    Cite: `src/goldilocks.cpp:43–48`.
+
+12. **Single-limb reduce.**  
+    For \( x < 2^{64} \): `reduce(x) = (x >= P) ? x - P : x`.  
+    Cite: `src/goldilocks.cpp:12–16`; `include/goldilocks.h:35`.
+
+---
+
+## C. Field operations
+
+13. **Addition mod p.**  
+    \( r = a.v + b.v \); if \( r \ge P \) then \( r -= P \). Result is in \( \mathbb{F}_p \).  
+    Cite: `src/goldilocks.cpp:51–55`; asserted `100+200=300` in `src/test.cpp:33–39`.
+
+14. **Subtraction mod p.**  
+    Unsigned difference with conditional add of \( P \) on underflow (mask from high bit).  
+    Cite: `src/goldilocks.cpp:57–62`; asserted `100-50=50` in `src/test.cpp:60–66`.
+
+15. **Multiplication via mulmod.**  
+    `mul(a,b) = Elem(mulmod(a.v, b.v))`.  
+    Cite: `src/goldilocks.cpp:64–66`; asserted `7*6=42` in `src/test.cpp:42–48`.
+
+16. **Fermat inverse.**  
+    \( a^{-1} = a^{p-2} \pmod{p} \) via `inv(a) = pow(a, P-2)`.  
+    Cite: `include/goldilocks.h:27`; `src/goldilocks.cpp:68–70`; README test legend (line 403); asserted `a * inv(a) = 1` for `a=42` in `src/test.cpp:51–57`.
+
+17. **Binary exponentiation.**  
+    `pow(a,e)`: square-and-multiply from `result=1`, `base=a`.  
+    Cite: `src/goldilocks.cpp:73–81`; `include/goldilocks.h:28`.
+
+18. **Batch add/mul.**  
+    Elementwise `add` / `mul` over length-`n` arrays.  
+    Cite: `include/goldilocks.h:31–32`; `src/goldilocks.cpp:84–96`.
+
+---
+
+## D. Named constants (non-field)
+
+19. **K_MAX.**  
+    `K_MAX = 133144` (README: max W8A8 accumulation).  
+    Cite: `include/types.h:18`; README.md § "Key Constants" (line 316).
+
+20. **MAX_DRIFT.**  
+    `MAX_DRIFT = 300000000000000000ULL` (README: \( 3\times 10^{17} \), “0.3Ξ drift bound” / “0.3Ξ in wei”).  
+    Cite: `include/types.h:19`; README.md § "Key Constants" (line 317).
+
+21. **PIRTM_MAGIC.**  
+    `PIRTM_MAGIC = 0x7F504952` (README: `\x7FPIR` bytecode magic).  
+    Cite: `include/types.h:20`; README.md § "Key Constants" (line 318); linker test bytes `src/test.cpp:371–372`.
+
+22. **PHI.**  
+    `PHI = 1.618033988749895`.  
+    Cite: `include/types.h:21`. (Sources do not state further mathematical use in the UAC/recurrence core.)
+
+23. **P_64 — first 64 primes.**  
+    Array of length 64:  
+    `2,3,5,7,11,13,17,19,23,29,31,37,41,43,47,53,59,61,67,71,73,79,83,89,97,101,103,107,109,113,127,131,137,139,149,151,157,163,167,173,179,181,191,193,197,199,211,223,227,229,233,239,241,251,257,263,269,271,277,281,283,293,307,311`.  
+    Cite: `include/types.h:24–30`; README.md § "Key Constants" (line 319).
+
+24. **GENESIS_HASH_SIZE.**  
+    `GENESIS_HASH_SIZE = 32`.  
+    Cite: `include/types.h:22`.
+
+25. **Tier epsilons (contraction margins).**  
+    T1→0.10, T2→0.05, T3→0.02, T4→0.01; default fallback 0.10.  
+    Cite: `include/types.h:34–48`.
+
+---
+
+## E. PMAT / prime monomial facts
+
+26. **PMat entry shape.**  
+    Sparse entry is `(sign, monomial, row, col)` with `sign ∈ {±1}` and `Signature = (delta_source, delta_target)`.  
+    Cite: `include/pmat.h:10–15`; `include/types.h:103–112`.
+
+27. **Insert domain checks.**  
+    Insert fails if `row ≥ rows` or `col ≥ cols`, or if `sign ∉ {1,-1}`; else appends entry.  
+    Cite: `src/pmat.cpp:11–16`; asserted in `src/test.cpp:71–77`.
+
+28. **Grading condition (stated).**  
+    Header/README narrative: grading condition `tgt_sig - src_sig = monomial` is enforced on insertion / validated globally.  
+    Cite: `include/pmat.h:3,21–25`.  
+    **Gap note:** `insert` does not compare signatures to row/col grades; `validate_grading` always returns `true` (`src/pmat.cpp:19–22`). J must decide whether to enforce the stated condition or mirror the current C++ stub.
+
+29. **Conservation theorem.**  
+    Product (componentwise sum) of all entry monomials equals accumulated `(Σ delta_source, Σ delta_target)`.  
+    Cite: `include/pmat.h:27–28`; `src/pmat.cpp:25–33`; asserted sums `(6,8)` for monomials `{3,5}+{1,2}+{2,1}` in `src/test.cpp:80–89`.
+
+30. **Composition preserves grading (stated).**  
+    Compose multiplies signs and accumulates monomials along matching mid-indices; result size `(rows_, other.cols_)`.  
+    Cite: `include/pmat.h:30–31`; `src/pmat.cpp:36–66`.
+
+31. **Compose monomial accumulation rule (as coded).**  
+    On matching `a.col == b.row`: `sign_acc *= a.sign * b.sign`; `monom_acc.delta_source += a.monomial.delta_source`; `monom_acc.delta_target += b.monomial.delta_target`.  
+    Cite: `src/pmat.cpp:51–55`.
+
+32. **Frobenius norm of PMat.**  
+    Each entry has magnitude 1; \( \|M\|_F = \sqrt{\#\mathrm{entries}} \).  
+    Cite: `include/pmat.h:33–34`; `src/pmat.cpp:69–74`.
+
+---
+
+## F. Spectral governor (Gershgorin / contractive)
+
+33. **Gershgorin disk bound.**  
+    For each row \( i \): radius \( = \sum_{j\neq i}|J_{ij}| \); disk max \( = |J_{ii}| + \mathrm{radius} \); bound = max over rows.  
+    Cite: `src/spectral.cpp:10–24`; `include/spectral.h:36–37`.
+
+34. **Contractive test (Gershgorin).**  
+    `contractive ⟺ bound < (1.0 - epsilon)`.  
+    Cite: `src/spectral.cpp:27–36`; `include/spectral.h:17–18`.
+
+35. **Power iteration (Rayleigh).**  
+    Iterate \( v \leftarrow Jv/\|Jv\| \); eigenvalue ≈ \( v^\top Jv \); return absolute value; default tolerance `1e-12`, default `max_iters=100`.  
+    Cite: `include/spectral.h:29–30,40–41`; `src/spectral.cpp:39–86`.
+
+36. **Contractive test (power iteration).**  
+    Same predicate: dominant eigenvalue modulus \( < 1 - \epsilon \).  
+    Cite: `src/spectral.cpp:88–98`.
+
+37. **Analyze fallback policy.**  
+    Try Gershgorin first; if contractive but `gershgorin_bound > (1-epsilon)*0.95`, recheck with power iteration.  
+    Cite: `src/spectral.cpp:101–111`; `include/spectral.h:32–34`.
+
+38. **Tested contractive / expansive examples.**  
+    \( J=\begin{bmatrix}0.2&0.1\\0.05&0.15\end{bmatrix} \) with \( \epsilon=0.1 \) is contractive;  
+    \( J=\begin{bmatrix}0.9&0.3\\0.3&0.95\end{bmatrix} \) with \( \epsilon=0.1 \) is not.  
+    Cite: `src/test.cpp:94–113`.
+
+---
+
+## G. Banach recurrence
+
+39. **Recurrence equation.**  
+    \( x_{t+1} = \Xi_t \cdot x_t + \Lambda_t \cdot T(x_t) + g_t \).  
+    Cite: README.md § "Banach Contraction Mapping" (lines 226–232); `include/recurrence.h:3`; `src/recurrence.cpp:105–110`.
+
+40. **Contraction condition.**  
+    \( q_t = \|\Xi_t\| + \|\Lambda_t\| \cdot \|T\| < 1 - \varepsilon \).  
+    Cite: README.md (lines 234–235, 280); `include/recurrence.h:4`; `include/types.h:119`.
+
+41. **Unique fixed-point guarantee (narrative).**  
+    Strict Banach contraction ⇒ convergence to unique fixed point; spectral governor verifies a priori.  
+    Cite: README.md § "The Core Guarantee" (lines 282–284).
+
+42. **q estimate in step (as coded).**  
+    \( n_\Xi, n_\Lambda \) = max-abs of schedule vectors (length 2); \( n_T \) = max-abs of \( T(x) \) scaled by max-abs of \( x \) when \( \|x\|_\infty > 10^{-15} \); \( q = n_\Xi + n_\Lambda \cdot n_T \).  
+    Cite: `src/recurrence.cpp:66–87`.
+
+43. **Soft projection.**  
+    If \( q > 1 - \mathrm{tier\_epsilon} \), scale Ξ and Λ by \( (1-\varepsilon)/q \).  
+    Cite: `include/recurrence.h:60–63`; `src/recurrence.cpp:46–55,89–102`.
+
+44. **Weight budget split.**  
+    `q_star = 1 - tier_epsilon(tier)`; `xi_val = q_star * factor * 0.7`; `lam_val = q_star * factor * 0.3`; Uniform/Harmonic/LogDecay factors as coded.  
+    Cite: `src/recurrence.cpp:21–42`.
+
+45. **Projector.**  
+    After affine update, apply `p_op` (example: clip to \([-1,1]\)).  
+    Cite: `include/recurrence.h:15–16`; `src/recurrence.cpp:113–114`; test projector `src/test.cpp:133–135`.
+
+46. **Residual.**  
+    \( \mathrm{residual} = \|x_{next} - x_t\|_2 \). Convergence when residual \( < \) `convergence_tol`.  
+    Cite: `src/recurrence.cpp:116–122,159–161`; test tol `1e-6` in `src/test.cpp:125,139`.
+
+47. **WORM / seal chain invariant (system-level).**  
+    \( \forall k>0:\ \mathrm{hash}(\mathrm{seal}_{k-1}) = \mathrm{seal}_k.\mathrm{prev\_hash} \) (README); Triple-Lock seals chain Guardian→Examiner→Publisher.  
+    Cite: README.md Layer 8 (line 130), Quick Reference (line 525); `src/test.cpp:300–324`.
+
+---
+
+## H. Emission / CSL / certification math (adjacent to contraction)
+
+48. **Emission Suppress.**  
+    If \( q \ge 1-\varepsilon \), emit zeros; else pass output.  
+    Cite: `include/types.h:63`; `src/gate.cpp:21–25`; `src/test.cpp:145–150`.
+
+49. **Emission Attenuate scale.**  
+    Scale by \( \max(0,\ 1-\varepsilon-q) \).  
+    Cite: `include/types.h:65`; `src/gate.cpp:34–40`.
+
+50. **CSL neutrality.**  
+    Pairwise: if \( |x_i-x_j|>10^{-15} \) and \( |T_i-T_j|/|x_i-x_j| > 1+\varepsilon \), fail neutrality.  
+    Cite: `src/gate.cpp:50–62`; `include/gate.h:34–37`.
+
+51. **CSL beneficence.**  
+    \( \|T(x)\|_2 \le (1+\varepsilon)\|x\|_2 \) and residual \( \le (1+\varepsilon)\|x\|_2 \).  
+    Cite: `src/gate.cpp:65–86`; `include/gate.h:39–42`.
+
+52. **CSL commutation.**  
+    \( \|\mathrm{filter}(T(x)) - T(\mathrm{filter}(x))\|_\infty \le \varepsilon \) (componentwise abs ≤ ε).  
+    Cite: `src/gate.cpp:89–104`; `include/gate.h:44–48`.
+
+53. **AceCertificate safety margin.**  
+    `safety_margin = (1 - epsilon) - max_q`; certified iff `margin >= delta`.  
+    Cite: `include/types.h:133–136`; `src/certify.cpp:44–45,35`.
+
+54. **AceCertificate tail bound.**  
+    If `max_q >= 1` then \( +\infty \); else `tail_norm / (1 - max_q)`.  
+    Cite: `include/types.h:135`; `src/certify.cpp:48–50`.
+
+55. **Guardian spectral legality.**  
+    Reject if `spectral_radius >= 1.0` or non-finite next state; reject status `"PROVISIONAL"`.  
+    Cite: `src/gate.cpp:159–177`; `src/test.cpp:193–201,276–284`.
+
+56. **Consensus / false-positive bound (narrative).**  
+    Every claim requires all Triple-Lock parties; \( P(\mathrm{false\ positive}) \le 2^{-256} \).  
+    Cite: README.md Triple-Lock (lines 272–273), Implications (line 451).
+
+---
+
+## Gaps (sources silent — do not invent)
+
+- **Named C++ identifier `EPSILON`:** named only in README Key Constants; code uses literal `0xFFFFFFFFULL` in mulmod, not a `types.h` symbol.
+- **`BARRITT_MU`:** defined equal to `P` and unused (`src/goldilocks.cpp:9–10`); no Barrett algorithm steps beyond the comment.
+- **PMat per-entry grading vs indices:** stated in `pmat.h:3` but not checked in `insert` / `validate_grading`.
+- **Compose monomial rule vs “sum of both signatures”:** coded as `a.delta_source` + `b.delta_target` only (`src/pmat.cpp:54–55`), not full addition of both signatures from both factors.
+- **PHI usage** in UAC/recurrence math: constant present; no consuming identity in the cited math cpp files.
+- **Alapeno:** out of scope; left untouched (`/workspace/alapeno`).
+
+---
+
+## Count
+
+**Numbered properties: 56**

verify/INVENTORY.md

@@ -0,0 +1,55 @@
+<!--
+  Copyright (C) 2026 Foundry J contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Foundry J Verify — Test Inventory
+
+Sources: `src/test.cpp`, `spec/PROPERTIES.md`, Core `j/foundry.ijs`.
+Detail map: `PROPERTY_MAP.md` (all 56 properties).
+
+## Named mathematical tests (baseline)
+
+| # | Test | Family | Property # | Core verbs | Measured |
+|---|------|--------|------------|------------|----------|
+| 1 | `goldilocks_add` | goldilocks | **13** | `fp_add` | PASS |
+| 2 | `goldilocks_mul` | goldilocks | **15** | `fp_mul` | PASS |
+| 3 | `goldilocks_inv` | goldilocks | **16** | `fp_inv`/`fp_mul` | PASS |
+| 4 | `goldilocks_sub` | goldilocks | **14** | `fp_sub` | PASS |
+| 5 | `pmat_insert` | pmat | **27** | `pmat_new`/`pmat_insert`/`pmat_entries` | PASS |
+| 6 | `pmat_conservation` | pmat | **29** | `pmat_conservation` | PASS |
+| 7 | `spectral_contractive` | spectral | **38** | `spectral_analyze` | PASS |
+| 8 | `spectral_expansive` | spectral | **38** | `spectral_analyze` | PASS |
+| 9 | `recurrence_converges` | recurrence | **46** | `rec_run`/`synth_weights` | PASS |
+
+**Named count: 9** · Latest: **9 PASS / 0 FAIL** (`logs/run-20261007-075943.log`)
+
+## Property coverage files
+
+| File | Props |
+|------|-------|
+| `tests/goldilocks.ijs` | 1–18 (+ named) |
+| `tests/constants.ijs` | 19–25 |
+| `tests/pmat.ijs` | 26–32 (+ named) |
+| `tests/spectral.ijs` | 33–38 (+ named) |
+| `tests/recurrence.ijs` | 39–46 (+ named; 41 SKIP) |
+| `tests/emit_csl_ace.ijs` | 47–56 (47/55/56 SKIP; 49–50 FAIL) |
+
+### Load convention
+
+```
+load '../j/foundry.ijs'
+foundry_export ''    NB. copies J_API names into base
+```
+
+## Out of scope / SKIP
+
+- **41** narrative Banach unique fixed-point
+- **47** WORM/seal / triple-lock theater
+- **55** guardian (no Core verb)
+- **56** consensus narrative
+
+## Known Core FAILs (honest)
+
+- **49** attenuate scale (J RTL vs Spec)
+- **50** `csl_neutrality` index error (J RTL loop bound)

verify/LICENSE

@@ -0,0 +1,661 @@
+                    GNU AFFERO GENERAL PUBLIC LICENSE
+                       Version 3, 19 November 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <https://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                            Preamble
+
+  The GNU Affero General Public License is a free, copyleft license for
+software and other kinds of works, specifically designed to ensure
+cooperation with the community in the case of network server software.
+
+  The licenses for most software and other practical works are designed
+to take away your freedom to share and change the works.  By contrast,
+our General Public Licenses are intended to guarantee your freedom to
+share and change all versions of a program--to make sure it remains free
+software for all its users.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+them if you wish), that you receive source code or can get it if you
+want it, that you can change the software or use pieces of it in new
+free programs, and that you know you can do these things.
+
+  Developers that use our General Public Licenses protect your rights
+with two steps: (1) assert copyright on the software, and (2) offer
+you this License which gives you legal permission to copy, distribute
+and/or modify the software.
+
+  A secondary benefit of defending all users' freedom is that
+improvements made in alternate versions of the program, if they
+receive widespread use, become available for other developers to
+incorporate.  Many developers of free software are heartened and
+encouraged by the resulting cooperation.  However, in the case of
+software used on network servers, this result may fail to come about.
+The GNU General Public License permits making a modified version and
+letting the public access it on a server without ever releasing its
+source code to the public.
+
+  The GNU Affero General Public License is designed specifically to
+ensure that, in such cases, the modified source code becomes available
+to the community.  It requires the operator of a network server to
+provide the source code of the modified version running there to the
+users of that server.  Therefore, public use of a modified version, on
+a publicly accessible server, gives the public access to the source
+code of the modified version.
+
+  An older license, called the Affero General Public License and
+published by Affero, was designed to accomplish similar goals.  This is
+a different license, not a version of the Affero GPL, but Affero has
+released a new version of the Affero GPL which permits relicensing under
+this license.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+
+                       TERMS AND CONDITIONS
+
+  0. Definitions.
+
+  "This License" refers to version 3 of the GNU Affero General Public License.
+
+  "Copyright" also means copyright-like laws that apply to other kinds of
+works, such as semiconductor masks.
+
+  "The Program" refers to any copyrightable work licensed under this
+License.  Each licensee is addressed as "you".  "Licensees" and
+"recipients" may be individuals or organizations.
+
+  To "modify" a work means to copy from or adapt all or part of the work
+in a fashion requiring copyright permission, other than the making of an
+exact copy.  The resulting work is called a "modified version" of the
+earlier work or a work "based on" the earlier work.
+
+  A "covered work" means either the unmodified Program or a work based
+on the Program.
+
+  To "propagate" a work means to do anything with it that, without
+permission, would make you directly or secondarily liable for
+infringement under applicable copyright law, except executing it on a
+computer or modifying a private copy.  Propagation includes copying,
+distribution (with or without modification), making available to the
+public, and in some countries other activities as well.
+
+  To "convey" a work means any kind of propagation that enables other
+parties to make or receive copies.  Mere interaction with a user through
+a computer network, with no transfer of a copy, is not conveying.
+
+  An interactive user interface displays "Appropriate Legal Notices"
+to the extent that it includes a convenient and prominently visible
+feature that (1) displays an appropriate copyright notice, and (2)
+tells the user that there is no warranty for the work (except to the
+extent that warranties are provided), that licensees may convey the
+work under this License, and how to view a copy of this License.  If
+the interface presents a list of user commands or options, such as a
+menu, a prominent item in the list meets this criterion.
+
+  1. Source Code.
+
+  The "source code" for a work means the preferred form of the work
+for making modifications to it.  "Object code" means any non-source
+form of a work.
+
+  A "Standard Interface" means an interface that either is an official
+standard defined by a recognized standards body, or, in the case of
+interfaces specified for a particular programming language, one that
+is widely used among developers working in that language.
+
+  The "System Libraries" of an executable work include anything, other
+than the work as a whole, that (a) is included in the normal form of
+packaging a Major Component, but which is not part of that Major
+Component, and (b) serves only to enable use of the work with that
+Major Component, or to implement a Standard Interface for which an
+implementation is available to the public in source code form.  A
+"Major Component", in this context, means a major essential component
+(kernel, window system, and so on) of the specific operating system
+(if any) on which the executable work runs, or a compiler used to
+produce the work, or an object code interpreter used to run it.
+
+  The "Corresponding Source" for a work in object code form means all
+the source code needed to generate, install, and (for an executable
+work) run the object code and to modify the work, including scripts to
+control those activities.  However, it does not include the work's
+System Libraries, or general-purpose tools or generally available free
+programs which are used unmodified in performing those activities but
+which are not part of the work.  For example, Corresponding Source
+includes interface definition files associated with source files for
+the work, and the source code for shared libraries and dynamically
+linked subprograms that the work is specifically designed to require,
+such as by intimate data communication or control flow between those
+subprograms and other parts of the work.
+
+  The Corresponding Source need not include anything that users
+can regenerate automatically from other parts of the Corresponding
+Source.
+
+  The Corresponding Source for a work in source code form is that
+same work.
+
+  2. Basic Permissions.
+
+  All rights granted under this License are granted for the term of
+copyright on the Program, and are irrevocable provided the stated
+conditions are met.  This License explicitly affirms your unlimited
+permission to run the unmodified Program.  The output from running a
+covered work is covered by this License only if the output, given its
+content, constitutes a covered work.  This License acknowledges your
+rights of fair use or other equivalent, as provided by copyright law.
+
+  You may make, run and propagate covered works that you do not
+convey, without conditions so long as your license otherwise remains
+in force.  You may convey covered works to others for the sole purpose
+of having them make modifications exclusively for you, or provide you
+with facilities for running those works, provided that you comply with
+the terms of this License in conveying all material for which you do
+not control copyright.  Those thus making or running the covered works
+for you must do so exclusively on your behalf, under your direction
+and control, on terms that prohibit them from making any copies of
+your copyrighted material outside their relationship with you.
+
+  Conveying under any other circumstances is permitted solely under
+the conditions stated below.  Sublicensing is not allowed; section 10
+makes it unnecessary.
+
+  3. Protecting Users' Legal Rights From Anti-Circumvention Law.
+
+  No covered work shall be deemed part of an effective technological
+measure under any applicable law fulfilling obligations under article
+11 of the WIPO copyright treaty adopted on 20 December 1996, or
+similar laws prohibiting or restricting circumvention of such
+measures.
+
+  When you convey a covered work, you waive any legal power to forbid
+circumvention of technological measures to the extent such circumvention
+is effected by exercising rights under this License with respect to
+the covered work, and you disclaim any intention to limit operation or
+modification of the work as a means of enforcing, against the work's
+users, your or third parties' legal rights to forbid circumvention of
+technological measures.
+
+  4. Conveying Verbatim Copies.
+
+  You may convey verbatim copies of the Program's source code as you
+receive it, in any medium, provided that you conspicuously and
+appropriately publish on each copy an appropriate copyright notice;
+keep intact all notices stating that this License and any
+non-permissive terms added in accord with section 7 apply to the code;
+keep intact all notices of the absence of any warranty; and give all
+recipients a copy of this License along with the Program.
+
+  You may charge any price or no price for each copy that you convey,
+and you may offer support or warranty protection for a fee.
+
+  5. Conveying Modified Source Versions.
+
+  You may convey a work based on the Program, or the modifications to
+produce it from the Program, in the form of source code under the
+terms of section 4, provided that you also meet all of these conditions:
+
+    a) The work must carry prominent notices stating that you modified
+    it, and giving a relevant date.
+
+    b) The work must carry prominent notices stating that it is
+    released under this License and any conditions added under section
+    7.  This requirement modifies the requirement in section 4 to
+    "keep intact all notices".
+
+    c) You must license the entire work, as a whole, under this
+    License to anyone who comes into possession of a copy.  This
+    License will therefore apply, along with any applicable section 7
+    additional terms, to the whole of the work, and all its parts,
+    regardless of how they are packaged.  This License gives no
+    permission to license the work in any other way, but it does not
+    invalidate such permission if you have separately received it.
+
+    d) If the work has interactive user interfaces, each must display
+    Appropriate Legal Notices; however, if the Program has interactive
+    interfaces that do not display Appropriate Legal Notices, your
+    work need not make them do so.
+
+  A compilation of a covered work with other separate and independent
+works, which are not by their nature extensions of the covered work,
+and which are not combined with it such as to form a larger program,
+in or on a volume of a storage or distribution medium, is called an
+"aggregate" if the compilation and its resulting copyright are not
+used to limit the access or legal rights of the compilation's users
+beyond what the individual works permit.  Inclusion of a covered work
+in an aggregate does not cause this License to apply to the other
+parts of the aggregate.
+
+  6. Conveying Non-Source Forms.
+
+  You may convey a covered work in object code form under the terms
+of sections 4 and 5, provided that you also convey the
+machine-readable Corresponding Source under the terms of this License,
+in one of these ways:
+
+    a) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by the
+    Corresponding Source fixed on a durable physical medium
+    customarily used for software interchange.
+
+    b) Convey the object code in, or embodied in, a physical product
+    (including a physical distribution medium), accompanied by a
+    written offer, valid for at least three years and valid for as
+    long as you offer spare parts or customer support for that product
+    model, to give anyone who possesses the object code either (1) a
+    copy of the Corresponding Source for all the software in the
+    product that is covered by this License, on a durable physical
+    medium customarily used for software interchange, for a price no
+    more than your reasonable cost of physically performing this
+    conveying of source, or (2) access to copy the
+    Corresponding Source from a network server at no charge.
+
+    c) Convey individual copies of the object code with a copy of the
+    written offer to provide the Corresponding Source.  This
+    alternative is allowed only occasionally and noncommercially, and
+    only if you received the object code with such an offer, in accord
+    with subsection 6b.
+
+    d) Convey the object code by offering access from a designated
+    place (gratis or for a charge), and offer equivalent access to the
+    Corresponding Source in the same way through the same place at no
+    further charge.  You need not require recipients to copy the
+    Corresponding Source along with the object code.  If the place to
+    copy the object code is a network server, the Corresponding Source
+    may be on a different server (operated by you or a third party)
+    that supports equivalent copying facilities, provided you maintain
+    clear directions next to the object code saying where to find the
+    Corresponding Source.  Regardless of what server hosts the
+    Corresponding Source, you remain obligated to ensure that it is
+    available for as long as needed to satisfy these requirements.
+
+    e) Convey the object code using peer-to-peer transmission, provided
+    you inform other peers where the object code and Corresponding
+    Source of the work are being offered to the general public at no
+    charge under subsection 6d.
+
+  A separable portion of the object code, whose source code is excluded
+from the Corresponding Source as a System Library, need not be
+included in conveying the object code work.
+
+  A "User Product" is either (1) a "consumer product", which means any
+tangible personal property which is normally used for personal, family,
+or household purposes, or (2) anything designed or sold for incorporation
+into a dwelling.  In determining whether a product is a consumer product,
+doubtful cases shall be resolved in favor of coverage.  For a particular
+product received by a particular user, "normally used" refers to a
+typical or common use of that class of product, regardless of the status
+of the particular user or of the way in which the particular user
+actually uses, or expects or is expected to use, the product.  A product
+is a consumer product regardless of whether the product has substantial
+commercial, industrial or non-consumer uses, unless such uses represent
+the only significant mode of use of the product.
+
+  "Installation Information" for a User Product means any methods,
+procedures, authorization keys, or other information required to install
+and execute modified versions of a covered work in that User Product from
+a modified version of its Corresponding Source.  The information must
+suffice to ensure that the continued functioning of the modified object
+code is in no case prevented or interfered with solely because
+modification has been made.
+
+  If you convey an object code work under this section in, or with, or
+specifically for use in, a User Product, and the conveying occurs as
+part of a transaction in which the right of possession and use of the
+User Product is transferred to the recipient in perpetuity or for a
+fixed term (regardless of how the transaction is characterized), the
+Corresponding Source conveyed under this section must be accompanied
+by the Installation Information.  But this requirement does not apply
+if neither you nor any third party retains the ability to install
+modified object code on the User Product (for example, the work has
+been installed in ROM).
+
+  The requirement to provide Installation Information does not include a
+requirement to continue to provide support service, warranty, or updates
+for a work that has been modified or installed by the recipient, or for
+the User Product in which it has been modified or installed.  Access to a
+network may be denied when the modification itself materially and
+adversely affects the operation of the network or violates the rules and
+protocols for communication across the network.
+
+  Corresponding Source conveyed, and Installation Information provided,
+in accord with this section must be in a format that is publicly
+documented (and with an implementation available to the public in
+source code form), and must require no special password or key for
+unpacking, reading or copying.
+
+  7. Additional Terms.
+
+  "Additional permissions" are terms that supplement the terms of this
+License by making exceptions from one or more of its conditions.
+Additional permissions that are applicable to the entire Program shall
+be treated as though they were included in this License, to the extent
+that they are valid under applicable law.  If additional permissions
+apply only to part of the Program, that part may be used separately
+under those permissions, but the entire Program remains governed by
+this License without regard to the additional permissions.
+
+  When you convey a copy of a covered work, you may at your option
+remove any additional permissions from that copy, or from any part of
+it.  (Additional permissions may be written to require their own
+removal in certain cases when you modify the work.)  You may place
+additional permissions on material, added by you to a covered work,
+for which you have or can give appropriate copyright permission.
+
+  Notwithstanding any other provision of this License, for material you
+add to a covered work, you may (if authorized by the copyright holders of
+that material) supplement the terms of this License with terms:
+
+    a) Disclaiming warranty or limiting liability differently from the
+    terms of sections 15 and 16 of this License; or
+
+    b) Requiring preservation of specified reasonable legal notices or
+    author attributions in that material or in the Appropriate Legal
+    Notices displayed by works containing it; or
+
+    c) Prohibiting misrepresentation of the origin of that material, or
+    requiring that modified versions of such material be marked in
+    reasonable ways as different from the original version; or
+
+    d) Limiting the use for publicity purposes of names of licensors or
+    authors of the material; or
+
+    e) Declining to grant rights under trademark law for use of some
+    trade names, trademarks, or service marks; or
+
+    f) Requiring indemnification of licensors and authors of that
+    material by anyone who conveys the material (or modified versions of
+    it) with contractual assumptions of liability to the recipient, for
+    any liability that these contractual assumptions directly impose on
+    those licensors and authors.
+
+  All other non-permissive additional terms are considered "further
+restrictions" within the meaning of section 10.  If the Program as you
+received it, or any part of it, contains a notice stating that it is
+governed by this License along with a term that is a further
+restriction, you may remove that term.  If a license document contains
+a further restriction but permits relicensing or conveying under this
+License, you may add to a covered work material governed by the terms
+of that license document, provided that the further restriction does
+not survive such relicensing or conveying.
+
+  If you add terms to a covered work in accord with this section, you
+must place, in the relevant source files, a statement of the
+additional terms that apply to those files, or a notice indicating
+where to find the applicable terms.
+
+  Additional terms, permissive or non-permissive, may be stated in the
+form of a separately written license, or stated as exceptions;
+the above requirements apply either way.
+
+  8. Termination.
+
+  You may not propagate or modify a covered work except as expressly
+provided under this License.  Any attempt otherwise to propagate or
+modify it is void, and will automatically terminate your rights under
+this License (including any patent licenses granted under the third
+paragraph of section 11).
+
+  However, if you cease all violation of this License, then your
+license from a particular copyright holder is reinstated (a)
+provisionally, unless and until the copyright holder explicitly and
+finally terminates your license, and (b) permanently, if the copyright
+holder fails to notify you of the violation by some reasonable means
+prior to 60 days after the cessation.
+
+  Moreover, your license from a particular copyright holder is
+reinstated permanently if the copyright holder notifies you of the
+violation by some reasonable means, this is the first time you have
+received notice of violation of this License (for any work) from that
+copyright holder, and you cure the violation prior to 30 days after
+your receipt of the notice.
+
+  Termination of your rights under this section does not terminate the
+licenses of parties who have received copies or rights from you under
+this License.  If your rights have been terminated and not permanently
+reinstated, you do not qualify to receive new licenses for the same
+material under section 10.
+
+  9. Acceptance Not Required for Having Copies.
+
+  You are not required to accept this License in order to receive or
+run a copy of the Program.  Ancillary propagation of a covered work
+occurring solely as a consequence of using peer-to-peer transmission
+to receive a copy likewise does not require acceptance.  However,
+nothing other than this License grants you permission to propagate or
+modify any covered work.  These actions infringe copyright if you do
+not accept this License.  Therefore, by modifying or propagating a
+covered work, you indicate your acceptance of this License to do so.
+
+  10. Automatic Licensing of Downstream Recipients.
+
+  Each time you convey a covered work, the recipient automatically
+receives a license from the original licensors, to run, modify and
+propagate that work, subject to this License.  You are not responsible
+for enforcing compliance by third parties with this License.
+
+  An "entity transaction" is a transaction transferring control of an
+organization, or substantially all assets of one, or subdividing an
+organization, or merging organizations.  If propagation of a covered
+work results from an entity transaction, each party to that
+transaction who receives a copy of the work also receives whatever
+licenses to the work the party's predecessor in interest had or could
+give under the previous paragraph, plus a right to possession of the
+Corresponding Source of the work from the predecessor in interest, if
+the predecessor has it or can get it with reasonable efforts.
+
+  You may not impose any further restrictions on the exercise of the
+rights granted or affirmed under this License.  For example, you may
+not impose a license fee, royalty, or other charge for exercise of
+rights granted under this License, and you may not initiate litigation
+(including a cross-claim or counterclaim in a lawsuit) alleging that
+any patent claim is infringed by making, using, selling, offering for
+sale, or importing the Program or any portion of it.
+
+  11. Patents.
+
+  A "contributor" is a copyright holder who authorizes use under this
+License of the Program or a work on which the Program is based.  The
+work thus licensed is called the contributor's "contributor version".
+
+  A contributor's "essential patent claims" are all patent claims
+owned or controlled by the contributor, whether already acquired or
+hereafter acquired, that would be infringed by some manner, permitted
+by this License, of making, using, or selling its contributor version,
+but do not include claims that would be infringed only as a
+consequence of further modification of the contributor version.  For
+purposes of this definition, "control" includes the right to grant
+patent sublicenses in a manner consistent with the requirements of
+this License.
+
+  Each contributor grants you a non-exclusive, worldwide, royalty-free
+patent license under the contributor's essential patent claims, to
+make, use, sell, offer for sale, import and otherwise run, modify and
+propagate the contents of its contributor version.
+
+  In the following three paragraphs, a "patent license" is any express
+agreement or commitment, however denominated, not to enforce a patent
+(such as an express permission to practice a patent or covenant not to
+sue for patent infringement).  To "grant" such a patent license to a
+party means to make such an agreement or commitment not to enforce a
+patent against the party.
+
+  If you convey a covered work, knowingly relying on a patent license,
+and the Corresponding Source of the work is not available for anyone
+to copy, free of charge and under the terms of this License, through a
+publicly available network server or other readily accessible means,
+then you must either (1) cause the Corresponding Source to be so
+available, or (2) arrange to deprive yourself of the benefit of the
+patent license for this particular work, or (3) arrange, in a manner
+consistent with the requirements of this License, to extend the patent
+license to downstream recipients.  "Knowingly relying" means you have
+actual knowledge that, but for the patent license, your conveying the
+covered work in a country, or your recipient's use of the covered work
+in a country, would infringe one or more identifiable patents in that
+country that you have reason to believe are valid.
+
+  If, pursuant to or in connection with a single transaction or
+arrangement, you convey, or propagate by procuring conveyance of, a
+covered work, and grant a patent license to some of the parties
+receiving the covered work authorizing them to use, propagate, modify
+or convey a specific copy of the covered work, then the patent license
+you grant is automatically extended to all recipients of the covered
+work and works based on it.
+
+  A patent license is "discriminatory" if it does not include within
+the scope of its coverage, prohibits the exercise of, or is
+conditioned on the non-exercise of one or more of the rights that are
+specifically granted under this License.  You may not convey a covered
+work if you are a party to an arrangement with a third party that is
+in the business of distributing software, under which you make payment
+to the third party based on the extent of your activity of conveying
+the work, and under which the third party grants, to any of the
+parties who would receive the covered work from you, a discriminatory
+patent license (a) in connection with copies of the covered work
+conveyed by you (or copies made from those copies), or (b) primarily
+for and in connection with specific products or compilations that
+contain the covered work, unless you entered into that arrangement,
+or that patent license was granted, prior to 28 March 2007.
+
+  Nothing in this License shall be construed as excluding or limiting
+any implied license or other defenses to infringement that may
+otherwise be available to you under applicable patent law.
+
+  12. No Surrender of Others' Freedom.
+
+  If conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot convey a
+covered work so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you may
+not convey it at all.  For example, if you agree to terms that obligate you
+to collect a royalty for further conveying from those to whom you convey
+the Program, the only way you could satisfy both those terms and this
+License would be to refrain entirely from conveying the Program.
+
+  13. Remote Network Interaction; Use with the GNU General Public License.
+
+  Notwithstanding any other provision of this License, if you modify the
+Program, your modified version must prominently offer all users
+interacting with it remotely through a computer network (if your version
+supports such interaction) an opportunity to receive the Corresponding
+Source of your version by providing access to the Corresponding Source
+from a network server at no charge, through some standard or customary
+means of facilitating copying of software.  This Corresponding Source
+shall include the Corresponding Source for any work covered by version 3
+of the GNU General Public License that is incorporated pursuant to the
+following paragraph.
+
+  Notwithstanding any other provision of this License, you have
+permission to link or combine any covered work with a work licensed
+under version 3 of the GNU General Public License into a single
+combined work, and to convey the resulting work.  The terms of this
+License will continue to apply to the part which is the covered work,
+but the work with which it is combined will remain governed by version
+3 of the GNU General Public License.
+
+  14. Revised Versions of this License.
+
+  The Free Software Foundation may publish revised and/or new versions of
+the GNU Affero General Public License from time to time.  Such new versions
+will be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+  Each version is given a distinguishing version number.  If the
+Program specifies that a certain numbered version of the GNU Affero General
+Public License "or any later version" applies to it, you have the
+option of following the terms and conditions either of that numbered
+version or of any later version published by the Free Software
+Foundation.  If the Program does not specify a version number of the
+GNU Affero General Public License, you may choose any version ever published
+by the Free Software Foundation.
+
+  If the Program specifies that a proxy can decide which future
+versions of the GNU Affero General Public License can be used, that proxy's
+public statement of acceptance of a version permanently authorizes you
+to choose that version for the Program.
+
+  Later license versions may give you additional or different
+permissions.  However, no additional obligations are imposed on any
+author or copyright holder as a result of your choosing to follow a
+later version.
+
+  15. Disclaimer of Warranty.
+
+  THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY
+APPLICABLE LAW.  EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT
+HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY
+OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO,
+THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM
+IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF
+ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+  16. Limitation of Liability.
+
+  IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS
+THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY
+GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE
+USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF
+DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD
+PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS),
+EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGES.
+
+  17. Interpretation of Sections 15 and 16.
+
+  If the disclaimer of warranty and limitation of liability provided
+above cannot be given local legal effect according to their terms,
+reviewing courts shall apply local law that most closely approximates
+an absolute waiver of all civil liability in connection with the
+Program, unless a warranty or assumption of liability accompanies a
+copy of the Program in return for a fee.
+
+                     END OF TERMS AND CONDITIONS
+
+            How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+state the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software: you can redistribute it and/or modify
+    it under the terms of the GNU Affero General Public License as published by
+    the Free Software Foundation, either version 3 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU Affero General Public License for more details.
+
+    You should have received a copy of the GNU Affero General Public License
+    along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+Also add information on how to contact you by electronic and paper mail.
+
+  If your software can interact with users remotely through a computer
+network, you should also make sure that it provides a way for users to
+get its source.  For example, if your program is a web application, its
+interface could display a "Source" link that leads users to an archive
+of the code.  There are many ways you could offer source, and different
+solutions will be better for different programs; see section 13 for the
+specific requirements.
+
+  You should also get your employer (if you work as a programmer) or school,
+if any, to sign a "copyright disclaimer" for the program, if necessary.
+For more information on this, and how to apply and follow the GNU AGPL, see
+<https://www.gnu.org/licenses/>.

verify/PROPERTY_MAP.md

@@ -0,0 +1,108 @@
+<!--
+  Copyright (C) 2026 Foundry J contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Harness ↔ PROPERTIES.md mapping + measured results
+
+Properties: `spec/PROPERTIES.md` (56).
+Core entry: `j/foundry.ijs` + `foundry_export''`.
+Log: `logs/run-20261007-075943.log` (PT).
+
+Statuses below match that log exactly. Named baseline tests are listed after the property table.
+
+| # | Title | Status | Harness id | Log citation |
+|---|-------|--------|------------|--------------|
+| 1 | Goldilocks prime (decimal) | **PASS** | `prop_1` | `PASS prop_1` |
+| 2 | Goldilocks prime (hex / named) | **PASS** | `prop_2` | `PASS prop_2` |
+| 3 | Field elements u64 reduced mod p | **PASS** | `prop_3` | `PASS prop_3` |
+| 4 | Elem construction reduces | **PASS** | `prop_4` | `PASS prop_4` |
+| 5 | Congruence 2^64 ≡ 2^32−1 (mod p) | **PASS** | `prop_5` | `PASS prop_5` |
+| 6 | Fold constant EPSILON | **PASS** | `prop_6` | `PASS prop_6` |
+| 7 | 128-bit product split (via fp_mulmod) | **PASS** | `prop_7` | `PASS prop_7` |
+| 8 | hi split into 32-bit halves | **PASS** | `prop_8` | `PASS prop_8` |
+| 9 | Reduction identity (fold) | **PASS** | `prop_9` | `PASS prop_9` |
+| 10 | Underflow handling on fold | **PASS** | `prop_10` | `PASS prop_10` |
+| 11 | Final conditional reduction | **PASS** | `prop_11` | `PASS prop_11` |
+| 12 | Single-limb reduce | **PASS** | `prop_12` | `PASS prop_12` |
+| 13 | Addition mod p | **PASS** | `prop_13` | `PASS prop_13` |
+| 14 | Subtraction mod p | **PASS** | `prop_14` | `PASS prop_14` |
+| 15 | Multiplication via mulmod | **PASS** | `prop_15` | `PASS prop_15` |
+| 16 | Fermat inverse | **PASS** | `prop_16` | `PASS prop_16` |
+| 17 | Binary exponentiation | **PASS** | `prop_17` | `PASS prop_17` |
+| 18 | Batch add/mul | **PASS** | `prop_18` | `PASS prop_18` |
+| 19 | K_MAX | **PASS** | `prop_19` | `PASS prop_19` |
+| 20 | MAX_DRIFT | **PASS** | `prop_20` | `PASS prop_20` |
+| 21 | PIRTM_MAGIC | **PASS** | `prop_21` | `PASS prop_21` |
+| 22 | PHI | **PASS** | `prop_22` | `PASS prop_22` |
+| 23 | P_64 first 64 primes | **PASS** | `prop_23` | `PASS prop_23` |
+| 24 | GENESIS_HASH_SIZE | **PASS** | `prop_24` | `PASS prop_24` |
+| 25 | Tier epsilons | **PASS** | `prop_25` | `PASS prop_25` |
+| 26 | PMat entry shape | **PASS** | `prop_26` | `PASS prop_26` |
+| 27 | Insert domain checks | **PASS** | `prop_27` | `PASS prop_27` |
+| 28 | Grading condition (C++ stub mirror) | **PASS** | `prop_28` | `PASS prop_28` |
+| 29 | Conservation theorem | **PASS** | `prop_29` | `PASS prop_29` |
+| 30 | Composition preserves grading/shape | **PASS** | `prop_30` | `PASS prop_30` |
+| 31 | Compose monomial accumulation rule | **PASS** | `prop_31` | `PASS prop_31` |
+| 32 | Frobenius norm of PMat | **PASS** | `prop_32` | `PASS prop_32` |
+| 33 | Gershgorin disk bound | **PASS** | `prop_33` | `PASS prop_33` |
+| 34 | Contractive test (Gershgorin) | **PASS** | `prop_34` | `PASS prop_34` |
+| 35 | Power iteration (Rayleigh) | **PASS** | `prop_35` | `PASS prop_35` |
+| 36 | Contractive test (power iteration) | **PASS** | `prop_36` | `PASS prop_36` |
+| 37 | Analyze fallback policy | **PASS** | `prop_37` | `PASS prop_37` |
+| 38 | Tested contractive / expansive examples | **PASS** | `prop_38` | `PASS prop_38` |
+| 39 | Recurrence equation | **PASS** | `prop_39` | `PASS prop_39` |
+| 40 | Contraction condition | **PASS** | `prop_40` | `PASS prop_40` |
+| 41 | Unique fixed-point guarantee (narrative) | **SKIP** | `prop_41` | `SKIP prop_41: narrative-only Banach guarantee` |
+| 42 | q estimate in step | **PASS** | `prop_42` | `PASS prop_42` |
+| 43 | Soft projection | **PASS** | `prop_43` | `PASS prop_43` |
+| 44 | Weight budget split | **PASS** | `prop_44` | `PASS prop_44` |
+| 45 | Projector | **PASS** | `prop_45` | `PASS prop_45` |
+| 46 | Residual / convergence | **PASS** | `prop_46` | `PASS prop_46` |
+| 47 | WORM / seal chain invariant | **SKIP** | `prop_47` | `SKIP prop_47: WORM/seal chain / triple-lock theater out of harness scope` |
+| 48 | Emission Suppress | **PASS** | `prop_48` | `PASS prop_48` |
+| 49 | Emission Attenuate scale | **FAIL** | `prop_49` | `FAIL prop_49: Spec expect 0.4*out; Core got 1.4 2.8 4.2` |
+| 50 | CSL neutrality | **FAIL** | `prop_50` | `FAIL prop_50: index error in csl_neutrality` |
+| 51 | CSL beneficence | **PASS** | `prop_51` | `PASS prop_51` |
+| 52 | CSL commutation | **PASS** | `prop_52` | `PASS prop_52` |
+| 53 | AceCertificate safety margin | **PASS** | `prop_53` | `PASS prop_53` |
+| 54 | AceCertificate tail bound | **PASS** | `prop_54` | `PASS prop_54` |
+| 55 | Guardian spectral legality | **SKIP** | `prop_55` | `SKIP prop_55: no Core guardian verb (gate theater out of harness scope)` |
+| 56 | Consensus / false-positive bound | **SKIP** | `prop_56` | `SKIP prop_56: narrative-only consensus / 2^-256 bound` |
+
+## Property summary (56)
+
+| Status | Count |
+|--------|------:|
+| PASS | **50** |
+| FAIL | **2** (`prop_49`, `prop_50`) |
+| SKIP | **4** (`prop_41`, `prop_47`, `prop_55`, `prop_56`) |
+| BLOCKED | **0** |
+
+## Named baseline tests (same log)
+
+| Harness test | Primary # | Measured |
+|--------------|-----------|----------|
+| `goldilocks_add` | 13 | **PASS** |
+| `goldilocks_mul` | 15 | **PASS** |
+| `goldilocks_inv` | 16 | **PASS** |
+| `goldilocks_sub` | 14 | **PASS** |
+| `pmat_insert` | 27 | **PASS** |
+| `pmat_conservation` | 29 | **PASS** |
+| `spectral_contractive` | 38 | **PASS** |
+| `spectral_expansive` | 38 | **PASS** |
+| `recurrence_converges` | 46 | **PASS** |
+
+Named: **PASS=9 FAIL=0 BLOCKED=0** (no regression vs `logs/run-20261007-061853.log`).
+
+## Full harness counters (named + prop_*)
+
+`PASS=59 FAIL=2 SKIP=4 BLOCKED=0` · `exit_code=1`
+
+## Notes for Hilbert / Core
+
+1. **Measured against Core** `7cc1ba6` (BOXING.md freeze). Prop 16 / `goldilocks_inv` **PASS**. Prop 46 driven via `rec_run` (list of `<StepInfo>`).
+2. **prop_49 FAIL** — Spec `max(0,(1−ε)−q)`; Core `emit_apply` Attenuate uses J RTL `1 - eps - q` → `1-(eps-q)`, so q=0.5 ε=0.1 yields scale 1.4 not 0.4.
+3. **prop_50 FAIL** — Core `csl_neutrality` loop bound `n - i - 1` is J RTL (`n-(i-1)`), causing index error for normal vector lengths. Measured FAIL (verb exists; not SKIP).
+4. Props 7–11 exercise mulmod via `fp_mulmod` identities (128-bit split internals are not separately exported).
+5. Prop 28 mirrors C++ stub (`pmat_validate_grading` always 1); Spec gap noted in PROPERTIES.md / GAP_DECISIONS.

verify/README.md

@@ -0,0 +1,34 @@
+<!--
+  Copyright (C) 2026 Foundry J contributors
+  SPDX-License-Identifier: AGPL-3.0-or-later
+-->
+
+# Foundry J — Verification Harness
+
+Pure-J checks for all 56 mathematical properties from `spec/PROPERTIES.md`.
+Core is the arithmetic authority (no Python).
+
+## Run
+
+```bash
+cd verify
+./run.sh
+# → logs/run-<timestamp>.log
+```
+
+jconsole: `/home/box/j/j9.7/bin/jconsole` (override with `JCONSOLE`).
+
+## Core load
+
+```
+load '../j/foundry.ijs'
+foundry_export ''
+```
+
+## Verdicts
+
+`PASS` / `FAIL <name>: reason` / `SKIP <name>: reason` / `BLOCKED <name>: missing …`
+
+Per-property lines use ids `prop_1` … `prop_56`. Named baseline tests (`goldilocks_add`, …) are retained.
+
+Exit non-zero on any FAIL. See `PROPERTY_MAP.md` for the authoritative table.

verify/harness.ijs

@@ -0,0 +1,55 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. PASS/FAIL/SKIP/BLOCKED helpers + Foundry Core loader (foundry.ijs + foundry_export).
+
+cocurrent 'z'
+
+PASS_N  =: 0
+FAIL_N  =: 0
+SKIP_N  =: 0
+BLOCK_N =: 0
+CORE_OK =: 0
+
+FOUNDRY_IJS =: '../j/foundry.ijs'
+
+fexists =: 3 : '0 < # 1!:0 < y'
+
+pass =: 3 : 0
+  PASS_N =: PASS_N + 1
+  echo 'PASS ' , y
+)
+
+fail =: 4 : 0
+  FAIL_N =: FAIL_N + 1
+  echo 'FAIL ' , y , ': ' , x
+)
+
+skip =: 4 : 0
+  SKIP_N =: SKIP_N + 1
+  echo 'SKIP ' , y , ': ' , x
+)
+
+blocked =: 4 : 0
+  BLOCK_N =: BLOCK_N + 1
+  echo 'BLOCKED ' , y , ': ' , x
+)
+
+NB. Load package entrypoint and export J_API verbs into base.
+NB. Returns 1 on success, 0 if foundry.ijs missing.
+load_foundry =: 3 : 0
+  if. -. fexists FOUNDRY_IJS do.
+    CORE_OK =: 0
+    0 return.
+  end.
+  load FOUNDRY_IJS
+  foundry_export ''
+  CORE_OK =: 1
+  1
+)
+
+harness_finish =: 3 : 0
+  echo ''
+  echo '═══════════════════════════════════════'
+  echo 'PASS=' , (": PASS_N) , ' FAIL=' , (": FAIL_N) , ' SKIP=' , (": SKIP_N) , ' BLOCKED=' , (": BLOCK_N)
+  if. FAIL_N > 0 do. 2!:55 ] 1 else. 2!:55 ] 0 end.
+)

verify/logs/run-20261007-061237.log

@@ -0,0 +1,53 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:12:37 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core dir: ../j/
+
+── goldilocks ──
+FAIL goldilocks_add: |value error: gl_add
+|   r=.100x     gl_add 200x
+|[-62] /workspace/foundry-j/verify/tests/goldilocks.ijs
+
+FAIL goldilocks_mul: |value error: gl_mul
+|   r=.7x     gl_mul 6x
+|[-62] /workspace/foundry-j/verify/tests/goldilocks.ijs
+
+FAIL goldilocks_inv: |value error: gl_inv
+|   inv=.    gl_inv a
+|[-62] /workspace/foundry-j/verify/tests/goldilocks.ijs
+
+FAIL goldilocks_sub: |value error: gl_sub
+|   r=.100x     gl_sub 50x
+|[-62] /workspace/foundry-j/verify/tests/goldilocks.ijs
+
+── pmat ──
+FAIL pmat_insert: |value error: pmat_new
+|   m=.    pmat_new 3 3
+|[-51] /workspace/foundry-j/verify/tests/pmat.ijs
+
+FAIL pmat_conservation: |value error: pmat_new
+|   m=.    pmat_new 2 2
+|[-51] /workspace/foundry-j/verify/tests/pmat.ijs
+
+── spectral ──
+FAIL spectral_contractive: |value error: spectral_analyze
+|   r=.    spectral_analyze J;0.1
+|[-42] /workspace/foundry-j/verify/tests/spectral.ijs
+
+FAIL spectral_expansive: |value error: spectral_analyze
+|   r=.    spectral_analyze J;0.1
+|[-42] /workspace/foundry-j/verify/tests/spectral.ijs
+
+── recurrence ──
+BLOCKED recurrence_converges: missing ../j/recurrence.ijs
+
+═══════════════════════════════════════
+PASS=0 FAIL=8 BLOCKED=1
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-061237.log

verify/logs/run-20261007-061352.log

@@ -0,0 +1,29 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:13:52 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core dir: ../j/
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+FAIL goldilocks_inv: expected 1 got 11152786313141180820
+PASS goldilocks_sub
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+── recurrence ──
+FAIL recurrence_converges: rec_run present but no recurrence_converges helper — need Core driver
+
+═══════════════════════════════════════
+PASS=7 FAIL=2 BLOCKED=0
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-061352.log

verify/logs/run-20261007-061501.log

@@ -0,0 +1,32 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:15:01 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core dir: ../j/
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+FAIL goldilocks_inv: expected 1 got 11152786313141180820
+PASS goldilocks_sub
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+── recurrence ──
+FAIL recurrence_converges: |index error in rec_run, executing dyad {::
+|   resid=.6    {::>info
+|[-53] /workspace/foundry-j/verify/tests/recurrence.ijs
+
+
+═══════════════════════════════════════
+PASS=7 FAIL=2 BLOCKED=0
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-061501.log

verify/logs/run-20261007-061701.log

@@ -0,0 +1,31 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:17:01 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core: ../j/foundry.ijs + foundry_export
+
+core_loaded=1
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+FAIL goldilocks_inv: expected 1 got 11152786313141180820
+PASS goldilocks_sub
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+── recurrence ──
+PASS recurrence_converges
+
+═══════════════════════════════════════
+PASS=8 FAIL=1 BLOCKED=0
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-061701.log

verify/logs/run-20261007-061836.log

@@ -0,0 +1,35 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:18:36 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core: ../j/foundry.ijs + foundry_export
+
+core_loaded=1
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+PASS goldilocks_inv
+PASS goldilocks_sub
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+── recurrence ──
+FAIL recurrence_converges: |domain error in run_recurrence, executing dyad <
+|x is boxed
+|   resid    <1e_6
+|[-52] /workspace/foundry-j/verify/tests/recurrence.ijs
+
+
+═══════════════════════════════════════
+PASS=8 FAIL=1 BLOCKED=0
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-061836.log

verify/logs/run-20261007-061847.log

@@ -0,0 +1,34 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:18:47 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core: ../j/foundry.ijs + foundry_export
+
+core_loaded=1
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+PASS goldilocks_inv
+PASS goldilocks_sub
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+── recurrence ──
+FAIL recurrence_converges: |value error: REC_STATE
+|       conv*.resid<1e_6
+|[-41] /workspace/foundry-j/verify/tests/recurrence.ijs
+
+
+═══════════════════════════════════════
+PASS=8 FAIL=1 BLOCKED=0
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-061847.log

verify/logs/run-20261007-061853.log

@@ -0,0 +1,31 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j/verify
+Timestamp (PT): 2026-10-07 06:18:53 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core: ../j/foundry.ijs + foundry_export
+
+core_loaded=1
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+PASS goldilocks_inv
+PASS goldilocks_sub
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+── recurrence ──
+PASS recurrence_converges
+
+═══════════════════════════════════════
+PASS=9 FAIL=0 BLOCKED=0
+────────────────────────────────────────
+exit_code=0
+log=logs/run-20261007-061853.log

verify/logs/run-20261007-075943.log

@@ -0,0 +1,93 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j-remote/verify
+Timestamp (PT): 2026-10-07 07:59:43 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core: ../j/foundry.ijs + foundry_export
+
+core_loaded=1
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+PASS goldilocks_inv
+PASS goldilocks_sub
+PASS prop_1
+PASS prop_2
+PASS prop_3
+PASS prop_4
+PASS prop_5
+PASS prop_6
+PASS prop_7
+PASS prop_8
+PASS prop_9
+PASS prop_10
+PASS prop_11
+PASS prop_12
+PASS prop_13
+PASS prop_14
+PASS prop_15
+PASS prop_16
+PASS prop_17
+PASS prop_18
+── constants ──
+PASS prop_19
+PASS prop_20
+PASS prop_21
+PASS prop_22
+PASS prop_23
+PASS prop_24
+PASS prop_25
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+PASS prop_26
+PASS prop_27
+PASS prop_28
+PASS prop_29
+PASS prop_30
+PASS prop_31
+PASS prop_32
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+PASS prop_33
+PASS prop_34
+PASS prop_35
+PASS prop_36
+PASS prop_37
+PASS prop_38
+── recurrence ──
+PASS recurrence_converges
+PASS prop_39
+PASS prop_40
+SKIP prop_41: narrative-only Banach guarantee
+PASS prop_42
+PASS prop_43
+PASS prop_44
+PASS prop_45
+PASS prop_46
+── emit/csl/ace ──
+SKIP prop_47: WORM/seal chain / triple-lock theater out of harness scope
+PASS prop_48
+FAIL prop_49: Spec expect 0.4*out; Core got 1.4 2.8 4.2
+FAIL prop_50: |index error in csl_neutrality_foundry_, executing dyad {
+|x is 3; too long for y, whose length is only 3
+|   dx=.|(i{xv)-j    {xv
+|[-82] /workspace/foundry-j-remote/verify/tests/emit_csl_ace.ijs
+
+PASS prop_51
+PASS prop_52
+PASS prop_53
+PASS prop_54
+SKIP prop_55: no Core guardian verb (gate theater out of harness scope)
+SKIP prop_56: narrative-only consensus / 2^-256 bound
+
+═══════════════════════════════════════
+PASS=59 FAIL=2 SKIP=4 BLOCKED=0
+────────────────────────────────────────
+exit_code=1
+log=logs/run-20261007-075943.log

verify/logs/run-20261007-080122.log

@@ -0,0 +1,89 @@
+Using jconsole: /home/box/j/j9.7/bin/jconsole
+Working directory: /workspace/foundry-j-repo/verify
+Timestamp (PT): 2026-10-07 08:01:22 PDT
+Core present: yes
+────────────────────────────────────────
+Foundry J — Verification Harness
+═══════════════════════════════════════
+jconsole: j9.7.1/j64/linux/commercial/www.jsoftware.com/2026-04-06T04:00:54/clang-14-0-0/SLEEF=0
+core: ../j/foundry.ijs + foundry_export
+
+core_loaded=1
+
+── goldilocks ──
+PASS goldilocks_add
+PASS goldilocks_mul
+PASS goldilocks_inv
+PASS goldilocks_sub
+PASS prop_1
+PASS prop_2
+PASS prop_3
+PASS prop_4
+PASS prop_5
+PASS prop_6
+PASS prop_7
+PASS prop_8
+PASS prop_9
+PASS prop_10
+PASS prop_11
+PASS prop_12
+PASS prop_13
+PASS prop_14
+PASS prop_15
+PASS prop_16
+PASS prop_17
+PASS prop_18
+── constants ──
+PASS prop_19
+PASS prop_20
+PASS prop_21
+PASS prop_22
+PASS prop_23
+PASS prop_24
+PASS prop_25
+── pmat ──
+PASS pmat_insert
+PASS pmat_conservation
+PASS prop_26
+PASS prop_27
+PASS prop_28
+PASS prop_29
+PASS prop_30
+PASS prop_31
+PASS prop_32
+── spectral ──
+PASS spectral_contractive
+PASS spectral_expansive
+PASS prop_33
+PASS prop_34
+PASS prop_35
+PASS prop_36
+PASS prop_37
+PASS prop_38
+── recurrence ──
+PASS recurrence_converges
+PASS prop_39
+PASS prop_40
+SKIP prop_41: narrative-only Banach guarantee
+PASS prop_42
+PASS prop_43
+PASS prop_44
+PASS prop_45
+PASS prop_46
+── emit/csl/ace ──
+SKIP prop_47: WORM/seal chain / triple-lock theater out of harness scope
+PASS prop_48
+PASS prop_49
+PASS prop_50
+PASS prop_51
+PASS prop_52
+PASS prop_53
+PASS prop_54
+SKIP prop_55: no Core guardian verb (gate theater out of harness scope)
+SKIP prop_56: narrative-only consensus / 2^-256 bound
+
+═══════════════════════════════════════
+PASS=61 FAIL=0 SKIP=4 BLOCKED=0
+────────────────────────────────────────
+exit_code=0
+log=logs/run-20261007-080122.log

verify/run.ijs

@@ -0,0 +1,30 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Foundry J verification suite — load Core via foundry.ijs + foundry_export.
+
+echo 'Foundry J — Verification Harness'
+echo '═══════════════════════════════════════'
+echo 'jconsole: ' , 9!:14 ''
+echo 'core: ../j/foundry.ijs + foundry_export'
+echo ''
+
+load 'harness.ijs'
+
+ok =. load_foundry ''
+echo 'core_loaded=' , ": ok
+echo ''
+
+echo '── goldilocks ──'
+load 'tests/goldilocks.ijs'
+echo '── constants ──'
+load 'tests/constants.ijs'
+echo '── pmat ──'
+load 'tests/pmat.ijs'
+echo '── spectral ──'
+load 'tests/spectral.ijs'
+echo '── recurrence ──'
+load 'tests/recurrence.ijs'
+echo '── emit/csl/ace ──'
+load 'tests/emit_csl_ace.ijs'
+
+harness_finish ''

verify/run.sh

@@ -0,0 +1,37 @@
+#!/usr/bin/env bash
+# Copyright (C) 2026 Foundry J contributors
+# SPDX-License-Identifier: AGPL-3.0-or-later
+#
+# Run the Foundry J verification suite and capture real stdout.
+set -u
+cd "$(dirname "$0")"
+
+JCONSOLE="${JCONSOLE:-/home/box/j/j9.7/bin/jconsole}"
+if [[ ! -x "$JCONSOLE" ]]; then
+  if [[ -x /home/box/j/j9.7/jconsole.sh ]]; then
+    JCONSOLE=/home/box/j/j9.7/jconsole.sh
+  else
+    echo "FAIL harness: jconsole not found at $JCONSOLE" >&2
+    exit 1
+  fi
+fi
+
+TS="$(date '+%Y%m%d-%H%M%S')"
+LOG="logs/run-${TS}.log"
+mkdir -p logs
+
+echo "Using jconsole: $JCONSOLE" | tee "$LOG"
+echo "Working directory: $(pwd)" | tee -a "$LOG"
+echo "Timestamp (PT): $(date '+%Y-%m-%d %H:%M:%S %Z')" | tee -a "$LOG"
+echo "Core present: $([[ -d ../j ]] && echo yes || echo no)" | tee -a "$LOG"
+echo "────────────────────────────────────────" | tee -a "$LOG"
+
+set +e
+"$JCONSOLE" run.ijs 2>&1 | tee -a "$LOG"
+RC=${PIPESTATUS[0]}
+set -e
+
+echo "────────────────────────────────────────" | tee -a "$LOG"
+echo "exit_code=$RC" | tee -a "$LOG"
+echo "log=$LOG" | tee -a "$LOG"
+exit "$RC"

verify/tests/constants.ijs

@@ -0,0 +1,55 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Named constants props 19–25.
+
+run_constants =: 3 : 0
+  if. -. CORE_OK do.
+    ('missing ' , FOUNDRY_IJS) blocked 'prop_19'
+    '' return.
+  end.
+
+  NB. prop_19 K_MAX
+  try.
+    if. K_MAX = 133144 do. pass 'prop_19' else. (('got ' , ": K_MAX)) fail 'prop_19' end.
+  catch. (13!:12 '') fail 'prop_19' end.
+
+  NB. prop_20 MAX_DRIFT
+  try.
+    if. MAX_DRIFT = 300000000000000000x do. pass 'prop_20'
+    else. (('got ' , ": MAX_DRIFT)) fail 'prop_20' end.
+  catch. (13!:12 '') fail 'prop_20' end.
+
+  NB. prop_21 PIRTM_MAGIC = 0x7F504952
+  try.
+    if. PIRTM_MAGIC = 2135945554x do. pass 'prop_21'
+    else. (('got ' , ": PIRTM_MAGIC)) fail 'prop_21' end.
+  catch. (13!:12 '') fail 'prop_21' end.
+
+  NB. prop_22 PHI
+  try.
+    if. 1e_12 > | PHI - 1.618033988749895 do. pass 'prop_22'
+    else. (('got ' , ": PHI)) fail 'prop_22' end.
+  catch. (13!:12 '') fail 'prop_22' end.
+
+  NB. prop_23 P_64 first 64 primes
+  try.
+    expect =. 2 3 5 7 11 13 17 19 23 29 31 37 41 43 47 53 59 61 67 71 73 79 83 89 97 101 103 107 109 113 127 131 137 139 149 151 157 163 167 173 179 181 191 193 197 199 211 223 227 229 233 239 241 251 257 263 269 271 277 281 283 293 307 311
+    if. (64 = # P64) *. (P64 -: expect) *. (P_64 -: P64) do. pass 'prop_23'
+    else. 'P64 mismatch' fail 'prop_23' end.
+  catch. (13!:12 '') fail 'prop_23' end.
+
+  NB. prop_24 GENESIS_HASH_SIZE (in foundry locale; not always exported)
+  try.
+    ghs =. GENESIS_HASH_SIZE_foundry_
+    if. ghs = 32 do. pass 'prop_24' else. (('got ' , ": ghs)) fail 'prop_24' end.
+  catch. (13!:12 '') fail 'prop_24' end.
+
+  NB. prop_25 tier epsilons
+  try.
+    ok =. ((tier_eps 1) = 0.10) *. ((tier_eps 2) = 0.05) *. ((tier_eps 3) = 0.02) *. ((tier_eps 4) = 0.01) *. ((tier_eps 99) = 0.10)
+    if. ok do. pass 'prop_25' else. 'tier_eps mismatch' fail 'prop_25' end.
+  catch. (13!:12 '') fail 'prop_25' end.
+  ''
+)
+
+run_constants ''

verify/tests/emit_csl_ace.ijs

@@ -0,0 +1,82 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Emission / CSL / Ace props 48–54; SKIP 47,55,56.
+
+run_emit_csl_ace =: 3 : 0
+  if. -. CORE_OK do.
+    ('missing ' , FOUNDRY_IJS) blocked 'prop_48'
+    '' return.
+  end.
+
+  NB. ── prop_47 WORM / seal chain (system-level theater) ─────────────────────
+  'WORM/seal chain / triple-lock theater out of harness scope' skip 'prop_47'
+
+  NB. ── prop_48 Emission Suppress ───────────────────────────────────────────
+  try.
+    z =. (1 2 3) emit_apply (0 0 0) ; 0.95 ; GP_SUPPRESS ; 0.1
+    p =. (1 2 3) emit_apply (0 0 0) ; 0.5 ; GP_SUPPRESS ; 0.1
+    if. (z -: 0 0 0) *. (p -: 1 2 3) do. pass 'prop_48'
+    else. (('suppress z=' , (": z) , ' p=' , ": p)) fail 'prop_48' end.
+  catch. (13!:12 '') fail 'prop_48' end.
+
+  NB. ── prop_49 Emission Attenuate scale max(0,1-ε-q) ────────────────────────
+  try.
+    NB. Spec: scale = max(0, (1-ε)-q); q=0.5 eps=0.1 → 0.4
+    NB. Core emit_apply uses J RTL `1 - eps - q` (=1.4 here) — mismatch → FAIL if so
+    out =. (1 2 3) emit_apply (0 0 0) ; 0.5 ; GP_ATTENUATE ; 0.1
+    expect =. 0.4 * 1 2 3
+    if. 1e_9 > >./ | out - expect do. pass 'prop_49'
+    else. (('Spec expect 0.4*out; Core got ' , ": out)) fail 'prop_49' end.
+  catch. (13!:12 '') fail 'prop_49' end.
+
+  NB. ── prop_50 CSL neutrality ──────────────────────────────────────────────
+  try.
+    NB. identity-ish: Tx = 0.5 * x → Lip 0.5 < 1+ε
+    v =. (1 2 3) csl_neutrality ((0.5 1 1.5) ; 0.1)
+    if. v = CSL_PASS do. pass 'prop_50'
+    else. (('neutrality=' , ": v)) fail 'prop_50' end.
+  catch. (13!:12 '') fail 'prop_50' end.
+
+  NB. ── prop_51 CSL beneficence ─────────────────────────────────────────────
+  try.
+    v =. (1 0) csl_beneficence ((0.5 0) ; 0.1 ; 0.1)
+    if. v = CSL_PASS do. pass 'prop_51'
+    else. (('beneficence=' , ": v)) fail 'prop_51' end.
+  catch. (13!:12 '') fail 'prop_51' end.
+
+  NB. ── prop_52 CSL commutation ─────────────────────────────────────────────
+  try.
+    cocurrent 'foundry'
+    idT =: ]
+    idF =: ]
+    cocurrent 'base'
+    v =. (1 2) csl_commutation ((<'idT') ; (<'idF') ; 0.1)
+    if. v = CSL_PASS do. pass 'prop_52'
+    else. (('commutation=' , ": v)) fail 'prop_52' end.
+  catch. (13!:12 '') fail 'prop_52' end.
+
+  NB. ── prop_53 AceCertificate safety margin ────────────────────────────────
+  try.
+    m =. 0.5 ace_safety_margin 0.1
+    NB. (1-0.1)-0.5 = 0.4
+    if. 1e_9 > | m - 0.4 do. pass 'prop_53'
+    else. (('margin=' , ": m)) fail 'prop_53' end.
+  catch. (13!:12 '') fail 'prop_53' end.
+
+  NB. ── prop_54 AceCertificate tail bound ───────────────────────────────────
+  try.
+    t =. 1 ace_tail_bound 0.5
+    inf =. 1 ace_tail_bound 1
+    if. (1e_9 > | t - 2) *. (inf = _) do. pass 'prop_54'
+    else. (('tail=' , (": t) , ' inf=' , ": inf)) fail 'prop_54' end.
+  catch. (13!:12 '') fail 'prop_54' end.
+
+  NB. ── prop_55 Guardian spectral legality ──────────────────────────────────
+  'no Core guardian verb (gate theater out of harness scope)' skip 'prop_55'
+
+  NB. ── prop_56 Consensus / false-positive bound (narrative) ────────────────
+  'narrative-only consensus / 2^-256 bound' skip 'prop_56'
+  ''
+)
+
+run_emit_csl_ace ''

verify/tests/goldilocks.ijs

@@ -0,0 +1,156 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Named tests + Goldilocks props 1–18 (where Core verbs exist).
+
+run_goldilocks =: 3 : 0
+  if. -. CORE_OK do.
+    r =. 'missing ' , FOUNDRY_IJS
+    r blocked 'goldilocks_add'
+    r blocked 'goldilocks_mul'
+    r blocked 'goldilocks_inv'
+    r blocked 'goldilocks_sub'
+    '' return.
+  end.
+
+  NB. ── named tests (baseline) ──────────────────────────────────────────────
+  try. r =. 100x fp_add 200x
+    if. r = 300x do. pass 'goldilocks_add' else. (('expected 300 got ' , ": r)) fail 'goldilocks_add' end.
+  catch. (13!:12 '') fail 'goldilocks_add' end.
+
+  try. r =. 7x fp_mul 6x
+    if. r = 42x do. pass 'goldilocks_mul' else. (('expected 42 got ' , ": r)) fail 'goldilocks_mul' end.
+  catch. (13!:12 '') fail 'goldilocks_mul' end.
+
+  try. one =. 42x fp_mul (fp_inv 42x)
+    if. one = 1x do. pass 'goldilocks_inv' else. (('expected 1 got ' , ": one)) fail 'goldilocks_inv' end.
+  catch. (13!:12 '') fail 'goldilocks_inv' end.
+
+  try. r =. 100x fp_sub 50x
+    if. r = 50x do. pass 'goldilocks_sub' else. (('expected 50 got ' , ": r)) fail 'goldilocks_sub' end.
+  catch. (13!:12 '') fail 'goldilocks_sub' end.
+
+  NB. ── prop_1 Goldilocks prime (decimal) ───────────────────────────────────
+  try.
+    if. GOLDILOCKS_PRIME = 18446744069414584321x do. pass 'prop_1'
+    else. (('got ' , ": GOLDILOCKS_PRIME)) fail 'prop_1' end.
+  catch. (13!:12 '') fail 'prop_1' end.
+
+  NB. ── prop_2 hex / named constant (= decimal p) ───────────────────────────
+  try.
+    if. (p = GOLDILOCKS_PRIME) *. (p = 18446744069414584321x) do. pass 'prop_2'
+    else. 'p / GOLDILOCKS_PRIME mismatch' fail 'prop_2' end.
+  catch. (13!:12 '') fail 'prop_2' end.
+
+  NB. ── prop_3 field elements reduced mod p (carrier < p) ───────────────────
+  try.
+    r =. fp_reduce 42x
+    if. (r = 42x) *. (r < p) do. pass 'prop_3'
+    else. (('got ' , ": r)) fail 'prop_3' end.
+  catch. (13!:12 '') fail 'prop_3' end.
+
+  NB. ── prop_4 Elem construction reduces (fp_reduce) ────────────────────────
+  try.
+    r =. fp_reduce (p + 5x)
+    if. r = 5x do. pass 'prop_4'
+    else. (('expected 5 got ' , ": r)) fail 'prop_4' end.
+  catch. (13!:12 '') fail 'prop_4' end.
+
+  NB. ── prop_5 congruence 2^64 ≡ 2^32-1 (mod p) ──────────────────────────────
+  try.
+    NB. TWO64 - p = 2^32 - 1 = EPSILON_FOLD
+    if. (TWO64_foundry_ - p) = EPSILON_FOLD do. pass 'prop_5'
+    else. 'TWO64 - p != EPSILON_FOLD' fail 'prop_5' end.
+  catch. (13!:12 '') fail 'prop_5' end.
+
+  NB. ── prop_6 EPSILON fold constant ────────────────────────────────────────
+  try.
+    if. EPSILON_FOLD = 4294967295x do. pass 'prop_6'
+    else. (('got ' , ": EPSILON_FOLD)) fail 'prop_6' end.
+  catch. (13!:12 '') fail 'prop_6' end.
+
+  NB. ── prop_7..11 mulmod fold path (exercised via fp_mulmod / fp_mul) ──────
+  NB. Internal 128-bit split is not separately exported; identity a*b mod p
+  NB. via Goldilocks fold covers props 7–11 as a unit for harness purposes.
+  try.
+    r =. 7x fp_mulmod 6x
+    if. r = 42x do. pass 'prop_7'
+    else. (('fp_mulmod 7*6 expected 42 got ' , ": r)) fail 'prop_7' end.
+  catch. (13!:12 '') fail 'prop_7' end.
+
+  try.
+    NB. larger product exercises hi/lo split (props 8–11)
+    a =. 123456789x
+    b =. 987654321x
+    r =. a fp_mulmod b
+    expect =. p | (a * b)
+    if. r = expect do. pass 'prop_8'
+    else. (('hi_lo path mismatch got ' , (": r) , ' expect ' , ": expect)) fail 'prop_8' end.
+  catch. (13!:12 '') fail 'prop_8' end.
+
+  try.
+    a =. (p - 1x)
+    b =. (p - 1x)
+    r =. a fp_mulmod b
+    expect =. p | (a * b)
+    if. r = expect do. pass 'prop_9'
+    else. (('fold identity fail got ' , (": r) , ' expect ' , ": expect)) fail 'prop_9' end.
+  catch. (13!:12 '') fail 'prop_9' end.
+
+  try.
+    NB. underflow / conditional reduction path: product near multiples of p
+    r =. 2x fp_mulmod (p - 1x)
+    expect =. p | (2x * (p - 1x))
+    if. r = expect do. pass 'prop_10'
+    else. (('underflow path got ' , (": r) , ' expect ' , ": expect)) fail 'prop_10' end.
+  catch. (13!:12 '') fail 'prop_10' end.
+
+  try.
+    r =. 3x fp_mulmod 5x
+    if. (r < p) *. (r = 15x) do. pass 'prop_11'
+    else. (('final reduce got ' , ": r)) fail 'prop_11' end.
+  catch. (13!:12 '') fail 'prop_11' end.
+
+  NB. ── prop_12 single-limb reduce ──────────────────────────────────────────
+  try.
+    ok =. ((fp_reduce 10x) = 10x) *. ((fp_reduce p) = 0x) *. ((fp_reduce (p + 1x)) = 1x)
+    if. ok do. pass 'prop_12' else. 'fp_reduce cases failed' fail 'prop_12' end.
+  catch. (13!:12 '') fail 'prop_12' end.
+
+  NB. ── prop_13 add ─────────────────────────────────────────────────────────
+  try.
+    if. (100x fp_add 200x) = 300x do. pass 'prop_13' else. 'add != 300' fail 'prop_13' end.
+  catch. (13!:12 '') fail 'prop_13' end.
+
+  NB. ── prop_14 sub ─────────────────────────────────────────────────────────
+  try.
+    if. (100x fp_sub 50x) = 50x do. pass 'prop_14' else. 'sub != 50' fail 'prop_14' end.
+  catch. (13!:12 '') fail 'prop_14' end.
+
+  NB. ── prop_15 mul ─────────────────────────────────────────────────────────
+  try.
+    if. (7x fp_mul 6x) = 42x do. pass 'prop_15' else. 'mul != 42' fail 'prop_15' end.
+  catch. (13!:12 '') fail 'prop_15' end.
+
+  NB. ── prop_16 Fermat inverse ──────────────────────────────────────────────
+  try.
+    one =. 42x fp_mul (fp_inv 42x)
+    if. one = 1x do. pass 'prop_16' else. (('a*inv(a) got ' , ": one)) fail 'prop_16' end.
+  catch. (13!:12 '') fail 'prop_16' end.
+
+  NB. ── prop_17 binary exponentiation ───────────────────────────────────────
+  try.
+    r =. 7x fp_pow 3x
+    if. r = 343x do. pass 'prop_17' else. (('7^3 got ' , ": r)) fail 'prop_17' end.
+  catch. (13!:12 '') fail 'prop_17' end.
+
+  NB. ── prop_18 batch add/mul ───────────────────────────────────────────────
+  try.
+    ra =. 100 200 fp_add_batch 1 2
+    rm =. 7 8 fp_mul_batch 6 5
+    if. (ra -: 101 202) *. (rm -: 42 40) do. pass 'prop_18'
+    else. (('batch got add=' , (": ra) , ' mul=' , ": rm)) fail 'prop_18' end.
+  catch. (13!:12 '') fail 'prop_18' end.
+  ''
+)
+
+run_goldilocks ''

verify/tests/pmat.ijs

@@ -0,0 +1,107 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Named tests + PMAT props 26–32.
+
+run_pmat =: 3 : 0
+  if. -. CORE_OK do.
+    r =. 'missing ' , FOUNDRY_IJS
+    r blocked 'pmat_insert'
+    r blocked 'pmat_conservation'
+    '' return.
+  end.
+
+  NB. ── named tests ─────────────────────────────────────────────────────────
+  try.
+    m =. 3 pmat_new 3
+    'm ok1' =. m pmat_insert 0 0 1 1 1
+    'm ok2' =. m pmat_insert 0 1 _1 0 1
+    c =. # pmat_entries m
+    if. ok1 *. ok2 *. c = 2 do. pass 'pmat_insert'
+    else. (('ok1=' , (": ok1) , ' ok2=' , (": ok2) , ' count=' , ": c)) fail 'pmat_insert' end.
+  catch. (13!:12 '') fail 'pmat_insert' end.
+
+  try.
+    m =. 2 pmat_new 2
+    'm ok' =. m pmat_insert 0 0 1 3 5
+    'm ok' =. m pmat_insert 0 1 _1 1 2
+    'm ok' =. m pmat_insert 1 0 1 2 1
+    cons =. pmat_conservation m
+    if. cons -: 6 8 do. pass 'pmat_conservation'
+    else. (('expected 6 8 got ' , ": cons)) fail 'pmat_conservation' end.
+  catch. (13!:12 '') fail 'pmat_conservation' end.
+
+  NB. ── prop_26 PMat entry shape (sign, monomial ds/dt, row, col) ────────────
+  try.
+    m =. 2 pmat_new 2
+    'm ok' =. m pmat_insert 0 1 _1 3 4
+    e =. {. pmat_entries m
+    NB. entry row: sign, ds, dt, row, col
+    if. ok *. (e -: _1 3 4 0 1) do. pass 'prop_26'
+    else. (('entry=' , ": e)) fail 'prop_26' end.
+  catch. (13!:12 '') fail 'prop_26' end.
+
+  NB. ── prop_27 insert domain checks ────────────────────────────────────────
+  try.
+    m =. 2 pmat_new 2
+    'm1 ok_bad_row' =. m pmat_insert 5 0 1 0 0
+    'm2 ok_bad_sign' =. m pmat_insert 0 0 2 0 0
+    'm3 ok_good' =. m pmat_insert 0 0 1 1 1
+    if. (-. ok_bad_row) *. (-. ok_bad_sign) *. ok_good do. pass 'prop_27'
+    else. 'domain checks wrong' fail 'prop_27' end.
+  catch. (13!:12 '') fail 'prop_27' end.
+
+  NB. ── prop_28 grading stub (mirrors C++ always-true) ───────────────────────
+  try.
+    m =. 2 pmat_new 2
+    'm ok' =. m pmat_insert 0 0 1 1 1
+    if. 1 = pmat_validate_grading m do. pass 'prop_28'
+    else. 'validate_grading not 1' fail 'prop_28' end.
+  catch. (13!:12 '') fail 'prop_28' end.
+
+  NB. ── prop_29 conservation ────────────────────────────────────────────────
+  try.
+    m =. 2 pmat_new 2
+    'm ok' =. m pmat_insert 0 0 1 3 5
+    'm ok' =. m pmat_insert 0 1 _1 1 2
+    'm ok' =. m pmat_insert 1 0 1 2 1
+    if. (pmat_conservation m) -: 6 8 do. pass 'prop_29'
+    else. 'conservation != 6 8' fail 'prop_29' end.
+  catch. (13!:12 '') fail 'prop_29' end.
+
+  NB. ── prop_30 compose preserves shape (rows_A × cols_B) ───────────────────
+  try.
+    a =. 2 pmat_new 3
+    'a ok' =. a pmat_insert 0 1 1 1 0
+    b =. 3 pmat_new 2
+    'b ok' =. b pmat_insert 1 0 1 0 2
+    c =. a pmat_compose b
+    if. (pmat_shape c) -: 2 2 do. pass 'prop_30'
+    else. (('shape=' , ": pmat_shape c)) fail 'prop_30' end.
+  catch. (13!:12 '') fail 'prop_30' end.
+
+  NB. ── prop_31 compose monomial rule (ds+=a.ds, dt+=b.dt; sign*=) ──────────
+  try.
+    a =. 1 pmat_new 1
+    'a ok' =. a pmat_insert 0 0 1 5 0
+    b =. 1 pmat_new 1
+    'b ok' =. b pmat_insert 0 0 _1 0 7
+    c =. a pmat_compose b
+    e =. {. pmat_entries c
+    NB. sign = 1*_1 = -1; ds=5; dt=7; row=0; col=0
+    if. e -: _1 5 7 0 0 do. pass 'prop_31'
+    else. (('compose entry=' , ": e)) fail 'prop_31' end.
+  catch. (13!:12 '') fail 'prop_31' end.
+
+  NB. ── prop_32 Frobenius = sqrt(#entries) ──────────────────────────────────
+  try.
+    m =. 2 pmat_new 2
+    'm ok' =. m pmat_insert 0 0 1 1 1
+    'm ok' =. m pmat_insert 0 1 1 2 3
+    f =. pmat_frobenius m
+    if. 1e_9 > | f - %: 2 do. pass 'prop_32'
+    else. (('frobenius=' , ": f)) fail 'prop_32' end.
+  catch. (13!:12 '') fail 'prop_32' end.
+  ''
+)
+
+run_pmat ''

verify/tests/recurrence.ijs

@@ -0,0 +1,130 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Named tests + recurrence props 39–46 (41 narrative SKIP).
+
+run_recurrence =: 3 : 0
+  if. -. CORE_OK do.
+    ('missing ' , FOUNDRY_IJS) blocked 'recurrence_converges'
+    '' return.
+  end.
+
+  try.
+    cocurrent 'foundry'
+    verify_T =: 3 : ', (0.5 * {. y) + 0.3'
+    verify_proj =: 3 : '_1 >. 1 <. , y'
+    cocurrent 'base'
+
+    if. 0 = 4!:0 <'rec_run' do.
+      'rec_run not exported' fail 'recurrence_converges'
+      '' return.
+    end.
+
+    hist =. (, 1.) rec_run 200 ; T1 ; WP_UNIFORM ; 1e_6 ; (<'verify_T') ; (<'verify_proj')
+    st =. REC_STATE_foundry_
+    conv =. > 1 { st
+    resid =. 99.
+    if. 0 < # hist do.
+      last =. > {: hist
+      resid =. > 6 { last
+    end.
+
+    if. conv *. resid < 1e_6 do. pass 'recurrence_converges'
+    else. (('converged=' , (": conv) , ' residual=' , ": resid)) fail 'recurrence_converges' end.
+  catch.
+    (13!:12 '') fail 'recurrence_converges'
+  end.
+
+  NB. ── prop_39 recurrence equation via rec_step ────────────────────────────
+  try.
+    cocurrent 'foundry'
+    verify_T =: 3 : ', 0.5 * , y'
+    verify_proj =: ]
+    cocurrent 'base'
+    xi =. 0.5 0
+    lam =. 0 0.3
+    g =. 0.1 0
+    x0 =. 1 1
+    pair =. x0 rec_step xi ; lam ; g ; (<'verify_T') ; (<'verify_proj') ; 0 ; T1
+    xn =. , > 0 { pair
+    NB. x'[i] = xi[i]*x[i] + lam[i]*T(x)[i] + g[i]; T=0.5*x
+    NB. i0: 0.5*1 + 0*0.5 + 0.1 = 0.6
+    NB. i1: 0*1 + 0.3*0.5 + 0 = 0.15
+    expect =. 0.6 0.15
+    if. 1e_9 > >./ | xn - expect do. pass 'prop_39'
+    else. (('x_next=' , ": xn)) fail 'prop_39' end.
+  catch. (13!:12 '') fail 'prop_39' end.
+
+  NB. ── prop_40 contraction condition q < 1-ε after soft project ────────────
+  try.
+    cocurrent 'foundry'
+    verify_T =: 3 : ', 0.5 * , y'
+    verify_proj =: ]
+    cocurrent 'base'
+    pair =. (, 1.) rec_step (0.5 0) ; (0 0.2) ; (0) ; (<'verify_T') ; (<'verify_proj') ; 0 ; T1
+    info =. > 1 { pair
+    q =. > 1 { info
+    eps =. > 2 { info
+    if. q < 1 - eps do. pass 'prop_40'
+    else. (('q=' , (": q) , ' eps=' , ": eps)) fail 'prop_40' end.
+  catch. (13!:12 '') fail 'prop_40' end.
+
+  NB. ── prop_41 unique fixed-point guarantee (narrative) ────────────────────
+  'narrative-only Banach guarantee' skip 'prop_41'
+
+  NB. ── prop_42 q_estimate coded form ───────────────────────────────────────
+  try.
+    q =. q_estimate (0.5 0) ; (0 0.2) ; (1 1) ; (0.5 0.5)
+    NB. n_xi=0.5, n_lam=0.2, n_T=0.5/1=0.5 → q=0.5+0.2*0.5=0.6
+    if. 1e_9 > | q - 0.6 do. pass 'prop_42'
+    else. (('q=' , ": q)) fail 'prop_42' end.
+  catch. (13!:12 '') fail 'prop_42' end.
+
+  NB. ── prop_43 soft projection ─────────────────────────────────────────────
+  try.
+    sp =. ((0.9 0) ; (0 0.9)) soft_project 1.2 0.1
+    xi =. , > 0 { sp
+    lam =. , > 1 { sp
+    NB. target=0.9; scale=0.9/1.2=0.75 → 0.675
+    if. (1e_9 > | (0 { xi) - 0.675) *. (1e_9 > | (1 { lam) - 0.675) do. pass 'prop_43'
+    else. (('xi=' , (": xi) , ' lam=' , ": lam)) fail 'prop_43' end.
+  catch. (13!:12 '') fail 'prop_43' end.
+
+  NB. ── prop_44 weight budget split 0.7/0.3 of q_star ───────────────────────
+  try.
+    sched =. synth_weights 1 ; T1 ; WP_UNIFORM
+    xi =. {. > 0 { sched
+    lam =. {. > 1 { sched
+    q_star =. 1 - 0.10
+    expect_xi =. q_star * 0.7
+    expect_lam =. q_star * 0.3
+    if. (1e_9 > | (0 { xi) - expect_xi) *. (1e_9 > | (1 { lam) - expect_lam) do. pass 'prop_44'
+    else. (('xi=' , (": xi) , ' lam=' , ": lam)) fail 'prop_44' end.
+  catch. (13!:12 '') fail 'prop_44' end.
+
+  NB. ── prop_45 projector clip [-1,1] ───────────────────────────────────────
+  try.
+    cocurrent 'foundry'
+    verify_T =: ]
+    verify_proj =: 3 : '_1 >. 1 <. , y'
+    cocurrent 'base'
+    NB. xi=1 carries x=5 through affine update; projector clips to 1
+    pair =. (, 5.) rec_step (1 0) ; (0 0) ; (0) ; (<'verify_T') ; (<'verify_proj') ; 0 ; T1
+    xn =. , > 0 { pair
+    if. xn = 1 do. pass 'prop_45'
+    else. (('projected=' , ": xn)) fail 'prop_45' end.
+  catch. (13!:12 '') fail 'prop_45' end.
+
+  NB. ── prop_46 residual / convergence ──────────────────────────────────────
+  try.
+    hist =. (, 1.) rec_run 200 ; T1 ; WP_UNIFORM ; 1e_6 ; (<'verify_T') ; (<'verify_proj')
+    st =. REC_STATE_foundry_
+    conv =. > 1 { st
+    resid =. 99.
+    if. 0 < # hist do. resid =. > 6 { > {: hist end.
+    if. conv *. resid < 1e_6 do. pass 'prop_46'
+    else. (('conv=' , (": conv) , ' resid=' , ": resid)) fail 'prop_46' end.
+  catch. (13!:12 '') fail 'prop_46' end.
+  ''
+)
+
+run_recurrence ''

verify/tests/spectral.ijs

@@ -0,0 +1,77 @@
+NB. Copyright (C) 2026 Foundry J contributors
+NB. SPDX-License-Identifier: AGPL-3.0-or-later
+NB. Named tests + spectral props 33–38.
+NB. Core BOXING.md: SpectralResult producers return <fields>; open before indexing.
+
+run_spectral =: 3 : 0
+  if. -. CORE_OK do.
+    r =. 'missing ' , FOUNDRY_IJS
+    r blocked 'spectral_contractive'
+    r blocked 'spectral_expansive'
+    '' return.
+  end.
+
+  NB. Open <SpectralResult> — Core sr_open is > after foundry_export
+  open =. ]
+  if. 3 = 4!:0 <'sr_open' do. open =. sr_open else. open =. > end.
+
+  Jc =. 2 2 $ 0.2 0.1 0.05 0.15
+  Je =. 2 2 $ 0.9 0.3 0.3 0.95
+
+  NB. ── named tests ─────────────────────────────────────────────────────────
+  try.
+    res =. open Jc spectral_analyze 0.1
+    if. > 1 { res do. pass 'spectral_contractive' else. 'should be contractive' fail 'spectral_contractive' end.
+  catch. (13!:12 '') fail 'spectral_contractive' end.
+
+  try.
+    res =. open Je spectral_analyze 0.1
+    if. -. > 1 { res do. pass 'spectral_expansive' else. 'should not be contractive' fail 'spectral_expansive' end.
+  catch. (13!:12 '') fail 'spectral_expansive' end.
+
+  NB. ── prop_33 Gershgorin disk bound ───────────────────────────────────────
+  try.
+    b =. gershgorin_bound Jc
+    if. 1e_9 > | b - 0.3 do. pass 'prop_33'
+    else. (('bound=' , ": b)) fail 'prop_33' end.
+  catch. (13!:12 '') fail 'prop_33' end.
+
+  NB. ── prop_34 contractive via Gershgorin ──────────────────────────────────
+  try.
+    res =. open Jc gershgorin_check 0.1
+    if. > 1 { res do. pass 'prop_34' else. 'gershgorin_check not contractive' fail 'prop_34' end.
+  catch. (13!:12 '') fail 'prop_34' end.
+
+  NB. ── prop_35 power iteration (Rayleigh) ──────────────────────────────────
+  try.
+    ev =. Jc power_iteration 100 1e_12
+    if. (ev > 0) *. (ev < 0.9) do. pass 'prop_35'
+    else. (('power_iteration=' , ": ev)) fail 'prop_35' end.
+  catch. (13!:12 '') fail 'prop_35' end.
+
+  NB. ── prop_36 power_iteration_check contractive predicate ─────────────────
+  try.
+    res =. open Jc power_iteration_check 0.1 100
+    if. > 1 { res do. pass 'prop_36' else. 'PI check not contractive' fail 'prop_36' end.
+  catch. (13!:12 '') fail 'prop_36' end.
+
+  NB. ── prop_37 analyze fallback policy (Gershgorin then optional PI) ───────
+  try.
+    res =. open Jc spectral_analyze 0.1
+    c =. > 1 { res
+    used =. > 4 { res
+    if. c *. (-. used) do. pass 'prop_37'
+    else. (('c=' , (": c) , ' used_pi=' , ": used)) fail 'prop_37' end.
+  catch. (13!:12 '') fail 'prop_37' end.
+
+  NB. ── prop_38 tested contractive / expansive examples ─────────────────────
+  try.
+    okc =. > 1 { open Jc spectral_analyze 0.1
+    oke =. -. > 1 { open Je spectral_analyze 0.1
+    if. okc *. oke do. pass 'prop_38'
+    else. 'prop_38 example matrices failed' fail 'prop_38' end.
+  catch. (13!:12 '') fail 'prop_38' end.
+  ''
+)
+
+run_spectral ''